From 6f11d9a4d40b42c362d2dadb79c2d32caea2e7c0 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 25 Apr 2025 13:55:28 +0100
Subject: Clarify the table.

---
 sec/systemt.ltx | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 8fcedd1..8b3f173 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -109,24 +109,27 @@ and test equality recursively.
 
 In the remainder of the section we outline four different strategies for
 encoding inductive types within System~T. We judge each encoding on whether it
-is a local, simply-typed transformation as well as how easy it is to hand write
-the three fundamental operators. As you can see from the summary in
-\cref{tbl:encodings}, each strategy is lacking in some regard.
+can encode inductive types with higher-order data such as functions; is a local,
+simply-typed transformation that does not require polymorphism or a global
+program analysis; as well as how easy it is to hand write the three fundamental
+operators. As you can see from the summary in \cref{tbl:encodings}, each
+strategy is lacking in some regard.
 
 \begin{table}
   \caption{Comparison of encoding strategies for inductive types within
-    System~T. The first column assesses if the strategy is a local, simply-typed
-    transformation. The remainder indicate whether it is ``easy'' to hand write
-    the constructors, fold and pattern matching
+    System~T. The first two columns assesses whether a strategy works for
+    higher-order types and is a local, simply-typed transformation. The
+    remainder indicate whether it is ``easy'' (\ding{51}) or possible
+    (\ding{81}) to hand write the constructors, fold and pattern matching
     respectively.}\label{tbl:encodings}
-  \begin{tabular}{lcccc}
+  \begin{tabular}{lccccc}
     \toprule
-    Strategy & Local & Constructors & Fold & Pattern Match \\
+    Strategy & Higher Order & Local & Constructors & Fold & Pattern Match \\
     \midrule
-    G\"odel & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\
-    Church & \ding{55} & \ding{51} & \ding{51} & \ding{55} \\
-    Eliminator & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\
-    Heap & \ding{51} & \ding{55} & \ding{51} & \ding{51} \\
+    G\"odel & \ding{55} & \ding{51} & \ding{51} & \ding{81} & \ding{51} \\
+    Church & \ding{51} & \ding{55} & \ding{51} & \ding{51} & \ding{81} \\
+    Eliminator & \ding{51} & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\
+    Heap & \ding{51} & \ding{51} & \ding{81} & \ding{81} & \ding{51} \\
     \bottomrule
   \end{tabular}
 \end{table}
-- 
cgit v1.2.3

