State some limits of partial evaluation.

1 files changed, 12 insertions, 6 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index d7e7344..b5edb14 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -193,11 +193,17 @@ 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 potential benefit of composing two programs
-    \item explain the limitiations of the reducer (e.g. eta and bools)
-  \end{itemize}
-}
+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?}
 
 \end{document}