summaryrefslogtreecommitdiff
path: root/sec/reducer.ltx
diff options
context:
space:
mode:
Diffstat (limited to 'sec/reducer.ltx')
-rw-r--r--sec/reducer.ltx11
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}