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