Describe why composing programs could work.

1 files changed, 10 insertions, 1 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index b1c597a..d7e7344 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -183,9 +183,18 @@ exactly as expressive as the chosen type, with inductive hypothesis
 hypothesis for two reasons: it has a simpler categorical semantics;
 many folds do not need the non-destructive argument.
 
+\subsection{Composing the Two Programs}
+
+Our encoding algorithm introduces many administrative
+\(\beta\)-redexes. We manually reduced many of them in the examples at the
+end of each phase in \cref{M-sec:encoding}. The final desugaring in
+phase seven also introduced many redexes when eliminating \letkw{}
+expressions. Thus the ``efficiency'' of an encoded program can be
+improved by performing the simple partial evaluation of our fuelled
+reducer.
+
 \TODO{
   \begin{itemize}
-    \item describe why encoded terms have lots of beta redices
     \item describe potential benefit of composing two programs
     \item explain the limitiations of the reducer (e.g. eta and bools)
   \end{itemize}