\documentclass[../main.tex]{subfiles}

\begin{document}
\section{Writing ARTyST Programs}%
\label{sec:reducer}

We have used \lang{} to write two non-trivial programs that can be
embedded in System~T. The first is a fuelled reducer for
System~T. Given \(n\) units of fuel, the reducer will perform \(n\)
steps of complete~development~\cite{cd} on a System~T term. The second
program is the encoding from \lang{} to System~T. This takes a
type-annotated \lang{} program and encodes it as a System~T term.

\TODO{
  \begin{itemize}
    \item describe the syntactic sugar I have added
  \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 explain why fuel is necessary for the reducer
    \item show some example snippets
  \end{itemize}
}

\TODO{
  \begin{itemize}
    \item describe the inputs to the embedding
    \item describe the output of the embedding
    \item show a ``non-destructive'' fold
    \item justify use of destructive folds
  \end{itemize}
}

\TODO{
  \begin{itemize}
    \item describe why encoded terms have lots of beta redices
    \item describe potential benefit of composing two programs
    \item explain the limitiations of the reducer (e.g. eta and bools)
  \end{itemize}
}

\end{document}