From 1fd772839e9336310155eb39be3698032996f7f4 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 24 Apr 2025 13:32:12 +0100 Subject: Describe the roll' operator. --- sec/encoding.ltx | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'sec/encoding.ltx') diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 0e7b244..8087e20 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -60,10 +60,22 @@ inductive type \(\mu X. (1 + \nat \times X + \mu Y. 1 + X \times Y) \times (1 + this type can have any number of inductive values, located in distant parts of the term. +Collecting all the inductive values into one location will make future encoding +steps much easier. We enforce this by removing the \roll{} operator and adding +the \roll*{} operator, which has the following type derivation: +\[ +\begin{prooftree} + \hypo{\judgement{\Gamma}{t}{\mathsf{List}~(\mu X.A)}} + \hypo{\judgement{\Gamma}{u}{\sub{A}{X/\nat}}} + \infer2{\judgement{\Gamma}{\roll*~t~u}{\mu X. A}} +\end{prooftree} +\] +Rather than include the inductive values within the term to roll, they are +instead gathered into an external list. The places that contained inductive +values in the rolled term now contain indices into the list. + \TODO{ \begin{itemize} - \item describe that collecting them into one location makes future encoding - steps easier \item justify why I add lists as a built-in type former \item describe the strength function, the key step in this phase \item state it is defined by induction on the outer functor -- cgit v1.2.3