Describe encoding of inductive types.

2 files changed, 11 insertions, 3 deletions

diff --git a/main.tex b/main.tex
index f5743b9..91aa555 100644
--- a/main.tex
+++ b/main.tex
@@ -71,7 +71,7 @@
   \setcopyright{none}
 \fi
 
-\title{ARTiST:\ Adding Regular Types in System~T}
+\title{ARTyST:\ Adding Regular Types to System~T}
 
 \ifacmart
   \keywords{}
@@ -154,7 +154,7 @@
 \newmintinline[systemtinline]{'lexer.py:SystemTLexer -x'}{}
 
 % TODOS and such
-\newcommand\lang{{\color{Green} ARTiST}}
+\newcommand\lang{{\color{Green} ARTyST}}
 \newcommand\TODO[1]{{\color{Blue}TODO:\ {#1}}}
 \newcommand\FIXME[1]{{\color{Red}FIXME:\ {#1}}}
 
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index ffc868b..a8d0269 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -101,9 +101,17 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X
 that calls each accumulator within \(A\) in sequence. The definition is by
 induction on the well-formedness derivation.
 
+\subsection{Phase 2: Encoding Inductive Types}%
+\label{subsec:inductive-types}
+
+We use a modified heap encoding to encode regular types. We use a
+\(\mathsf{List}~\nat\)-indexed heap, but keep the pointers within terms as
+naturals. The idea is that the heap index describes the path taken through the
+term to reach a particular point, whilst the pointers describe the next step
+along the path.
+
 \TODO{
   \begin{itemize}
-    \item state that we encode inductive types as nat-list-indexed heaps
     \item describe that storing higher-order data makes G\"odel encodings
       impractical
     \item describe that the need for local encodings rules out Church encodings