From 02895b46ecbf12728d5545cad2361e6751c495a9 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 26 Jun 2025 18:06:46 +0100 Subject: Fix 901--915. --- sec/reducer.ltx | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/sec/reducer.ltx b/sec/reducer.ltx index 2a0b193..78a341b 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -183,22 +183,20 @@ not need the non-destructive argument. 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{} +phase seven also introduces 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. +improved by partially evaluating of our fuelled reducer. Even with a partial reduction pass, our encoder can still have some performance issues. Neither \lang{} nor System~T have \emph{commuting conversions}; equations about how two case splits, folds or primitive recursions interact. This means two contextually equivalent terms are -not equal in the equational theory. An example of this are the -\systemtinline{compose} and \systemtinline{compose'} functions from -encoding phase two. Because it performs fewer pattern matches, -\systemtinline{compose'} would have a encoding than -\systemtinline{compose} despite containing the same information. - -There are no equations we can add to resolve this for \foldkw{} or -\primreckw{}. \TODO{how do I mitigate this?} +not equal in the equational theory. An example of this is our +simplification of the \systemtinline{compose} function from encoding +phase two. Because it performs fewer pattern matches, the second +\systemtinline{compose} would have a ``simpler'' encoding than the +original despite containing the same information. + +\TODO{System~T self reducer} \end{document} -- cgit v1.2.3