From 9d1ecdd0ca556ad1899275bd50dc5468c35f898e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 27 May 2025 18:07:11 +0100
Subject: Describe why composing programs could work.

---
 sec/reducer.ltx | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'sec/reducer.ltx')

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}
-- 
cgit v1.2.3

