From 5f572b63ed243ac2d77575935beafcdace085809 Mon Sep 17 00:00:00 2001 From: Chloe Brown 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