754
|
1 |
(*<*)
|
|
2 |
theory Paper
|
1506
|
3 |
imports "../Nominal/Test" "LaTeXsugar"
|
754
|
4 |
begin
|
1493
|
5 |
|
|
6 |
notation (latex output)
|
|
7 |
swap ("'(_ _')" [1000, 1000] 1000) and
|
|
8 |
fresh ("_ # _" [51, 51] 50) and
|
1506
|
9 |
fresh_star ("_ #* _" [51, 51] 50) and
|
1493
|
10 |
supp ("supp _" [78] 73) and
|
|
11 |
uminus ("-_" [78] 73) and
|
|
12 |
If ("if _ then _ else _" 10)
|
754
|
13 |
(*>*)
|
|
14 |
|
|
15 |
section {* Introduction *}
|
|
16 |
|
|
17 |
text {*
|
1524
|
18 |
So far, Nominal Isabelle provides a mechanism for constructing
|
1607
|
19 |
alpha-equated terms, for example
|
1485
|
20 |
|
1520
|
21 |
\begin{center}
|
|
22 |
$t ::= x \mid t\;t \mid \lambda x. t$
|
|
23 |
\end{center}
|
|
24 |
|
|
25 |
\noindent
|
1550
|
26 |
where free and bound variables have names. For such terms Nominal Isabelle
|
1607
|
27 |
derives automatically a reasoning infrastructure that has been used
|
1550
|
28 |
successfully in formalisations of an equivalence checking algorithm for LF
|
|
29 |
\cite{UrbanCheneyBerghofer08}, Typed
|
1520
|
30 |
Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
|
|
31 |
\cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result
|
|
32 |
for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
|
|
33 |
used by Pollack for formalisations in the locally-nameless approach to
|
|
34 |
binding \cite{SatoPollack10}.
|
|
35 |
|
1535
|
36 |
However, Nominal Isabelle has fared less well in a formalisation of
|
1524
|
37 |
the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
|
|
38 |
are of the form
|
1570
|
39 |
%
|
|
40 |
\begin{equation}\label{tysch}
|
|
41 |
\begin{array}{l}
|
|
42 |
T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T
|
|
43 |
\end{array}
|
|
44 |
\end{equation}
|
1520
|
45 |
|
|
46 |
\noindent
|
1566
|
47 |
and the quantification $\forall$ binds a finite (possibly empty) set of
|
1550
|
48 |
type-variables. While it is possible to implement this kind of more general
|
|
49 |
binders by iterating single binders, this leads to a rather clumsy
|
|
50 |
formalisation of W. The need of iterating single binders is also one reason
|
|
51 |
why Nominal Isabelle and similar theorem provers that only provide
|
|
52 |
mechanisms for binding single variables have not fared extremely well with the
|
|
53 |
more advanced tasks in the POPLmark challenge \cite{challenge05}, because
|
|
54 |
also there one would like to bind multiple variables at once.
|
1520
|
55 |
|
1577
|
56 |
Binding multiple variables has interesting properties that cannot be captured
|
1587
|
57 |
easily by iterating single binders. For example in case of type-schemes we do not
|
|
58 |
want to make a distinction about the order of the bound variables. Therefore
|
1550
|
59 |
we would like to regard the following two type-schemes as alpha-equivalent
|
1572
|
60 |
%
|
|
61 |
\begin{equation}\label{ex1}
|
|
62 |
\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x
|
|
63 |
\end{equation}
|
1520
|
64 |
|
|
65 |
\noindent
|
1587
|
66 |
but assuming that $x$, $y$ and $z$ are distinct variables,
|
|
67 |
the following two should \emph{not} be alpha-equivalent
|
1572
|
68 |
%
|
|
69 |
\begin{equation}\label{ex2}
|
|
70 |
\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z
|
|
71 |
\end{equation}
|
1520
|
72 |
|
|
73 |
\noindent
|
1587
|
74 |
Moreover, we like to regard type-schemes as
|
1524
|
75 |
alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
|
1572
|
76 |
%
|
|
77 |
\begin{equation}\label{ex3}
|
|
78 |
\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y
|
|
79 |
\end{equation}
|
1485
|
80 |
|
1520
|
81 |
\noindent
|
1535
|
82 |
where $z$ does not occur freely in the type.
|
1545
|
83 |
In this paper we will give a general binding mechanism and associated
|
1524
|
84 |
notion of alpha-equivalence that can be used to faithfully represent
|
1545
|
85 |
this kind of binding in Nominal Isabelle. The difficulty of finding the right notion
|
1607
|
86 |
for alpha-equivalence can be appreciated in this case by considering that the
|
1524
|
87 |
definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
|
|
88 |
|
1520
|
89 |
However, the notion of alpha-equivalence that is preserved by vacuous binders is not
|
1566
|
90 |
always wanted. For example in terms like
|
1587
|
91 |
%
|
1535
|
92 |
\begin{equation}\label{one}
|
1550
|
93 |
\LET x = 3 \AND y = 2 \IN x\,-\,y \END
|
1535
|
94 |
\end{equation}
|
1520
|
95 |
|
|
96 |
\noindent
|
1524
|
97 |
we might not care in which order the assignments $x = 3$ and $y = 2$ are
|
1535
|
98 |
given, but it would be unusual to regard \eqref{one} as alpha-equivalent
|
1524
|
99 |
with
|
1587
|
100 |
%
|
1520
|
101 |
\begin{center}
|
1550
|
102 |
$\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$
|
1520
|
103 |
\end{center}
|
|
104 |
|
|
105 |
\noindent
|
1550
|
106 |
Therefore we will also provide a separate binding mechanism for cases in
|
|
107 |
which the order of binders does not matter, but the ``cardinality'' of the
|
1535
|
108 |
binders has to agree.
|
1520
|
109 |
|
1550
|
110 |
However, we found that this is still not sufficient for dealing with
|
|
111 |
language constructs frequently occurring in programming language
|
|
112 |
research. For example in $\mathtt{let}$s containing patterns
|
1587
|
113 |
%
|
1535
|
114 |
\begin{equation}\label{two}
|
1550
|
115 |
\LET (x, y) = (3, 2) \IN x\,-\,y \END
|
1535
|
116 |
\end{equation}
|
1520
|
117 |
|
|
118 |
\noindent
|
1535
|
119 |
we want to bind all variables from the pattern inside the body of the
|
|
120 |
$\mathtt{let}$, but we also care about the order of these variables, since
|
1566
|
121 |
we do not want to regard \eqref{two} as alpha-equivalent with
|
1587
|
122 |
%
|
1520
|
123 |
\begin{center}
|
1550
|
124 |
$\LET (y, x) = (3, 2) \IN x\,- y\,\END$
|
1520
|
125 |
\end{center}
|
|
126 |
|
|
127 |
\noindent
|
1545
|
128 |
As a result, we provide three general binding mechanisms each of which binds multiple
|
1566
|
129 |
variables at once, and let the user chose which one is intended when formalising a
|
1524
|
130 |
programming language calculus.
|
1485
|
131 |
|
1545
|
132 |
By providing these general binding mechanisms, however, we have to work around
|
1524
|
133 |
a problem that has been pointed out by Pottier in \cite{Pottier06}: in
|
|
134 |
$\mathtt{let}$-constructs of the form
|
1587
|
135 |
%
|
1520
|
136 |
\begin{center}
|
|
137 |
$\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
|
|
138 |
\end{center}
|
|
139 |
|
|
140 |
\noindent
|
1524
|
141 |
which bind all the $x_i$ in $s$, we might not care about the order in
|
1520
|
142 |
which the $x_i = t_i$ are given, but we do care about the information that there are
|
1524
|
143 |
as many $x_i$ as there are $t_i$. We lose this information if we represent the
|
1550
|
144 |
$\mathtt{let}$-constructor by something like
|
1587
|
145 |
%
|
1523
|
146 |
\begin{center}
|
1524
|
147 |
$\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
|
1523
|
148 |
\end{center}
|
1520
|
149 |
|
1523
|
150 |
\noindent
|
1566
|
151 |
where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound
|
|
152 |
in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}
|
|
153 |
would be a perfectly legal instance. To exclude such terms an additional
|
|
154 |
predicate about well-formed terms is needed in order to ensure that the two
|
|
155 |
lists are of equal length. This can result into very messy reasoning (see
|
1577
|
156 |
for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications
|
1566
|
157 |
for $\mathtt{let}$s as follows
|
1587
|
158 |
%
|
1528
|
159 |
\begin{center}
|
|
160 |
\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
|
1570
|
161 |
$trm$ & $::=$ & \ldots\\
|
1545
|
162 |
& $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm]
|
1570
|
163 |
$assn$ & $::=$ & $\mathtt{anil}$\\
|
1528
|
164 |
& $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$
|
|
165 |
\end{tabular}
|
|
166 |
\end{center}
|
|
167 |
|
|
168 |
\noindent
|
1577
|
169 |
where $assn$ is an auxiliary type representing a list of assignments
|
1545
|
170 |
and $bn$ an auxiliary function identifying the variables to be bound by
|
1566
|
171 |
the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows
|
1528
|
172 |
|
|
173 |
\begin{center}
|
|
174 |
$bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$
|
|
175 |
\end{center}
|
1523
|
176 |
|
1528
|
177 |
\noindent
|
1550
|
178 |
The scope of the binding is indicated by labels given to the types, for
|
|
179 |
example \mbox{$s\!::\!trm$}, and a binding clause, in this case
|
1577
|
180 |
$\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the
|
1607
|
181 |
function call $bn\,(a)$ returns. This style of specifying terms and bindings is
|
1577
|
182 |
heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}.
|
1528
|
183 |
|
1545
|
184 |
However, we will not be able to deal with all specifications that are
|
1570
|
185 |
allowed by Ott. One reason is that Ott allows ``empty'' specifications
|
|
186 |
like
|
|
187 |
|
|
188 |
\begin{center}
|
|
189 |
$t ::= t\;t \mid \lambda x. t$
|
|
190 |
\end{center}
|
|
191 |
|
|
192 |
\noindent
|
1577
|
193 |
where no clause for variables is given. Such specifications make some sense in
|
1607
|
194 |
the context of Coq's type theory (which Ott supports), but not at all in a HOL-based
|
|
195 |
environment where every datatype must have a non-empty set-theoretic model.
|
1570
|
196 |
|
|
197 |
Another reason is that we establish the reasoning infrastructure
|
|
198 |
for alpha-\emph{equated} terms. In contrast, Ott produces a reasoning
|
|
199 |
infrastructure in Isabelle/HOL for
|
1545
|
200 |
\emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
|
1556
|
201 |
and the raw terms produced by Ott use names for bound variables,
|
1545
|
202 |
there is a key difference: working with alpha-equated terms means that the
|
|
203 |
two type-schemes with $x$, $y$ and $z$ being distinct
|
1528
|
204 |
|
|
205 |
\begin{center}
|
|
206 |
$\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$
|
|
207 |
\end{center}
|
|
208 |
|
|
209 |
\noindent
|
1550
|
210 |
are not just alpha-equal, but actually equal. As a
|
|
211 |
result, we can only support specifications that make sense on the level of
|
|
212 |
alpha-equated terms (offending specifications, which for example bind a variable
|
1556
|
213 |
according to a variable bound somewhere else, are not excluded by Ott, but we
|
|
214 |
have to). Our
|
1550
|
215 |
insistence on reasoning with alpha-equated terms comes from the wealth of
|
|
216 |
experience we gained with the older version of Nominal Isabelle: for
|
|
217 |
non-trivial properties, reasoning about alpha-equated terms is much easier
|
1556
|
218 |
than reasoning with raw terms. The fundamental reason for this is that the
|
1550
|
219 |
HOL-logic underlying Nominal Isabelle allows us to replace
|
|
220 |
``equals-by-equals''. In contrast replacing ``alpha-equals-by-alpha-equals''
|
|
221 |
in a representation based on raw terms requires a lot of extra reasoning work.
|
1535
|
222 |
|
|
223 |
Although in informal settings a reasoning infrastructure for alpha-equated
|
1607
|
224 |
terms is nearly always taken for granted, establishing
|
1550
|
225 |
it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task.
|
1535
|
226 |
For every specification we will need to construct a type containing as
|
1556
|
227 |
elements the alpha-equated terms. To do so, we use
|
1535
|
228 |
the standard HOL-technique of defining a new type by
|
1556
|
229 |
identifying a non-empty subset of an existing type. The construction we
|
1607
|
230 |
perform in HOL can be illustrated by the following picture:
|
1545
|
231 |
|
1528
|
232 |
\begin{center}
|
1552
|
233 |
\begin{tikzpicture}
|
|
234 |
%\draw[step=2mm] (-4,-1) grid (4,1);
|
|
235 |
|
|
236 |
\draw[very thick] (0.7,0.4) circle (4.25mm);
|
|
237 |
\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);
|
|
238 |
\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);
|
|
239 |
|
|
240 |
\draw (-2.0, 0.845) -- (0.7,0.845);
|
|
241 |
\draw (-2.0,-0.045) -- (0.7,-0.045);
|
|
242 |
|
|
243 |
\draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
|
|
244 |
\draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
|
|
245 |
\draw (1.8, 0.48) node[right=-0.1mm]
|
|
246 |
{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
|
|
247 |
\draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
|
|
248 |
\draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
|
|
249 |
|
|
250 |
\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
|
|
251 |
\draw (-0.95, 0.3) node[above=0mm] {isomorphism};
|
|
252 |
|
|
253 |
\end{tikzpicture}
|
1528
|
254 |
\end{center}
|
|
255 |
|
|
256 |
\noindent
|
1577
|
257 |
We take as the starting point a definition of raw terms (defined as a
|
1556
|
258 |
datatype in Isabelle/HOL); identify then the
|
1607
|
259 |
alpha-equivalence classes in the type of sets of raw terms according to our
|
1556
|
260 |
alpha-equivalence relation and finally define the new type as these
|
|
261 |
alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are
|
1607
|
262 |
definable as datatype in Isabelle/HOL and the fact that our relation for
|
|
263 |
alpha-equivalence is indeed an equivalence relation).
|
1556
|
264 |
|
1607
|
265 |
The fact that we obtain an isomorphism between the new type and the non-empty
|
1556
|
266 |
subset shows that the new type is a faithful representation of alpha-equated terms.
|
1577
|
267 |
That is not the case for example in the representation of terms using the locally
|
1607
|
268 |
nameless representation of binders \cite{McKinnaPollack99}: in this representation
|
|
269 |
there are ``junk'' terms that need to
|
1556
|
270 |
be excluded by reasoning about a well-formedness predicate.
|
|
271 |
|
1577
|
272 |
The problem with introducing a new type in Isabelle/HOL is that in order to be useful,
|
1572
|
273 |
a reasoning infrastructure needs to be ``lifted'' from the underlying subset to
|
1607
|
274 |
the new type. This is usually a tricky and arduous task. To ease it,
|
1577
|
275 |
we re-implemented in Isabelle/HOL the quotient package described by Homeier
|
|
276 |
\cite{Homeier05}. This package
|
|
277 |
allows us to lift definitions and theorems involving raw terms
|
1607
|
278 |
to definitions and theorems involving alpha-equated, terms. For example
|
1577
|
279 |
if we define the free-variable function over lambda terms
|
|
280 |
|
|
281 |
\begin{center}
|
|
282 |
$\fv(x) = \{x\}$\hspace{10mm}
|
|
283 |
$\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm]
|
|
284 |
$\fv(\lambda x.t) = \fv(t) - \{x\}$
|
|
285 |
\end{center}
|
|
286 |
|
|
287 |
\noindent
|
|
288 |
then with not too great effort we obtain a function $\fv_\alpha$
|
|
289 |
operating on quotients, or alpha-equivalence classes of terms, as follows
|
|
290 |
|
|
291 |
\begin{center}
|
|
292 |
$\fv_\alpha(x) = \{x\}$\hspace{10mm}
|
|
293 |
$\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm]
|
|
294 |
$\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$
|
|
295 |
\end{center}
|
|
296 |
|
|
297 |
\noindent
|
|
298 |
(Note that this means also the term-constructors for variables, applications
|
|
299 |
and lambda are lifted to the quotient level.) This construction, of course,
|
1607
|
300 |
only works if alpha-equivalence is an equivalence relation, and the
|
|
301 |
definitions and theorems are respectful w.r.t.~alpha-equivalence. Hence we
|
|
302 |
will not be able to lift a bound-variable function to alpha-equated terms
|
|
303 |
(since it does not respect alpha-equivalence). To sum up, every lifting of
|
|
304 |
theorems to the quotient level needs proofs of some respectfulness
|
|
305 |
properties. In the paper we show that we are able to automate these
|
|
306 |
proofs and therefore can establish a reasoning infrastructure for
|
|
307 |
alpha-equated terms.\medskip
|
1577
|
308 |
|
1506
|
309 |
|
1528
|
310 |
\noindent
|
|
311 |
{\bf Contributions:} We provide new definitions for when terms
|
|
312 |
involving multiple binders are alpha-equivalent. These definitions are
|
1607
|
313 |
inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
|
1528
|
314 |
proofs, we establish a reasoning infrastructure for alpha-equated
|
|
315 |
terms, including properties about support, freshness and equality
|
1607
|
316 |
conditions for alpha-equated terms. We are also able to derive, at the moment
|
|
317 |
only manually, strong induction principles that
|
|
318 |
have the variable convention already built in.
|
1485
|
319 |
*}
|
|
320 |
|
1493
|
321 |
section {* A Short Review of the Nominal Logic Work *}
|
|
322 |
|
|
323 |
text {*
|
1556
|
324 |
At its core, Nominal Isabelle is an adaption of the nominal logic work by
|
|
325 |
Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
326 |
\cite{HuffmanUrban10}, which we review here briefly to aid the description
|
1556
|
327 |
of what follows. Two central notions in the nominal logic work are sorted
|
1570
|
328 |
atoms and sort-respecting permutations of atoms. The sorts can be used to
|
|
329 |
represent different kinds of variables, such as term- and type-variables in
|
|
330 |
Core-Haskell, and it is assumed that there is an infinite supply of atoms
|
|
331 |
for each sort. However, in order to simplify the description, we shall
|
|
332 |
assume in what follows that there is only a single sort of atoms.
|
1556
|
333 |
|
1493
|
334 |
|
|
335 |
Permutations are bijective functions from atoms to atoms that are
|
|
336 |
the identity everywhere except on a finite number of atoms. There is a
|
|
337 |
two-place permutation operation written
|
|
338 |
|
1506
|
339 |
@{text[display,indent=5] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
|
1493
|
340 |
|
|
341 |
\noindent
|
|
342 |
with a generic type in which @{text "\<alpha>"} stands for the type of atoms
|
1570
|
343 |
and @{text "\<beta>"} for the type of the object on which the permutation
|
1493
|
344 |
acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"},
|
|
345 |
the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}
|
1570
|
346 |
and the inverse permutation of @{term p} as @{text "- p"}. The permutation
|
1493
|
347 |
operation is defined for products, lists, sets, functions, booleans etc
|
|
348 |
(see \cite{HuffmanUrban10}).
|
|
349 |
|
1570
|
350 |
The most original aspect of the nominal logic work of Pitts is a general
|
|
351 |
definition for the notion of ``the set of free variables of an object @{text
|
|
352 |
"x"}''. This notion, written @{term "supp x"}, is general in the sense that
|
|
353 |
it applies not only to lambda-terms alpha-equated or not, but also to lists,
|
|
354 |
products, sets and even functions. The definition depends only on the
|
|
355 |
permutation operation and on the notion of equality defined for the type of
|
|
356 |
@{text x}, namely:
|
1493
|
357 |
|
1506
|
358 |
@{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}
|
1493
|
359 |
|
|
360 |
\noindent
|
|
361 |
There is also the derived notion for when an atom @{text a} is \emph{fresh}
|
|
362 |
for an @{text x}, defined as
|
|
363 |
|
1506
|
364 |
@{thm[display,indent=5] fresh_def[no_vars]}
|
1493
|
365 |
|
|
366 |
\noindent
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
367 |
We also use for sets of atoms the abbreviation
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
368 |
@{thm (lhs) fresh_star_def[no_vars]} defined as
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
369 |
@{thm (rhs) fresh_star_def[no_vars]}.
|
1493
|
370 |
A striking consequence of these definitions is that we can prove
|
|
371 |
without knowing anything about the structure of @{term x} that
|
|
372 |
swapping two fresh atoms, say @{text a} and @{text b}, leave
|
1506
|
373 |
@{text x} unchanged.
|
|
374 |
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
375 |
\begin{property}
|
1506
|
376 |
@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
377 |
\end{property}
|
1506
|
378 |
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
379 |
\noindent
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
380 |
For a proof see \cite{HuffmanUrban10}.
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
381 |
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
382 |
\begin{property}
|
1506
|
383 |
@{thm[mode=IfThen] at_set_avoiding[no_vars]}
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
384 |
\end{property}
|
1493
|
385 |
|
|
386 |
*}
|
|
387 |
|
1485
|
388 |
|
1556
|
389 |
section {* General Binders *}
|
1485
|
390 |
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
391 |
text {*
|
1587
|
392 |
In Nominal Isabelle, the user is expected to write down a specification of a
|
|
393 |
term-calculus and then a reasoning infrastructure is automatically derived
|
1579
|
394 |
from this specifcation (remember that Nominal Isabelle is a definitional
|
1587
|
395 |
extension of Isabelle/HOL, which does not introduce any new axioms).
|
1579
|
396 |
|
1556
|
397 |
|
1579
|
398 |
In order to keep our work manageable, we will wherever possible state
|
|
399 |
definitions and perform proofs inside Isabelle, as opposed to write custom
|
|
400 |
ML-code that generates them for each instance of a term-calculus. To that
|
|
401 |
end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.
|
|
402 |
These pairs are intended to represent the abstraction, or binding, of the set $as$
|
|
403 |
in the body $x$.
|
1570
|
404 |
|
1579
|
405 |
The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are
|
|
406 |
alpha-equivalent? (At the moment we are interested in
|
1570
|
407 |
the notion of alpha-equivalence that is \emph{not} preserved by adding
|
1579
|
408 |
vacuous binders.) To answer this, we identify four conditions: {\it i)} given
|
|
409 |
a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
|
1572
|
410 |
need to have the same set of free variables; moreover there must be a permutation,
|
1579
|
411 |
$p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged,
|
|
412 |
but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation,
|
1572
|
413 |
say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes
|
1579
|
414 |
the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can
|
|
415 |
be stated formally as follows:
|
1556
|
416 |
%
|
1572
|
417 |
\begin{equation}\label{alphaset}
|
|
418 |
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
|
1579
|
419 |
\multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
|
1572
|
420 |
& @{text "fv(x) - as = fv(y) - bs"}\\
|
|
421 |
\wedge & @{text "fv(x) - as #* p"}\\
|
|
422 |
\wedge & @{text "(p \<bullet> x) R y"}\\
|
|
423 |
\wedge & @{text "(p \<bullet> as) = bs"}\\
|
|
424 |
\end{array}
|
1556
|
425 |
\end{equation}
|
|
426 |
|
|
427 |
\noindent
|
1579
|
428 |
Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where
|
|
429 |
we existentially quantify over this $p$.
|
|
430 |
Also note that the relation is dependent on a free-variable function $\fv$ and a relation
|
|
431 |
$R$. The reason for this extra generality is that we will use $\approx_{set}$ for both
|
|
432 |
``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by
|
|
433 |
equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support
|
|
434 |
of $x$ and $y$. To have these parameters means, however, we can derive properties about
|
|
435 |
them generically.
|
1572
|
436 |
|
|
437 |
The definition in \eqref{alphaset} does not make any distinction between the
|
1579
|
438 |
order of abstracted variables. If we want this, then we can define alpha-equivalence
|
|
439 |
for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
|
|
440 |
as follows
|
1572
|
441 |
%
|
|
442 |
\begin{equation}\label{alphalist}
|
|
443 |
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
|
1579
|
444 |
\multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
|
1572
|
445 |
& @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
|
|
446 |
\wedge & @{text "fv(x) - (set as) #* p"}\\
|
|
447 |
\wedge & @{text "(p \<bullet> x) R y"}\\
|
|
448 |
\wedge & @{text "(p \<bullet> as) = bs"}\\
|
|
449 |
\end{array}
|
|
450 |
\end{equation}
|
|
451 |
|
|
452 |
\noindent
|
|
453 |
where $set$ is just the function that coerces a list of atoms into a set of atoms.
|
1556
|
454 |
|
1572
|
455 |
If we do not want to make any difference between the order of binders and
|
1579
|
456 |
also allow vacuous binders, then we keep sets of binders, but drop the fourth
|
|
457 |
condition in \eqref{alphaset}:
|
1572
|
458 |
%
|
1579
|
459 |
\begin{equation}\label{alphares}
|
1572
|
460 |
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
|
1579
|
461 |
\multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
|
1572
|
462 |
& @{text "fv(x) - as = fv(y) - bs"}\\
|
|
463 |
\wedge & @{text "fv(x) - as #* p"}\\
|
|
464 |
\wedge & @{text "(p \<bullet> x) R y"}\\
|
|
465 |
\end{array}
|
|
466 |
\end{equation}
|
1556
|
467 |
|
1579
|
468 |
\begin{exmple}\rm
|
|
469 |
It might be useful to consider some examples for how these definitions pan out in practise.
|
|
470 |
For this consider the case of abstracting a set of variables over types (as in type-schemes).
|
|
471 |
We set $R$ to be the equality and for $\fv(T)$ we define
|
1572
|
472 |
|
|
473 |
\begin{center}
|
|
474 |
$\fv(x) = \{x\} \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$
|
|
475 |
\end{center}
|
|
476 |
|
|
477 |
\noindent
|
1579
|
478 |
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily
|
|
479 |
checked that @{text "({x, y}, x \<rightarrow> y)"} and
|
|
480 |
@{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to
|
|
481 |
be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"} then
|
|
482 |
$([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that
|
|
483 |
makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the
|
|
484 |
type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that
|
|
485 |
$(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation.
|
|
486 |
However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
|
|
487 |
the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).
|
|
488 |
\end{exmple}
|
|
489 |
|
|
490 |
\noindent
|
|
491 |
Let $\star$ range over $\{set, res, list\}$. We prove next under which
|
|
492 |
conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence
|
|
493 |
relations and equivariant:
|
|
494 |
|
|
495 |
\begin{lemma}
|
|
496 |
{\it i)} Given the fact that $x\;R\;x$ holds, then
|
|
497 |
$(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given
|
|
498 |
that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then
|
|
499 |
$(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies
|
|
500 |
$(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given
|
|
501 |
that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies
|
|
502 |
@{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$
|
|
503 |
and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies
|
|
504 |
$(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given
|
|
505 |
@{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and
|
|
506 |
@{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then
|
|
507 |
$(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies
|
|
508 |
$(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star
|
|
509 |
(p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.
|
|
510 |
\end{lemma}
|
|
511 |
|
|
512 |
\begin{proof}
|
|
513 |
All properties are by unfolding the definitions and simple calculations.
|
|
514 |
\end{proof}
|
1587
|
515 |
|
|
516 |
|
|
517 |
\begin{lemma}
|
|
518 |
$supp ([as]set. x) = supp x - as$
|
|
519 |
\end{lemma}
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
520 |
*}
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
521 |
|
1491
|
522 |
section {* Alpha-Equivalence and Free Variables *}
|
|
523 |
|
1520
|
524 |
text {*
|
1611
|
525 |
The syntax of a specification for a term-calculus in Nominal Isabelle is
|
|
526 |
heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a
|
|
527 |
collection of (possibly mutual recursive) type declarations, say
|
|
528 |
$ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a
|
|
529 |
collection of associated binding function declarations, say
|
1613
|
530 |
$bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically
|
|
531 |
written as follows:
|
1587
|
532 |
|
|
533 |
\begin{center}
|
1611
|
534 |
\begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
|
|
535 |
types \mbox{declaration part} &
|
|
536 |
$\begin{cases}
|
|
537 |
\mbox{\begin{tabular}{l}
|
|
538 |
\isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\
|
|
539 |
\isacommand{and} $ty_{\alpha{}2} = \ldots$\\
|
1587
|
540 |
$\ldots$\\
|
1611
|
541 |
\isacommand{and} $ty_{\alpha{}n} = \ldots$\\
|
|
542 |
\end{tabular}}
|
|
543 |
\end{cases}$\\
|
|
544 |
binding \mbox{functions part} &
|
|
545 |
$\begin{cases}
|
|
546 |
\mbox{\begin{tabular}{l}
|
|
547 |
\isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$
|
1587
|
548 |
$\ldots$\\
|
1611
|
549 |
\isacommand{where}\\
|
1587
|
550 |
$\ldots$\\
|
1611
|
551 |
\end{tabular}}
|
|
552 |
\end{cases}$\\
|
1587
|
553 |
\end{tabular}
|
|
554 |
\end{center}
|
|
555 |
|
|
556 |
\noindent
|
1611
|
557 |
Each type declaration $ty_{\alpha{}i}$ consists of a collection of
|
|
558 |
term-constructors, each of which comes with a list of labelled
|
|
559 |
types that indicate the types of the arguments of the term-constructor,
|
|
560 |
like
|
|
561 |
|
|
562 |
\begin{center}
|
|
563 |
$C_\alpha\;label_1\!::\!ty'_1\;\ldots label_j\!::\!ty'_j\;\;\textit{binding\_clauses}$
|
|
564 |
\end{center}
|
1587
|
565 |
|
1611
|
566 |
\noindent
|
|
567 |
The labels are optional and can be used in the (possibly empty) list of binding clauses.
|
|
568 |
These clauses indicate the binders and the scope of the binders in a term-constructor. They
|
|
569 |
are of the form
|
1587
|
570 |
|
1611
|
571 |
\begin{center}
|
|
572 |
\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}
|
|
573 |
\end{center}
|
|
574 |
|
|
575 |
\noindent
|
|
576 |
whereby we distinguish between \emph{shallow} binders and \emph{deep} binders.
|
|
577 |
Shallow binders are just of the form \isacommand{bind}\; {\it label}\;
|
|
578 |
\isacommand{in}\; {\it another\_label}. The only restriction on shallow binders
|
|
579 |
is that the {\it label} must refer to either a type which is single atom or
|
|
580 |
to a type which is a finite set of atoms. For example the specification of
|
|
581 |
lambda-terms and type-schemes use them:
|
|
582 |
|
|
583 |
\begin{center}
|
1612
|
584 |
\begin{tabular}{@ {}cc@ {}}
|
|
585 |
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
|
|
586 |
\isacommand{nominal\_datatype} {\it lam} =\\
|
|
587 |
\hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
|
|
588 |
\hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
|
|
589 |
\hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
|
|
590 |
\hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
|
1611
|
591 |
\end{tabular} &
|
1612
|
592 |
\begin{tabular}{@ {}l@ {}}
|
|
593 |
\isacommand{nominal\_datatype} {\it ty} =\\
|
|
594 |
\hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
|
|
595 |
\hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
|
|
596 |
\isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
|
|
597 |
\hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\
|
1611
|
598 |
\end{tabular}
|
|
599 |
\end{tabular}
|
|
600 |
\end{center}
|
1587
|
601 |
|
1612
|
602 |
\noindent
|
1587
|
603 |
A specification of a term-calculus in Nominal Isabell is very similar to
|
|
604 |
the usual datatype definition of Isabelle/HOL:
|
|
605 |
|
|
606 |
|
|
607 |
Because of the problem Pottier pointed out in \cite{Pottier06}, the general
|
|
608 |
binders from the previous section cannot be used directly to represent w
|
|
609 |
be used directly
|
|
610 |
*}
|
|
611 |
|
|
612 |
|
|
613 |
|
|
614 |
text {*
|
1520
|
615 |
Restrictions
|
|
616 |
|
|
617 |
\begin{itemize}
|
1572
|
618 |
\item non-emptiness
|
1520
|
619 |
\item positive datatype definitions
|
|
620 |
\item finitely supported abstractions
|
|
621 |
\item respectfulness of the bn-functions\bigskip
|
|
622 |
\item binders can only have a ``single scope''
|
1577
|
623 |
\item all bindings must have the same mode
|
1520
|
624 |
\end{itemize}
|
|
625 |
*}
|
|
626 |
|
1493
|
627 |
section {* Examples *}
|
1485
|
628 |
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
629 |
section {* Adequacy *}
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
630 |
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
631 |
section {* Related Work *}
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
632 |
|
1570
|
633 |
text {*
|
|
634 |
Ott is better with list dot specifications; subgrammars
|
|
635 |
|
|
636 |
untyped;
|
|
637 |
|
|
638 |
*}
|
|
639 |
|
|
640 |
|
1493
|
641 |
section {* Conclusion *}
|
1485
|
642 |
|
|
643 |
text {*
|
1520
|
644 |
Complication when the single scopedness restriction is lifted (two
|
|
645 |
overlapping permutations)
|
|
646 |
*}
|
|
647 |
|
|
648 |
text {*
|
1493
|
649 |
|
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
650 |
TODO: function definitions:
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
651 |
\medskip
|
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
652 |
|
1493
|
653 |
\noindent
|
1528
|
654 |
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
|
1506
|
655 |
many discussions about Nominal Isabelle. We thank Peter Sewell for
|
|
656 |
making the informal notes \cite{SewellBestiary} available to us and
|
1556
|
657 |
also for patiently explaining some of the finer points about the abstract
|
1545
|
658 |
definitions and about the implementation of the Ott-tool.
|
1485
|
659 |
|
1577
|
660 |
Lookup: Merlin paper by James Cheney; Mark Shinwell PhD
|
754
|
661 |
|
1577
|
662 |
Future work: distinct list abstraction
|
|
663 |
|
|
664 |
|
754
|
665 |
*}
|
|
666 |
|
1484
|
667 |
|
|
668 |
|
754
|
669 |
(*<*)
|
|
670 |
end
|
|
671 |
(*>*) |