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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
\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}
|
