diff options
Diffstat (limited to 'sec/reducer.ltx')
| -rw-r--r-- | sec/reducer.ltx | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx index 732154f..77b5ce7 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -120,7 +120,9 @@ let step (t : Term) : Term = \caption{Implementation of complete development.}\label{lst:step} \end{listing} -\TODO{explain why fuel is necessary for the reducer} +Our reducer only applies \(\beta\)-reduction. It is also possible to +perform \(\eta\)-contraction as computing a strengthened term requires only +structural induction. \subsection{Encoding Algorithm}% \label{subsec:encoding} |