From 9d1ecdd0ca556ad1899275bd50dc5468c35f898e Mon Sep 17 00:00:00 2001 From: Chloe Brown 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(-) 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