diff options
Diffstat (limited to 'sec/reducer.ltx')
-rw-r--r-- | sec/reducer.ltx | 11 |
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} |