From 84c45da603f38a7cd4e691386778920d30fe9047 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 21 May 2025 14:12:31 +0100
Subject: Describe the operation of the fuelled reducer.

---
 sec/reducer.ltx | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'sec/reducer.ltx')

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

