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