Fix 901--915.

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}