1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
\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}
\TODO{
\begin{itemize}
\item show some example snippets
\item explain why fuel is necessary for the reducer
\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}
|
