\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{describe the syntactic sugar I have added}

\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.

We define System~T terms as the inductive type in
\cref{lst:term-ty}. The compiler, detailed in \cref{M-sec:compiler}
makes a few small changes to the syntax to be more descriptive. Most
notably, products are indexed by labels instead of by position. For
example, the \verb|Primrec| constructor takes a product with three
components: the target, and the branches for zero and successor. As
\lang{} is simply typed, there is no way to enforce terms are
correctly typed nor correctly scoped.

\begin{listing}
  \begin{verbatim}
data Term
  [ Var: Nat
  ; Zero: <>
  ; Suc: Term
  ; Primrec: <Zero: Term; Suc: Term, Target: Term>
  ; Abs: Term
  ; App: <Fun: Term, Arg: Term>
  ]
  \end{verbatim}
  \caption{Inductive type representing System~T terms.}\label{lst:term-ty}
\end{listing}

An example function is \verb|rename|, taking a term and a renaming
function \verb|Nat -> Nat|, and updating all variables according to
the renaming function. The program is in \cref{lst:rename}. We use
\verb|~| as the syntax for \roll{} and \verb|foldcase| is syntactic
sugar for performing a \foldkw{} whose body immediately pattern
matches on the induction hypothesis. Recall that a fold fills the
shape type with the motive. For example, for the \verb|App| branch,
\verb|p| has type
\verb|<Fun: (Nat -> Nat) -> Term; Arg: (Nat -> Nat) -> Term>|. As
application doesn't bind any variables, we can pass the renaming
\verb|f| to the inductive components without modification. For
abstraction and primitive recursion, we have to lift the renaming
function, corresponding to binding a variable.

\begin{listing}
  \begin{verbatim}
let rename (t : Term) : (Nat -> Nat) -> Term =
  foldcase t by
    { Var n     => \f => ~(Var (f n))
    ; Zero _    => \f => ~(Zero <>)
    ; Suc r     => \f => ~(Suc (r f))
    ; Primrec p => \f =>
      ~(Primrec <Zero: p.Zero f; Suc: p.Suc (lift f); Target: p.Target f>)
    ; Abs r     => \f => ~(Abs (r (lift f)))
    ; App p     => \f => ~(App <Fun: p.Fun f; Arg: p.Arg f>)
    }
  \end{verbatim}
  \caption{Implementation of term renaming.}\label{lst:rename}
\end{listing}

The main driver in the reducer is the \verb|step| function, which
performs a complete development of a term. We give its definition in
\cref{lst:step}. By induction, all terms within the \verb|foldcase|
have been completely developed. Most cases pass through their
arguments unchanged: the only reductions for \(\suc~t\) happen within
\(t\) for instance. The two interesting cases are \verb|Primrec| and
\verb|App|. Here we match on the ``active'' term, performing a
reduction if possible. If the active term is either a neutral
(\verb|Var|) or absurd (\verb|Zero| as a function) we return the
inductive argument without further computation applied. Our fuelled
reducer applies the \verb|step| function to the input for each unit of
fuel it is given.

\begin{listing}
  \begin{verbatim}
let step (t : Term) : Term =
  foldcase t by
    { Var n     => ~(Var n)
    ; Zero _    => ~(Zero <>)
    ; Suc t     => ~(Suc t)
    ; Primrec p =>
      let default = ~(Primrec p) in
      case p.Target of
        { Var _     => default
        ; Zero _    => p.Zero
        ; Suc t     =>
          sub p.Suc [ ~(Primrec <Zero: p.Zero; Suc: p.Suc; Target: t>) ]
        ; Primrec _ => default
        ; Abs _     => default
        ; App _     => default
        }
    ; Abs t     => ~(Abs t)
    ; App p     =>
      let default = ~(App p) in
      case p.Fun of
        { Var _     => default
        ; Zero _    => default
        ; Suc t     => default
        ; Primrec _ => default
        ; Abs t     => sub t [ p.Arg ]
        ; App _     => default
        }
    }
  \end{verbatim}
  \caption{Implementation of complete development.}\label{lst:rename}
\end{listing}

\TODO{explain why fuel is necessary for the reducer}

\subsection{Encoding Algorithm}%
\label{subsec:encoding}

In \cref{M-sec:encoding} we described a process to embed \lang{}
within System~T. We have written this algorithm in \lang{} itself,
simultaneously mechanising the conversion and proving it is
terminating. Our input is type-annotated \lang{} terms, and we output
unannotated System~T terms as in \cref{lst:term-ty}. Each phase is
accompanied by its own inductive types representing types and
type-annotated terms.

\TODO{
  \begin{itemize}
    \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}