diff options
| -rw-r--r-- | sec/reducer.ltx | 20 |
1 files 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} |