Describe the operation of the fuelled reducer.

1 files changed, 11 insertions, 1 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index c73a4f6..56b24f2 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -17,9 +17,19 @@ type-annotated \lang{} program and encodes it as a System~T term.
   \end{itemize}
 }
 
+\subsection{Fuelled System~T Reducer}%
+\label{subsec:reducer}
+
+Given enough fuel to work with, a fuelled reducer takes a term as
+input and reduces it to normal form. Our fuelled reducer operates
+using term rewriting. For each unit of fuel, we perform one step of
+complete development; we reduce \emph{all} beta redices in the input
+term simultaneously. As System~T is confluent and strongly
+normalising, complete development will converge on the normal form of
+the input term.
+
 \TODO{
   \begin{itemize}
-    \item describe the operation of the fuelled reducer
     \item explain why fuel is necessary for the reducer
     \item show some example snippets
   \end{itemize}