From 5f572b63ed243ac2d77575935beafcdace085809 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 30 May 2025 13:50:33 +0100
Subject: State some limits of partial evaluation.

---
 sec/reducer.ltx | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

(limited to 'sec/reducer.ltx')

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}
-- 
cgit v1.2.3

