754
+ − 1
(*<*)
+ − 2
theory Paper
2465
+ − 3
imports "../Nominal/Nominal2" "LaTeXsugar"
754
+ − 4
begin
1493
+ − 5
1657
+ − 6
consts
+ − 7
fv :: "'a \<Rightarrow> 'b"
1728
+ − 8
abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
+ − 9
alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1763
+ − 10
abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"
1796
5165c350ee1a
clarified comment about distinct lists in th efuture work section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 11
Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
2163
+ − 12
Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
1657
+ − 13
+ − 14
definition
+ − 15
"equal \<equiv> (op =)"
+ − 16
1493
+ − 17
notation (latex output)
+ − 18
swap ("'(_ _')" [1000, 1000] 1000) and
+ − 19
fresh ("_ # _" [51, 51] 50) and
1694
+ − 20
fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
1493
+ − 21
supp ("supp _" [78] 73) and
+ − 22
uminus ("-_" [78] 73) and
1657
+ − 23
If ("if _ then _ else _" 10) and
2471
+ − 24
alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
2341
+ − 25
alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ − 26
alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
1657
+ − 27
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
1763
+ − 28
abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and
2347
+ − 29
fv ("fa'(_')" [100] 100) and
1657
+ − 30
equal ("=") and
2471
+ − 31
alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
+ − 32
Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
2331
+ − 33
Abs_lst ("[_]\<^bsub>list\<^esub>._") and
+ − 34
Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
+ − 35
Abs_res ("[_]\<^bsub>res\<^esub>._") and
+ − 36
Abs_print ("_\<^bsub>set\<^esub>._") and
1703
+ − 37
Cons ("_::_" [78,77] 73) and
2471
+ − 38
supp_set ("aux _" [1000] 10) and
1728
+ − 39
alpha_bn ("_ \<approx>bn _")
2359
+ − 40
+ − 41
consts alpha_trm ::'a
+ − 42
consts fa_trm :: 'a
+ − 43
consts alpha_trm2 ::'a
+ − 44
consts fa_trm2 :: 'a
+ − 45
consts ast :: 'a
+ − 46
consts ast' :: 'a
+ − 47
notation (latex output)
+ − 48
alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
+ − 49
fa_trm ("fa\<^bsub>trm\<^esub>") and
+ − 50
alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
+ − 51
fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
+ − 52
ast ("'(as, t')") and
+ − 53
ast' ("'(as', t\<PRIME> ')")
+ − 54
754
+ − 55
(*>*)
+ − 56
1657
+ − 57
754
+ − 58
section {* Introduction *}
+ − 59
+ − 60
text {*
1739
+ − 61
2345
+ − 62
So far, Nominal Isabelle provided a mechanism for constructing
2343
+ − 63
$\alpha$-equated terms, for example lambda-terms
1485
+ − 64
1520
+ − 65
\begin{center}
1657
+ − 66
@{text "t ::= x | t t | \<lambda>x. t"}
1520
+ − 67
\end{center}
+ − 68
+ − 69
\noindent
2341
+ − 70
where free and bound variables have names. For such $\alpha$-equated terms,
2163
+ − 71
Nominal Isabelle derives automatically a reasoning infrastructure that has
+ − 72
been used successfully in formalisations of an equivalence checking
+ − 73
algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
1520
+ − 74
Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
2163
+ − 75
\cite{BengtsonParow09} and a strong normalisation result for cut-elimination
+ − 76
in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for
+ − 77
formalisations in the locally-nameless approach to binding
+ − 78
\cite{SatoPollack10}.
1520
+ − 79
1535
+ − 80
However, Nominal Isabelle has fared less well in a formalisation of
1690
+ − 81
the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are,
+ − 82
respectively, of the form
1570
+ − 83
%
+ − 84
\begin{equation}\label{tysch}
+ − 85
\begin{array}{l}
1657
+ − 86
@{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}
+ − 87
@{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
1570
+ − 88
\end{array}
+ − 89
\end{equation}
1520
+ − 90
+ − 91
\noindent
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 92
and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
1550
+ − 93
type-variables. While it is possible to implement this kind of more general
+ − 94
binders by iterating single binders, this leads to a rather clumsy
+ − 95
formalisation of W. The need of iterating single binders is also one reason
+ − 96
why Nominal Isabelle and similar theorem provers that only provide
+ − 97
mechanisms for binding single variables have not fared extremely well with the
+ − 98
more advanced tasks in the POPLmark challenge \cite{challenge05}, because
+ − 99
also there one would like to bind multiple variables at once.
1520
+ − 100
1577
+ − 101
Binding multiple variables has interesting properties that cannot be captured
2176
+ − 102
easily by iterating single binders. For example in the case of type-schemes we do not
1587
+ − 103
want to make a distinction about the order of the bound variables. Therefore
2341
+ − 104
we would like to regard the following two type-schemes as $\alpha$-equivalent
1572
+ − 105
%
+ − 106
\begin{equation}\label{ex1}
2346
+ − 107
@{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. x \<rightarrow> y"}
1572
+ − 108
\end{equation}
1520
+ − 109
+ − 110
\noindent
1657
+ − 111
but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
2341
+ − 112
the following two should \emph{not} be $\alpha$-equivalent
1572
+ − 113
%
+ − 114
\begin{equation}\label{ex2}
1667
+ − 115
@{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
1572
+ − 116
\end{equation}
1520
+ − 117
+ − 118
\noindent
2341
+ − 119
Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ
1657
+ − 120
only on \emph{vacuous} binders, such as
1572
+ − 121
%
+ − 122
\begin{equation}\label{ex3}
1667
+ − 123
@{text "\<forall>{x}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{x, z}. x \<rightarrow> y"}
1572
+ − 124
\end{equation}
1485
+ − 125
1520
+ − 126
\noindent
1657
+ − 127
where @{text z} does not occur freely in the type. In this paper we will
2341
+ − 128
give a general binding mechanism and associated notion of $\alpha$-equivalence
1657
+ − 129
that can be used to faithfully represent this kind of binding in Nominal
2341
+ − 130
Isabelle. The difficulty of finding the right notion for $\alpha$-equivalence
1657
+ − 131
can be appreciated in this case by considering that the definition given by
2331
+ − 132
Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
1524
+ − 133
2341
+ − 134
However, the notion of $\alpha$-equivalence that is preserved by vacuous
1657
+ − 135
binders is not always wanted. For example in terms like
1587
+ − 136
%
1535
+ − 137
\begin{equation}\label{one}
1657
+ − 138
@{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}
1535
+ − 139
\end{equation}
1520
+ − 140
+ − 141
\noindent
2341
+ − 142
we might not care in which order the assignments @{text "x = 3"} and
+ − 143
\mbox{@{text "y = 2"}} are given, but it would be unusual to regard
+ − 144
\eqref{one} as $\alpha$-equivalent with
1587
+ − 145
%
1520
+ − 146
\begin{center}
1657
+ − 147
@{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}
1520
+ − 148
\end{center}
+ − 149
+ − 150
\noindent
1550
+ − 151
Therefore we will also provide a separate binding mechanism for cases in
+ − 152
which the order of binders does not matter, but the ``cardinality'' of the
1535
+ − 153
binders has to agree.
1520
+ − 154
1550
+ − 155
However, we found that this is still not sufficient for dealing with
+ − 156
language constructs frequently occurring in programming language
1690
+ − 157
research. For example in @{text "\<LET>"}s containing patterns like
1587
+ − 158
%
1535
+ − 159
\begin{equation}\label{two}
1657
+ − 160
@{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}
1535
+ − 161
\end{equation}
1520
+ − 162
+ − 163
\noindent
1535
+ − 164
we want to bind all variables from the pattern inside the body of the
+ − 165
$\mathtt{let}$, but we also care about the order of these variables, since
2341
+ − 166
we do not want to regard \eqref{two} as $\alpha$-equivalent with
1587
+ − 167
%
1520
+ − 168
\begin{center}
1657
+ − 169
@{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
1520
+ − 170
\end{center}
2218
+ − 171
%
1520
+ − 172
\noindent
1657
+ − 173
As a result, we provide three general binding mechanisms each of which binds
+ − 174
multiple variables at once, and let the user chose which one is intended
1711
+ − 175
when formalising a term-calculus.
1485
+ − 176
1657
+ − 177
By providing these general binding mechanisms, however, we have to work
+ − 178
around a problem that has been pointed out by Pottier \cite{Pottier06} and
+ − 179
Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form
1587
+ − 180
%
1520
+ − 181
\begin{center}
1657
+ − 182
@{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}
1520
+ − 183
\end{center}
+ − 184
+ − 185
\noindent
1657
+ − 186
which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care
+ − 187
about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given,
+ − 188
but we do care about the information that there are as many @{text
+ − 189
"x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if
+ − 190
we represent the @{text "\<LET>"}-constructor by something like
1587
+ − 191
%
1523
+ − 192
\begin{center}
2341
+ − 193
@{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s) [t\<^isub>1,\<dots>,t\<^isub>n]"}
1523
+ − 194
\end{center}
1520
+ − 195
1523
+ − 196
\noindent
2341
+ − 197
where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text
+ − 198
"x\<^isub>i"} becomes bound in @{text s}. In this representation the term
+ − 199
\mbox{@{text "\<LET> (\<lambda>x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
+ − 200
instance, but the lengths of the two lists do not agree. To exclude such
+ − 201
terms, additional predicates about well-formed terms are needed in order to
+ − 202
ensure that the two lists are of equal length. This can result in very messy
+ − 203
reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will
+ − 204
allow type specifications for @{text "\<LET>"}s as follows
1587
+ − 205
%
1528
+ − 206
\begin{center}
+ − 207
\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
1657
+ − 208
@{text trm} & @{text "::="} & @{text "\<dots>"}\\
2341
+ − 209
& @{text "|"} & @{text "\<LET> as::assn s::trm"}\hspace{4mm}
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 210
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
1657
+ − 211
@{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
2341
+ − 212
& @{text "|"} & @{text "\<ACONS> name trm assn"}
1528
+ − 213
\end{tabular}
+ − 214
\end{center}
+ − 215
+ − 216
\noindent
1657
+ − 217
where @{text assn} is an auxiliary type representing a list of assignments
+ − 218
and @{text bn} an auxiliary function identifying the variables to be bound
1687
+ − 219
by the @{text "\<LET>"}. This function can be defined by recursion over @{text
1657
+ − 220
assn} as follows
1528
+ − 221
+ − 222
\begin{center}
1657
+ − 223
@{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm}
+ − 224
@{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"}
1528
+ − 225
\end{center}
1523
+ − 226
1528
+ − 227
\noindent
1550
+ − 228
The scope of the binding is indicated by labels given to the types, for
1657
+ − 229
example @{text "s::trm"}, and a binding clause, in this case
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 230
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
2346
+ − 231
clause states that all the names the function @{text
+ − 232
"bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily
2488
+ − 233
inspired by the syntax of the Ott-tool \cite{ott-jfp}. Though, Ott
+ − 234
has only one binding mode, namely the one where the order of
+ − 235
binders matters. Consequently, type-schemes with binding sets
+ − 236
of names cannot be modelled in Ott.
1657
+ − 237
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 238
However, we will not be able to cope with all specifications that are
2176
+ − 239
allowed by Ott. One reason is that Ott lets the user specify ``empty''
1617
+ − 240
types like
1570
+ − 241
+ − 242
\begin{center}
1657
+ − 243
@{text "t ::= t t | \<lambda>x. t"}
1570
+ − 244
\end{center}
+ − 245
+ − 246
\noindent
1617
+ − 247
where no clause for variables is given. Arguably, such specifications make
+ − 248
some sense in the context of Coq's type theory (which Ott supports), but not
+ − 249
at all in a HOL-based environment where every datatype must have a non-empty
1719
+ − 250
set-theoretic model \cite{Berghofer99}.
1570
+ − 251
+ − 252
Another reason is that we establish the reasoning infrastructure
2341
+ − 253
for $\alpha$-\emph{equated} terms. In contrast, Ott produces a reasoning
1570
+ − 254
infrastructure in Isabelle/HOL for
2341
+ − 255
\emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms
1556
+ − 256
and the raw terms produced by Ott use names for bound variables,
2341
+ − 257
there is a key difference: working with $\alpha$-equated terms means, for example,
1693
+ − 258
that the two type-schemes
1528
+ − 259
+ − 260
\begin{center}
1667
+ − 261
@{text "\<forall>{x}. x \<rightarrow> y = \<forall>{x, z}. x \<rightarrow> y"}
1528
+ − 262
\end{center}
+ − 263
+ − 264
\noindent
2341
+ − 265
are not just $\alpha$-equal, but actually \emph{equal}! As a result, we can
+ − 266
only support specifications that make sense on the level of $\alpha$-equated
1657
+ − 267
terms (offending specifications, which for example bind a variable according
+ − 268
to a variable bound somewhere else, are not excluded by Ott, but we have
1687
+ − 269
to).
+ − 270
2341
+ − 271
Our insistence on reasoning with $\alpha$-equated terms comes from the
1657
+ − 272
wealth of experience we gained with the older version of Nominal Isabelle:
2341
+ − 273
for non-trivial properties, reasoning with $\alpha$-equated terms is much
1657
+ − 274
easier than reasoning with raw terms. The fundamental reason for this is
+ − 275
that the HOL-logic underlying Nominal Isabelle allows us to replace
+ − 276
``equals-by-equals''. In contrast, replacing
2341
+ − 277
``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
1657
+ − 278
requires a lot of extra reasoning work.
1535
+ − 279
2341
+ − 280
Although in informal settings a reasoning infrastructure for $\alpha$-equated
1657
+ − 281
terms is nearly always taken for granted, establishing it automatically in
+ − 282
the Isabelle/HOL theorem prover is a rather non-trivial task. For every
+ − 283
specification we will need to construct a type containing as elements the
2341
+ − 284
$\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
1657
+ − 285
a new type by identifying a non-empty subset of an existing type. The
1667
+ − 286
construction we perform in Isabelle/HOL can be illustrated by the following picture:
1657
+ − 287
1528
+ − 288
\begin{center}
1552
+ − 289
\begin{tikzpicture}
+ − 290
%\draw[step=2mm] (-4,-1) grid (4,1);
+ − 291
+ − 292
\draw[very thick] (0.7,0.4) circle (4.25mm);
+ − 293
\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);
+ − 294
\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);
+ − 295
+ − 296
\draw (-2.0, 0.845) -- (0.7,0.845);
+ − 297
\draw (-2.0,-0.045) -- (0.7,-0.045);
+ − 298
+ − 299
\draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
+ − 300
\draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
+ − 301
\draw (1.8, 0.48) node[right=-0.1mm]
+ − 302
{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+ − 303
\draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+ − 304
\draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
+ − 305
+ − 306
\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
+ − 307
\draw (-0.95, 0.3) node[above=0mm] {isomorphism};
+ − 308
+ − 309
\end{tikzpicture}
1528
+ − 310
\end{center}
+ − 311
+ − 312
\noindent
1657
+ − 313
We take as the starting point a definition of raw terms (defined as a
2361
+ − 314
datatype in Isabelle/HOL); then identify the $\alpha$-equivalence classes in
2341
+ − 315
the type of sets of raw terms according to our $\alpha$-equivalence relation,
+ − 316
and finally define the new type as these $\alpha$-equivalence classes
1657
+ − 317
(non-emptiness is satisfied whenever the raw terms are definable as datatype
2341
+ − 318
in Isabelle/HOL and the property that our relation for $\alpha$-equivalence is
1657
+ − 319
indeed an equivalence relation).
1556
+ − 320
1657
+ − 321
The fact that we obtain an isomorphism between the new type and the
+ − 322
non-empty subset shows that the new type is a faithful representation of
2341
+ − 323
$\alpha$-equated terms. That is not the case for example for terms using the
1657
+ − 324
locally nameless representation of binders \cite{McKinnaPollack99}: in this
+ − 325
representation there are ``junk'' terms that need to be excluded by
+ − 326
reasoning about a well-formedness predicate.
1556
+ − 327
1657
+ − 328
The problem with introducing a new type in Isabelle/HOL is that in order to
+ − 329
be useful, a reasoning infrastructure needs to be ``lifted'' from the
+ − 330
underlying subset to the new type. This is usually a tricky and arduous
+ − 331
task. To ease it, we re-implemented in Isabelle/HOL the quotient package
+ − 332
described by Homeier \cite{Homeier05} for the HOL4 system. This package
+ − 333
allows us to lift definitions and theorems involving raw terms to
2341
+ − 334
definitions and theorems involving $\alpha$-equated terms. For example if we
1657
+ − 335
define the free-variable function over raw lambda-terms
1577
+ − 336
+ − 337
\begin{center}
1657
+ − 338
@{text "fv(x) = {x}"}\hspace{10mm}
+ − 339
@{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]
+ − 340
@{text "fv(\<lambda>x.t) = fv(t) - {x}"}
1577
+ − 341
\end{center}
+ − 342
+ − 343
\noindent
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 344
then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
2341
+ − 345
operating on quotients, or $\alpha$-equivalence classes of lambda-terms. This
1628
+ − 346
lifted function is characterised by the equations
1577
+ − 347
+ − 348
\begin{center}
1657
+ − 349
@{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}
+ − 350
@{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]
+ − 351
@{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<alpha>(t) - {x}"}
1577
+ − 352
\end{center}
+ − 353
+ − 354
\noindent
+ − 355
(Note that this means also the term-constructors for variables, applications
+ − 356
and lambda are lifted to the quotient level.) This construction, of course,
2341
+ − 357
only works if $\alpha$-equivalence is indeed an equivalence relation, and the
+ − 358
``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence.
1694
+ − 359
For example, we will not be able to lift a bound-variable function. Although
+ − 360
this function can be defined for raw terms, it does not respect
2341
+ − 361
$\alpha$-equivalence and therefore cannot be lifted. To sum up, every lifting
1694
+ − 362
of theorems to the quotient level needs proofs of some respectfulness
+ − 363
properties (see \cite{Homeier05}). In the paper we show that we are able to
2128
+ − 364
automate these proofs and as a result can automatically establish a reasoning
2341
+ − 365
infrastructure for $\alpha$-equated terms.
1667
+ − 366
+ − 367
The examples we have in mind where our reasoning infrastructure will be
1694
+ − 368
helpful includes the term language of System @{text "F\<^isub>C"}, also
+ − 369
known as Core-Haskell (see Figure~\ref{corehas}). This term language
1711
+ − 370
involves patterns that have lists of type-, coercion- and term-variables,
1703
+ − 371
all of which are bound in @{text "\<CASE>"}-expressions. One
1926
+ − 372
feature is that we do not know in advance how many variables need to
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 373
be bound. Another is that each bound variable comes with a kind or type
1694
+ − 374
annotation. Representing such binders with single binders and reasoning
+ − 375
about them in a theorem prover would be a major pain. \medskip
1506
+ − 376
1528
+ − 377
\noindent
2381
+ − 378
{\bf Contributions:} We provide three new definitions for when terms
2341
+ − 379
involving general binders are $\alpha$-equivalent. These definitions are
1607
+ − 380
inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
2341
+ − 381
proofs, we establish a reasoning infrastructure for $\alpha$-equated
1528
+ − 382
terms, including properties about support, freshness and equality
2341
+ − 383
conditions for $\alpha$-equated terms. We are also able to derive strong
2218
+ − 384
induction principles that have the variable convention already built in.
2343
+ − 385
The method behind our specification of general binders is taken
2346
+ − 386
from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
2488
+ − 387
that our specifications make sense for reasoning about $\alpha$-equated terms. The main improvement over Ott is that we introduce three binding modes,
+ − 388
provide precise definitions for $\alpha$-equivalence and for free
+ − 389
variables of our terms, and provide automated proofs inside the
+ − 390
Isabelle theorem prover.
2341
+ − 391
1667
+ − 392
+ − 393
\begin{figure}
1687
+ − 394
\begin{boxedminipage}{\linewidth}
+ − 395
\begin{center}
1699
+ − 396
\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
1690
+ − 397
\multicolumn{3}{@ {}l}{Type Kinds}\\
1699
+ − 398
@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
1690
+ − 399
\multicolumn{3}{@ {}l}{Coercion Kinds}\\
1699
+ − 400
@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
1690
+ − 401
\multicolumn{3}{@ {}l}{Types}\\
1694
+ − 402
@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}
1699
+ − 403
@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
1690
+ − 404
\multicolumn{3}{@ {}l}{Coercion Types}\\
1694
+ − 405
@{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
1699
+ − 406
@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
+ − 407
& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
+ − 408
& @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
1690
+ − 409
\multicolumn{3}{@ {}l}{Terms}\\
1699
+ − 410
@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+ − 411
& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
+ − 412
& @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
1690
+ − 413
\multicolumn{3}{@ {}l}{Patterns}\\
1699
+ − 414
@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
1690
+ − 415
\multicolumn{3}{@ {}l}{Constants}\\
1699
+ − 416
& @{text C} & coercion constants\\
+ − 417
& @{text T} & value type constructors\\
+ − 418
& @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
+ − 419
& @{text K} & data constructors\smallskip\\
1690
+ − 420
\multicolumn{3}{@ {}l}{Variables}\\
1699
+ − 421
& @{text a} & type variables\\
+ − 422
& @{text c} & coercion variables\\
+ − 423
& @{text x} & term variables\\
1687
+ − 424
\end{tabular}
+ − 425
\end{center}
+ − 426
\end{boxedminipage}
2345
+ − 427
\caption{The System @{text "F\<^isub>C"}
1699
+ − 428
\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
2345
+ − 429
version of @{text "F\<^isub>C"} we made a modification by separating the
1711
+ − 430
grammars for type kinds and coercion kinds, as well as for types and coercion
1702
+ − 431
types. For this paper the interesting term-constructor is @{text "\<CASE>"},
+ − 432
which binds multiple type-, coercion- and term-variables.\label{corehas}}
1667
+ − 433
\end{figure}
1485
+ − 434
*}
+ − 435
1493
+ − 436
section {* A Short Review of the Nominal Logic Work *}
+ − 437
+ − 438
text {*
1556
+ − 439
At its core, Nominal Isabelle is an adaption of the nominal logic work by
+ − 440
Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
1694
+ − 441
\cite{HuffmanUrban10} (including proofs). We shall briefly review this work
+ − 442
to aid the description of what follows.
+ − 443
1711
+ − 444
Two central notions in the nominal logic work are sorted atoms and
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 445
sort-respecting permutations of atoms. We will use the letters @{text "a,
1711
+ − 446
b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
2347
+ − 447
permutations. The purpose of atoms is to represent variables, be they bound or free.
+ − 448
The sorts of atoms can be used to represent different kinds of
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 449
variables, such as the term-, coercion- and type-variables in Core-Haskell.
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
It is assumed that there is an infinite supply of atoms for each
1847
+ − 451
sort. However, in the interest of brevity, we shall restrict ourselves
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
in what follows to only one sort of atoms.
1493
+ − 453
+ − 454
Permutations are bijective functions from atoms to atoms that are
+ − 455
the identity everywhere except on a finite number of atoms. There is a
+ − 456
two-place permutation operation written
1617
+ − 457
%
1703
+ − 458
\begin{center}
+ − 459
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+ − 460
\end{center}
1493
+ − 461
+ − 462
\noindent
1628
+ − 463
in which the generic type @{text "\<beta>"} stands for the type of the object
1694
+ − 464
over which the permutation
1617
+ − 465
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
1690
+ − 466
the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
1570
+ − 467
and the inverse permutation of @{term p} as @{text "- p"}. The permutation
1890
+ − 468
operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10};
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 469
for example permutations acting on products, lists, sets, functions and booleans is
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
given by:
1702
+ − 471
%
1703
+ − 472
\begin{equation}\label{permute}
1694
+ − 473
\mbox{\begin{tabular}{@ {}cc@ {}}
1690
+ − 474
\begin{tabular}{@ {}l@ {}}
+ − 475
@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+ − 476
@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
+ − 477
@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+ − 478
\end{tabular} &
+ − 479
\begin{tabular}{@ {}l@ {}}
+ − 480
@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
1694
+ − 481
@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
1690
+ − 482
@{thm permute_bool_def[no_vars, THEN eq_reflection]}\\
+ − 483
\end{tabular}
1694
+ − 484
\end{tabular}}
+ − 485
\end{equation}
1690
+ − 486
+ − 487
\noindent
1730
+ − 488
Concrete permutations in Nominal Isabelle are built up from swappings,
+ − 489
written as \mbox{@{text "(a b)"}}, which are permutations that behave
+ − 490
as follows:
1617
+ − 491
%
1703
+ − 492
\begin{center}
+ − 493
@{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
+ − 494
\end{center}
+ − 495
1570
+ − 496
The most original aspect of the nominal logic work of Pitts is a general
1703
+ − 497
definition for the notion of the ``set of free variables of an object @{text
1570
+ − 498
"x"}''. This notion, written @{term "supp x"}, is general in the sense that
2341
+ − 499
it applies not only to lambda-terms ($\alpha$-equated or not), but also to lists,
1570
+ − 500
products, sets and even functions. The definition depends only on the
+ − 501
permutation operation and on the notion of equality defined for the type of
+ − 502
@{text x}, namely:
1617
+ − 503
%
1703
+ − 504
\begin{equation}\label{suppdef}
+ − 505
@{thm supp_def[no_vars, THEN eq_reflection]}
+ − 506
\end{equation}
1493
+ − 507
+ − 508
\noindent
+ − 509
There is also the derived notion for when an atom @{text a} is \emph{fresh}
+ − 510
for an @{text x}, defined as
1617
+ − 511
%
1703
+ − 512
\begin{center}
+ − 513
@{thm fresh_def[no_vars]}
+ − 514
\end{center}
1493
+ − 515
+ − 516
\noindent
1954
+ − 517
We use for sets of atoms the abbreviation
1703
+ − 518
@{thm (lhs) fresh_star_def[no_vars]}, defined as
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
+ − 519
@{thm (rhs) fresh_star_def[no_vars]}.
1493
+ − 520
A striking consequence of these definitions is that we can prove
+ − 521
without knowing anything about the structure of @{term x} that
2140
+ − 522
swapping two fresh atoms, say @{text a} and @{text b}, leaves
+ − 523
@{text x} unchanged:
1506
+ − 524
1711
+ − 525
\begin{property}\label{swapfreshfresh}
1506
+ − 526
@{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
+ − 527
\end{property}
1506
+ − 528
1711
+ − 529
While often the support of an object can be relatively easily
1730
+ − 530
described, for example for atoms, products, lists, function applications,
2341
+ − 531
booleans and permutations as follows
1690
+ − 532
%
+ − 533
\begin{eqnarray}
1703
+ − 534
@{term "supp a"} & = & @{term "{a}"}\\
1690
+ − 535
@{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
+ − 536
@{term "supp []"} & = & @{term "{}"}\\
1711
+ − 537
@{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\
1730
+ − 538
@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\label{suppfun}\\
1703
+ − 539
@{term "supp b"} & = & @{term "{}"}\\
+ − 540
@{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
1690
+ − 541
\end{eqnarray}
+ − 542
+ − 543
\noindent
2347
+ − 544
in some cases it can be difficult to characterise the support precisely, and
1730
+ − 545
only an approximation can be established (see \eqref{suppfun} above). Reasoning about
+ − 546
such approximations can be simplified with the notion \emph{supports}, defined
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 547
as follows:
1693
+ − 548
+ − 549
\begin{defn}
+ − 550
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
+ − 551
not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
+ − 552
\end{defn}
1690
+ − 553
1693
+ − 554
\noindent
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 555
The main point of @{text supports} is that we can establish the following
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 556
two properties.
1693
+ − 557
1703
+ − 558
\begin{property}\label{supportsprop}
2341
+ − 559
Given a set @{text "as"} of atoms.
2381
+ − 560
{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+ − 561
{\it (ii)} @{thm supp_supports[no_vars]}.
1693
+ − 562
\end{property}
+ − 563
+ − 564
Another important notion in the nominal logic work is \emph{equivariance}.
1703
+ − 565
For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 566
it is required that every permutation leaves @{text f} unchanged, that is
1711
+ − 567
%
+ − 568
\begin{equation}\label{equivariancedef}
+ − 569
@{term "\<forall>p. p \<bullet> f = f"}
+ − 570
\end{equation}
+ − 571
+ − 572
\noindent or equivalently that a permutation applied to the application
1730
+ − 573
@{text "f x"} can be moved to the argument @{text x}. That means for equivariant
2341
+ − 574
functions @{text f}, we have for all permutations @{text p}:
1703
+ − 575
%
+ − 576
\begin{equation}\label{equivariance}
1711
+ − 577
@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
+ − 578
@{text "p \<bullet> (f x) = f (p \<bullet> x)"}
1703
+ − 579
\end{equation}
1694
+ − 580
+ − 581
\noindent
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 582
From property \eqref{equivariancedef} and the definition of @{text supp}, we
2175
+ − 583
can easily deduce that equivariant functions have empty support. There is
1771
+ − 584
also a similar notion for equivariant relations, say @{text R}, namely the property
+ − 585
that
+ − 586
%
+ − 587
\begin{center}
2341
+ − 588
@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
1771
+ − 589
\end{center}
1711
+ − 590
2343
+ − 591
Finally, the nominal logic work provides us with general means for renaming
1711
+ − 592
binders. While in the older version of Nominal Isabelle, we used extensively
2343
+ − 593
Property~\ref{swapfreshfresh} to rename single binders, this property
2341
+ − 594
proved too unwieldy for dealing with multiple binders. For such binders the
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 595
following generalisations turned out to be easier to use.
1711
+ − 596
+ − 597
\begin{property}\label{supppermeq}
+ − 598
@{thm[mode=IfThen] supp_perm_eq[no_vars]}
+ − 599
\end{property}
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
+ − 600
1747
+ − 601
\begin{property}\label{avoiding}
1716
+ − 602
For a finite set @{text as} and a finitely supported @{text x} with
+ − 603
@{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
+ − 604
exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
1711
+ − 605
@{term "supp x \<sharp>* p"}.
+ − 606
\end{property}
+ − 607
+ − 608
\noindent
1716
+ − 609
The idea behind the second property is that given a finite set @{text as}
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 610
of binders (being bound, or fresh, in @{text x} is ensured by the
1716
+ − 611
assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 612
the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
1730
+ − 613
as long as it is finitely supported) and also @{text "p"} does not affect anything
1711
+ − 614
in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
+ − 615
fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 616
@{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
1711
+ − 617
2128
+ − 618
Most properties given in this section are described in detail in \cite{HuffmanUrban10}
1737
+ − 619
and of course all are formalised in Isabelle/HOL. In the next sections we will make
2341
+ − 620
extensive use of these properties in order to define $\alpha$-equivalence in
1737
+ − 621
the presence of multiple binders.
1493
+ − 622
*}
+ − 623
1485
+ − 624
2345
+ − 625
section {* General Bindings\label{sec:binders} *}
1485
+ − 626
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
+ − 627
text {*
1587
+ − 628
In Nominal Isabelle, the user is expected to write down a specification of a
+ − 629
term-calculus and then a reasoning infrastructure is automatically derived
1617
+ − 630
from this specification (remember that Nominal Isabelle is a definitional
1587
+ − 631
extension of Isabelle/HOL, which does not introduce any new axioms).
1579
+ − 632
1657
+ − 633
In order to keep our work with deriving the reasoning infrastructure
+ − 634
manageable, we will wherever possible state definitions and perform proofs
2341
+ − 635
on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
1657
+ − 636
generates them anew for each specification. To that end, we will consider
+ − 637
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
2128
+ − 638
are intended to represent the abstraction, or binding, of the set of atoms @{text
1657
+ − 639
"as"} in the body @{text "x"}.
1570
+ − 640
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 641
The first question we have to answer is when two pairs @{text "(as, x)"} and
2341
+ − 642
@{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
+ − 643
the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
+ − 644
vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
2347
+ − 645
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
1657
+ − 646
set"}}, then @{text x} and @{text y} need to have the same set of free
2348
+ − 647
atoms; moreover there must be a permutation @{text p} such that {\it
2347
+ − 648
(ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
2341
+ − 649
{\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
+ − 650
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
1662
+ − 651
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
2343
+ − 652
requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
1556
+ − 653
%
1572
+ − 654
\begin{equation}\label{alphaset}
2341
+ − 655
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
2471
+ − 656
\multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
2347
+ − 657
& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
+ − 658
@{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
2341
+ − 659
@{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+ − 660
@{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
1572
+ − 661
\end{array}
1556
+ − 662
\end{equation}
+ − 663
+ − 664
\noindent
2175
+ − 665
Note that this relation depends on the permutation @{text
2341
+ − 666
"p"}; $\alpha$-equivalence between two pairs is then the relation where we
1657
+ − 667
existentially quantify over this @{text "p"}. Also note that the relation is
2347
+ − 668
dependent on a free-atom function @{text "fa"} and a relation @{text
1657
+ − 669
"R"}. The reason for this extra generality is that we will use
2341
+ − 670
$\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In
+ − 671
the latter case, @{text R} will be replaced by equality @{text "="} and we
2347
+ − 672
will prove that @{text "fa"} is equal to @{text "supp"}.
1572
+ − 673
+ − 674
The definition in \eqref{alphaset} does not make any distinction between the
2347
+ − 675
order of abstracted atoms. If we want this, then we can define $\alpha$-equivalence
1579
+ − 676
for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
+ − 677
as follows
1572
+ − 678
%
+ − 679
\begin{equation}\label{alphalist}
2341
+ − 680
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
2347
+ − 681
\multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ − 682
& @{term "fa(x) - (set as) = fa(y) - (set bs)"} & \mbox{\it (i)}\\
+ − 683
\wedge & @{term "(fa(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
2341
+ − 684
\wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+ − 685
\wedge & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
1572
+ − 686
\end{array}
+ − 687
\end{equation}
+ − 688
+ − 689
\noindent
2341
+ − 690
where @{term set} is the function that coerces a list of atoms into a set of atoms.
1752
+ − 691
Now the last clause ensures that the order of the binders matters (since @{text as}
+ − 692
and @{text bs} are lists of atoms).
1556
+ − 693
1657
+ − 694
If we do not want to make any difference between the order of binders \emph{and}
1579
+ − 695
also allow vacuous binders, then we keep sets of binders, but drop the fourth
+ − 696
condition in \eqref{alphaset}:
1572
+ − 697
%
1579
+ − 698
\begin{equation}\label{alphares}
2341
+ − 699
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
2347
+ − 700
\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ − 701
& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
+ − 702
\wedge & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
2341
+ − 703
\wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
1572
+ − 704
\end{array}
+ − 705
\end{equation}
1556
+ − 706
2345
+ − 707
It might be useful to consider first some examples about how these definitions
2341
+ − 708
of $\alpha$-equivalence pan out in practice. For this consider the case of
2347
+ − 709
abstracting a set of atoms over types (as in type-schemes). We set
+ − 710
@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
2341
+ − 711
define
1572
+ − 712
+ − 713
\begin{center}
2347
+ − 714
@{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
1572
+ − 715
\end{center}
+ − 716
+ − 717
\noindent
1657
+ − 718
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
1687
+ − 719
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
2341
+ − 720
@{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
+ − 721
$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to
2175
+ − 722
be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
2341
+ − 723
"([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
2175
+ − 724
since there is no permutation that makes the lists @{text "[x, y]"} and
+ − 725
@{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
2341
+ − 726
unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$
2175
+ − 727
@{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
+ − 728
permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
2341
+ − 729
$\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
2175
+ − 730
permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
2341
+ − 731
(similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be
+ − 732
shown that all three notions of $\alpha$-equivalence coincide, if we only
2175
+ − 733
abstract a single atom.
1579
+ − 734
1730
+ − 735
In the rest of this section we are going to introduce three abstraction
+ − 736
types. For this we define
1657
+ − 737
%
+ − 738
\begin{equation}
2471
+ − 739
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
1657
+ − 740
\end{equation}
+ − 741
1579
+ − 742
\noindent
2341
+ − 743
(similarly for $\approx_{\,\textit{abs\_res}}$
+ − 744
and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
1687
+ − 745
relations and equivariant.
1579
+ − 746
1739
+ − 747
\begin{lemma}\label{alphaeq}
2341
+ − 748
The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
+ − 749
and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term
1739
+ − 750
"abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
+ − 751
bs, p \<bullet> y)"} (similarly for the other two relations).
1657
+ − 752
\end{lemma}
+ − 753
+ − 754
\begin{proof}
+ − 755
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
+ − 756
a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
1662
+ − 757
of transitivity, we have two permutations @{text p} and @{text q}, and for the
+ − 758
proof obligation use @{text "q + p"}. All conditions are then by simple
1657
+ − 759
calculations.
+ − 760
\end{proof}
+ − 761
+ − 762
\noindent
2343
+ − 763
This lemma allows us to use our quotient package for introducing
1662
+ − 764
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
2341
+ − 765
representing $\alpha$-equivalence classes of pairs of type
2128
+ − 766
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
+ − 767
(in the third case).
1954
+ − 768
The elements in these types will be, respectively, written as:
1657
+ − 769
+ − 770
\begin{center}
2471
+ − 771
@{term "Abs_set as x"} \hspace{5mm}
1954
+ − 772
@{term "Abs_res as x"} \hspace{5mm}
+ − 773
@{term "Abs_lst as x"}
1657
+ − 774
\end{center}
+ − 775
1662
+ − 776
\noindent
1859
+ − 777
indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
1716
+ − 778
call the types \emph{abstraction types} and their elements
1752
+ − 779
\emph{abstractions}. The important property we need to derive is the support of
1737
+ − 780
abstractions, namely:
1662
+ − 781
1687
+ − 782
\begin{thm}[Support of Abstractions]\label{suppabs}
1703
+ − 783
Assuming @{text x} has finite support, then\\[-6mm]
1662
+ − 784
\begin{center}
1687
+ − 785
\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
2502
+ − 786
@{thm (lhs) supp_Abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(1)[no_vars]}\\
+ − 787
@{thm (lhs) supp_Abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(2)[no_vars]}\\
+ − 788
@{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}
1687
+ − 789
\end{tabular}
1662
+ − 790
\end{center}
1687
+ − 791
\end{thm}
1662
+ − 792
+ − 793
\noindent
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 794
Below we will show the first equation. The others
1730
+ − 795
follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
1687
+ − 796
we have
+ − 797
%
+ − 798
\begin{equation}\label{abseqiff}
2502
+ − 799
@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
+ − 800
@{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
1687
+ − 801
\end{equation}
+ − 802
+ − 803
\noindent
1703
+ − 804
and also
+ − 805
%
2128
+ − 806
\begin{equation}\label{absperm}
1703
+ − 807
@{thm permute_Abs[no_vars]}
+ − 808
\end{equation}
1662
+ − 809
1703
+ − 810
\noindent
1716
+ − 811
The second fact derives from the definition of permutations acting on pairs
2341
+ − 812
\eqref{permute} and $\alpha$-equivalence being equivariant
1716
+ − 813
(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
2341
+ − 814
the following lemma about swapping two atoms in an abstraction.
1703
+ − 815
1662
+ − 816
\begin{lemma}
2502
+ − 817
@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
1662
+ − 818
\end{lemma}
+ − 819
+ − 820
\begin{proof}
1730
+ − 821
This lemma is straightforward using \eqref{abseqiff} and observing that
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 822
the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
1730
+ − 823
Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
1662
+ − 824
\end{proof}
1587
+ − 825
1687
+ − 826
\noindent
2163
+ − 827
Assuming that @{text "x"} has finite support, this lemma together
+ − 828
with \eqref{absperm} allows us to show
1687
+ − 829
%
+ − 830
\begin{equation}\label{halfone}
2502
+ − 831
@{thm Abs_supports(1)[no_vars]}
1687
+ − 832
\end{equation}
+ − 833
+ − 834
\noindent
1716
+ − 835
which by Property~\ref{supportsprop} gives us ``one half'' of
1752
+ − 836
Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
1716
+ − 837
it, we use a trick from \cite{Pitts04} and first define an auxiliary
1737
+ − 838
function @{text aux}, taking an abstraction as argument:
1687
+ − 839
%
+ − 840
\begin{center}
2471
+ − 841
@{thm supp_set.simps[THEN eq_reflection, no_vars]}
1687
+ − 842
\end{center}
+ − 843
1703
+ − 844
\noindent
+ − 845
Using the second equation in \eqref{equivariance}, we can show that
1716
+ − 846
@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
+ − 847
(supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support.
+ − 848
This in turn means
1703
+ − 849
%
+ − 850
\begin{center}
2471
+ − 851
@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
1703
+ − 852
\end{center}
1687
+ − 853
+ − 854
\noindent
1954
+ − 855
using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
1716
+ − 856
we further obtain
1703
+ − 857
%
+ − 858
\begin{equation}\label{halftwo}
2502
+ − 859
@{thm (concl) Abs_supp_subset1(1)[no_vars]}
1703
+ − 860
\end{equation}
+ − 861
+ − 862
\noindent
1737
+ − 863
since for finite sets of atoms, @{text "bs"}, we have
+ − 864
@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+ − 865
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
+ − 866
Theorem~\ref{suppabs}.
1703
+ − 867
1737
+ − 868
The method of first considering abstractions of the
2471
+ − 869
form @{term "Abs_set as x"} etc is motivated by the fact that
1956
+ − 870
we can conveniently establish at the Isabelle/HOL level
+ − 871
properties about them. It would be
+ − 872
laborious to write custom ML-code that derives automatically such properties
1730
+ − 873
for every term-constructor that binds some atoms. Also the generality of
2341
+ − 874
the definitions for $\alpha$-equivalence will help us in the next section.
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
+ − 875
*}
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
+ − 876
2345
+ − 877
section {* Specifying General Bindings\label{sec:spec} *}
1491
+ − 878
1520
+ − 879
text {*
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 880
Our choice of syntax for specifications is influenced by the existing
1765
+ − 881
datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
+ − 882
Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
+ − 883
collection of (possibly mutual recursive) type declarations, say @{text
+ − 884
"ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
+ − 885
binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
+ − 886
syntax in Nominal Isabelle for such specifications is roughly as follows:
1628
+ − 887
%
1619
+ − 888
\begin{equation}\label{scheme}
1636
+ − 889
\mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
1617
+ − 890
type \mbox{declaration part} &
1611
+ − 891
$\begin{cases}
+ − 892
\mbox{\begin{tabular}{l}
1765
+ − 893
\isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
+ − 894
\isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
1587
+ − 895
$\ldots$\\
1765
+ − 896
\isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\
1611
+ − 897
\end{tabular}}
+ − 898
\end{cases}$\\
1617
+ − 899
binding \mbox{function part} &
1611
+ − 900
$\begin{cases}
+ − 901
\mbox{\begin{tabular}{l}
1954
+ − 902
\isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
1611
+ − 903
\isacommand{where}\\
1587
+ − 904
$\ldots$\\
1611
+ − 905
\end{tabular}}
+ − 906
\end{cases}$\\
1619
+ − 907
\end{tabular}}
+ − 908
\end{equation}
1587
+ − 909
+ − 910
\noindent
1637
+ − 911
Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of
2341
+ − 912
term-constructors, each of which comes with a list of labelled
1620
+ − 913
types that stand for the types of the arguments of the term-constructor.
1765
+ − 914
For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
1611
+ − 915
+ − 916
\begin{center}
1637
+ − 917
@{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$ @{text "binding_clauses"}
1611
+ − 918
\end{center}
1587
+ − 919
1611
+ − 920
\noindent
2128
+ − 921
whereby some of the @{text ty}$'_{1..l}$ (or their components) can be contained
1730
+ − 922
in the collection of @{text ty}$^\alpha_{1..n}$ declared in
1737
+ − 923
\eqref{scheme}.
1765
+ − 924
In this case we will call the corresponding argument a
+ − 925
\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.
+ − 926
%The types of such recursive
1737
+ − 927
%arguments need to satisfy a ``positivity''
+ − 928
%restriction, which ensures that the type has a set-theoretic semantics
+ − 929
%\cite{Berghofer99}.
+ − 930
The labels
1730
+ − 931
annotated on the types are optional. Their purpose is to be used in the
+ − 932
(possibly empty) list of \emph{binding clauses}, which indicate the binders
+ − 933
and their scope in a term-constructor. They come in three \emph{modes}:
1587
+ − 934
1611
+ − 935
\begin{center}
1617
+ − 936
\begin{tabular}{l}
2343
+ − 937
\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
2488
+ − 938
\isacommand{bind (set)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+ − 939
\isacommand{bind (res)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
1617
+ − 940
\end{tabular}
1611
+ − 941
\end{center}
+ − 942
+ − 943
\noindent
1730
+ − 944
The first mode is for binding lists of atoms (the order of binders matters);
+ − 945
the second is for sets of binders (the order does not matter, but the
+ − 946
cardinality does) and the last is for sets of binders (with vacuous binders
2359
+ − 947
preserving $\alpha$-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
2343
+ − 948
clause will be called \emph{bodies}; the
2163
+ − 949
``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
+ − 950
Ott, we allow multiple labels in binders and bodies. For example we allow
+ − 951
binding clauses of the form:
1956
+ − 952
+ − 953
\begin{center}
2156
+ − 954
\begin{tabular}{@ {}ll@ {}}
2341
+ − 955
@{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &
2156
+ − 956
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
2341
+ − 957
@{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &
2156
+ − 958
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"},
+ − 959
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
1956
+ − 960
\end{tabular}
+ − 961
\end{center}
+ − 962
+ − 963
\noindent
2343
+ − 964
Similarly for the other binding modes.
2488
+ − 965
%Interestingly, in case of \isacommand{bind (set)}
+ − 966
%and \isacommand{bind (res)} the binding clauses above will make a difference to the semantics
2343
+ − 967
%of the specifications (the corresponding $\alpha$-equivalence will differ). We will
+ − 968
%show this later with an example.
2140
+ − 969
2347
+ − 970
There are also some restrictions we need to impose on our binding clauses in comparison to
+ − 971
the ones of Ott. The
2343
+ − 972
main idea behind these restrictions is that we obtain a sensible notion of
2347
+ − 973
$\alpha$-equivalence where it is ensured that within a given scope an
2348
+ − 974
atom occurrence cannot be both bound and free at the same time. The first
2344
+ − 975
restriction is that a body can only occur in
2343
+ − 976
\emph{one} binding clause of a term constructor (this ensures that the bound
2347
+ − 977
atoms of a body cannot be free at the same time by specifying an
2344
+ − 978
alternative binder for the same body). For binders we distinguish between
2343
+ − 979
\emph{shallow} and \emph{deep} binders. Shallow binders are just
+ − 980
labels. The restriction we need to impose on them is that in case of
2488
+ − 981
\isacommand{bind (set)} and \isacommand{bind (res)} the labels must either
2343
+ − 982
refer to atom types or to sets of atom types; in case of \isacommand{bind}
+ − 983
the labels must refer to atom types or lists of atom types. Two examples for
+ − 984
the use of shallow binders are the specification of lambda-terms, where a
+ − 985
single name is bound, and type-schemes, where a finite set of names is
+ − 986
bound:
+ − 987
1611
+ − 988
+ − 989
\begin{center}
1612
+ − 990
\begin{tabular}{@ {}cc@ {}}
2488
+ − 991
\begin{tabular}{@ {}l@ {\hspace{-2mm}}}
2341
+ − 992
\isacommand{nominal\_datatype} @{text lam} $=$\\
1719
+ − 993
\hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
+ − 994
\hspace{5mm}$\mid$~@{text "App lam lam"}\\
+ − 995
\hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
+ − 996
\hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
1611
+ − 997
\end{tabular} &
1612
+ − 998
\begin{tabular}{@ {}l@ {}}
2341
+ − 999
\isacommand{nominal\_datatype}~@{text ty} $=$\\
1719
+ − 1000
\hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
+ − 1001
\hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
+ − 1002
\isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
2488
+ − 1003
\hspace{21mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
1611
+ − 1004
\end{tabular}
+ − 1005
\end{tabular}
+ − 1006
\end{center}
1587
+ − 1007
1612
+ − 1008
\noindent
2341
+ − 1009
In these specifications @{text "name"} refers to an atom type, and @{text
+ − 1010
"fset"} to the type of finite sets.
2156
+ − 1011
Note that for @{text lam} it does not matter which binding mode we use. The
+ − 1012
reason is that we bind only a single @{text name}. However, having
2488
+ − 1013
\isacommand{bind (set)} or \isacommand{bind} in the second case makes a
2345
+ − 1014
difference to the semantics of the specification (which we will define in the next section).
2156
+ − 1015
2128
+ − 1016
2134
+ − 1017
A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
2156
+ − 1018
the atoms in one argument of the term-constructor, which can be bound in
+ − 1019
other arguments and also in the same argument (we will call such binders
2341
+ − 1020
\emph{recursive}, see below). The binding functions are
2488
+ − 1021
expected to return either a set of atoms (for \isacommand{bind (set)} and
+ − 1022
\isacommand{bind (res)}) or a list of atoms (for \isacommand{bind}). They can
2343
+ − 1023
be defined by recursion over the corresponding type; the equations
2156
+ − 1024
must be given in the binding function part of the scheme shown in
+ − 1025
\eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
+ − 1026
tuple patterns might be specified as:
1764
+ − 1027
%
+ − 1028
\begin{equation}\label{letpat}
+ − 1029
\mbox{%
1619
+ − 1030
\begin{tabular}{l}
1719
+ − 1031
\isacommand{nominal\_datatype} @{text trm} =\\
+ − 1032
\hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
+ − 1033
\hspace{5mm}$\mid$~@{term "App trm trm"}\\
+ − 1034
\hspace{5mm}$\mid$~@{text "Lam x::name t::trm"}
+ − 1035
\;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+ − 1036
\hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"}
+ − 1037
\;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
+ − 1038
\isacommand{and} @{text pat} =\\
+ − 1039
\hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
+ − 1040
\hspace{5mm}$\mid$~@{text "PVar name"}\\
+ − 1041
\hspace{5mm}$\mid$~@{text "PTup pat pat"}\\
1954
+ − 1042
\isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
1719
+ − 1043
\isacommand{where}~@{text "bn(PNil) = []"}\\
+ − 1044
\hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
2341
+ − 1045
\hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\
1764
+ − 1046
\end{tabular}}
+ − 1047
\end{equation}
1617
+ − 1048
1619
+ − 1049
\noindent
2140
+ − 1050
In this specification the function @{text "bn"} determines which atoms of
2346
+ − 1051
the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
2140
+ − 1052
second-last @{text bn}-clause the function @{text "atom"} coerces a name
+ − 1053
into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
+ − 1054
allows us to treat binders of different atom type uniformly.
1637
+ − 1055
2140
+ − 1056
As said above, for deep binders we allow binding clauses such as
+ − 1057
%
1620
+ − 1058
\begin{center}
+ − 1059
\begin{tabular}{ll}
2140
+ − 1060
@{text "Bar p::pat t::trm"} &
1954
+ − 1061
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
1620
+ − 1062
\end{tabular}
+ − 1063
\end{center}
+ − 1064
+ − 1065
\noindent
2344
+ − 1066
where the argument of the deep binder also occurs in the body. We call such
2140
+ − 1067
binders \emph{recursive}. To see the purpose of such recursive binders,
+ − 1068
compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
+ − 1069
specification:
2343
+ − 1070
%
1725
+ − 1071
\begin{equation}\label{letrecs}
+ − 1072
\mbox{%
1637
+ − 1073
\begin{tabular}{@ {}l@ {}}
1725
+ − 1074
\isacommand{nominal\_datatype}~@{text "trm ="}\\
1636
+ − 1075
\hspace{5mm}\phantom{$\mid$}\ldots\\
1725
+ − 1076
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
+ − 1077
\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
1954
+ − 1078
\hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
+ − 1079
\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
+ − 1080
\isacommand{and} @{text "ass"} =\\
1725
+ − 1081
\hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
+ − 1082
\hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
1954
+ − 1083
\isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
1725
+ − 1084
\isacommand{where}~@{text "bn(ANil) = []"}\\
+ − 1085
\hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
+ − 1086
\end{tabular}}
+ − 1087
\end{equation}
1636
+ − 1088
+ − 1089
\noindent
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1090
The difference is that with @{text Let} we only want to bind the atoms @{text
1730
+ − 1091
"bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
2346
+ − 1092
inside the assignment. This difference has consequences for the associated
2347
+ − 1093
notions of free-atoms and $\alpha$-equivalence.
2341
+ − 1094
2347
+ − 1095
To make sure that atoms bound by deep binders cannot be free at the
2346
+ − 1096
same time, we cannot have more than one binding function for a deep binder.
2344
+ − 1097
Consequently we exclude specifications such as
2140
+ − 1098
+ − 1099
\begin{center}
2341
+ − 1100
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
+ − 1101
@{text "Baz\<^isub>1 p::pat t::trm"} &
2140
+ − 1102
\isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
2341
+ − 1103
@{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} &
+ − 1104
\isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
+ − 1105
\isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
2140
+ − 1106
\end{tabular}
+ − 1107
\end{center}
+ − 1108
+ − 1109
\noindent
2344
+ − 1110
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
2348
+ − 1111
out different atoms to become bound, respectively be free, in @{text "p"}.
2359
+ − 1112
(Since the Ott-tool does not derive a reasoning infrastructure for
+ − 1113
$\alpha$-equated terms, it can permit such specifications.)
2343
+ − 1114
2344
+ − 1115
We also need to restrict the form of the binding functions in order
2345
+ − 1116
to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
2346
+ − 1117
terms. The main restriction is that we cannot return an atom in a binding function that is also
+ − 1118
bound in the corresponding term-constructor. That means in \eqref{letpat}
+ − 1119
that the term-constructors @{text PVar} and @{text PTup} may
1961
+ − 1120
not have a binding clause (all arguments are used to define @{text "bn"}).
+ − 1121
In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
2341
+ − 1122
may have a binding clause involving the argument @{text t} (the only one that
2343
+ − 1123
is \emph{not} used in the definition of the binding function). This restriction
2359
+ − 1124
is sufficient for having the binding function over $\alpha$-equated terms.
2341
+ − 1125
+ − 1126
In the version of
1961
+ − 1127
Nominal Isabelle described here, we also adopted the restriction from the
+ − 1128
Ott-tool that binding functions can only return: the empty set or empty list
+ − 1129
(as in case @{text PNil}), a singleton set or singleton list containing an
+ − 1130
atom (case @{text PVar}), or unions of atom sets or appended atom lists
2341
+ − 1131
(case @{text PTup}). This restriction will simplify some automatic definitions and proofs
1961
+ − 1132
later on.
+ − 1133
2347
+ − 1134
In order to simplify our definitions of free atoms and $\alpha$-equivalence,
2343
+ − 1135
we shall assume specifications
2341
+ − 1136
of term-calculi are implicitly \emph{completed}. By this we mean that
1954
+ − 1137
for every argument of a term-constructor that is \emph{not}
2163
+ − 1138
already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
+ − 1139
clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
1956
+ − 1140
of the lambda-calculus, the completion produces
1954
+ − 1141
+ − 1142
\begin{center}
+ − 1143
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+ − 1144
\isacommand{nominal\_datatype} @{text lam} =\\
+ − 1145
\hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
+ − 1146
\;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
+ − 1147
\hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
2163
+ − 1148
\;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
1954
+ − 1149
\hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
+ − 1150
\;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\
+ − 1151
\end{tabular}
+ − 1152
\end{center}
+ − 1153
+ − 1154
\noindent
+ − 1155
The point of completion is that we can make definitions over the binding
1961
+ − 1156
clauses and be sure to have captured all arguments of a term constructor.
2342
+ − 1157
*}
1954
+ − 1158
2347
+ − 1159
section {* Alpha-Equivalence and Free Atoms\label{sec:alpha} *}
2342
+ − 1160
+ − 1161
text {*
1637
+ − 1162
Having dealt with all syntax matters, the problem now is how we can turn
+ − 1163
specifications into actual type definitions in Isabelle/HOL and then
1926
+ − 1164
establish a reasoning infrastructure for them. As
1956
+ − 1165
Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just
1954
+ − 1166
re-arranging the arguments of
1956
+ − 1167
term-constructors so that binders and their bodies are next to each other will
2347
+ − 1168
result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}.
2343
+ − 1169
Therefore we will first
2346
+ − 1170
extract ``raw'' datatype definitions from the specification and then define
2343
+ − 1171
explicitly an $\alpha$-equivalence relation over them. We subsequently
+ − 1172
quotient the datatypes according to our $\alpha$-equivalence.
1637
+ − 1173
+ − 1174
2346
+ − 1175
The ``raw'' datatype definition can be obtained by stripping off the
1771
+ − 1176
binding clauses and the labels from the types. We also have to invent
1637
+ − 1177
new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
1756
+ − 1178
given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
1771
+ − 1179
But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate
2341
+ − 1180
that a notion is defined over $\alpha$-equivalence classes and leave it out
1724
+ − 1181
for the corresponding notion defined on the ``raw'' level. So for example
+ − 1182
we have
+ − 1183
1636
+ − 1184
\begin{center}
1723
+ − 1185
@{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
1636
+ − 1186
\end{center}
+ − 1187
+ − 1188
\noindent
1730
+ − 1189
where @{term ty} is the type used in the quotient construction for
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1190
@{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}.
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1191
1637
+ − 1192
The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
+ − 1193
non-empty and the types in the constructors only occur in positive
2348
+ − 1194
position (see \cite{Berghofer99} for an in-depth description of the datatype package
+ − 1195
in Isabelle/HOL). We subsequently define each of the user-specified binding
+ − 1196
functions @{term "bn"}$_{1..m}$ by recursion over the corresponding
1730
+ − 1197
raw datatype. We can also easily define permutation operations by
2345
+ − 1198
recursion so that for each term constructor @{text "C"} we have that
1766
+ − 1199
%
+ − 1200
\begin{equation}\label{ceqvt}
1961
+ − 1201
@{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
1766
+ − 1202
\end{equation}
2343
+ − 1203
2341
+ − 1204
The first non-trivial step we have to perform is the generation of
2348
+ − 1205
free-atom functions from the specification. For the
2347
+ − 1206
\emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
2343
+ − 1207
%
+ − 1208
\begin{equation}\label{fvars}
2347
+ − 1209
@{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
2343
+ − 1210
\end{equation}
2341
+ − 1211
+ − 1212
\noindent
2346
+ − 1213
by mutual recursion.
2347
+ − 1214
We define these functions together with auxiliary free-atom functions for
2343
+ − 1215
the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
+ − 1216
we define
+ − 1217
%
2341
+ − 1218
\begin{center}
2347
+ − 1219
@{text "fa_bn\<^isub>1, \<dots>, fa_bn\<^isub>m"}
2341
+ − 1220
\end{center}
+ − 1221
+ − 1222
\noindent
+ − 1223
The reason for this setup is that in a deep binder not all atoms have to be
+ − 1224
bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
2348
+ − 1225
that calculates those free atoms in a deep binder.
2343
+ − 1226
2347
+ − 1227
While the idea behind these free-atom functions is clear (they just
2343
+ − 1228
collect all atoms that are not bound), because of our rather complicated
2345
+ − 1229
binding mechanisms their definitions are somewhat involved. Given
2346
+ − 1230
a term-constructor @{text "C"} of type @{text ty} and some associated
2344
+ − 1231
binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
2347
+ − 1232
"fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
2348
+ − 1233
"fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
2488
+ − 1234
clause means. We only show the details for the mode \isacommand{bind (set)} (the other modes are similar).
2345
+ − 1235
Suppose the binding clause @{text bc\<^isub>i} is of the form
2343
+ − 1236
%
2348
+ − 1237
\begin{center}
2488
+ − 1238
\mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
2348
+ − 1239
\end{center}
2341
+ − 1240
2343
+ − 1241
\noindent
2344
+ − 1242
in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
+ − 1243
and the binders @{text b}$_{1..p}$
2343
+ − 1244
either refer to labels of atom types (in case of shallow binders) or to binding
2348
+ − 1245
functions taking a single label as argument (in case of deep binders). Assuming
+ − 1246
@{text "D"} stands for the set of free atoms of the bodies, @{text B} for the
+ − 1247
set of binding atoms in the binders and @{text "B'"} for the set of free atoms in
2344
+ − 1248
non-recursive deep binders,
2348
+ − 1249
then the free atoms of the binding clause @{text bc\<^isub>i} are
2343
+ − 1250
%
2348
+ − 1251
\begin{equation}\label{fadef}
+ − 1252
\mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
+ − 1253
\end{equation}
2343
+ − 1254
+ − 1255
\noindent
2348
+ − 1256
The set @{text D} is formally defined as
2343
+ − 1257
%
+ − 1258
\begin{center}
2347
+ − 1259
@{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
2343
+ − 1260
\end{center}
+ − 1261
+ − 1262
\noindent
2348
+ − 1263
where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
+ − 1264
specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
+ − 1265
we are defining by recursion
+ − 1266
(see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+ − 1267
+ − 1268
In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
+ − 1269
for atom types to which shallow binders may refer
2344
+ − 1270
%
1954
+ − 1271
\begin{center}
+ − 1272
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
2345
+ − 1273
@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
+ − 1274
@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
+ − 1275
@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
1954
+ − 1276
\end{tabular}
+ − 1277
\end{center}
+ − 1278
+ − 1279
\noindent
2348
+ − 1280
Like the function @{text atom}, the function @{text "atoms"} coerces
+ − 1281
a set of atoms to a set of the generic atom type. It is defined as
2344
+ − 1282
@{text "atoms as \<equiv> {atom a | a \<in> as}"}.
2345
+ − 1283
The set @{text B} is then formally defined as
2344
+ − 1284
%
+ − 1285
\begin{center}
+ − 1286
@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
+ − 1287
\end{center}
1954
+ − 1288
2344
+ − 1289
\noindent
2348
+ − 1290
where we use the auxiliary binding functions for shallow binders.
2344
+ − 1291
The set @{text "B'"} collects all free atoms in non-recursive deep
2347
+ − 1292
binders. Let us assume these binders in @{text "bc\<^isub>i"} are
1956
+ − 1293
%
2344
+ − 1294
\begin{center}
2348
+ − 1295
@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}
2344
+ − 1296
\end{center}
+ − 1297
+ − 1298
\noindent
2349
+ − 1299
with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the
+ − 1300
@{text "l"}$_{1..r}$ being among the bodies @{text
2345
+ − 1301
"d"}$_{1..q}$. The set @{text "B'"} is defined as
2344
+ − 1302
%
+ − 1303
\begin{center}
2348
+ − 1304
@{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
2344
+ − 1305
\end{center}
1628
+ − 1306
1636
+ − 1307
\noindent
2348
+ − 1308
This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.
2344
+ − 1309
2348
+ − 1310
Note that for non-recursive deep binders, we have to add in \eqref{fadef}
+ − 1311
the set of atoms that are left unbound by the binding functions @{text
2349
+ − 1312
"bn"}$_{1..m}$. We used for the definition of
2348
+ − 1313
this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual
+ − 1314
recursion. Assume the user specified a @{text bn}-clause of the form
1956
+ − 1315
%
2344
+ − 1316
\begin{center}
2347
+ − 1317
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
2344
+ − 1318
\end{center}
1628
+ − 1319
1954
+ − 1320
\noindent
2347
+ − 1321
where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of
2345
+ − 1322
the arguments we calculate the free atoms as follows:
2344
+ − 1323
%
+ − 1324
\begin{center}
+ − 1325
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
2347
+ − 1326
$\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}
2348
+ − 1327
(that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\\
2347
+ − 1328
$\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}
2345
+ − 1329
with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\
2344
+ − 1330
$\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"},
2347
+ − 1331
but without a recursive call.
2344
+ − 1332
\end{tabular}
+ − 1333
\end{center}
1758
731d39fb26b7
Update fv_bn definition for bindings allowed in types for which bn is present.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1334
2344
+ − 1335
\noindent
2348
+ − 1336
For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.
2344
+ − 1337
2348
+ − 1338
To see how these definitions work in practice, let us reconsider the
+ − 1339
term-constructors @{text "Let"} and @{text "Let_rec"} shown in
+ − 1340
\eqref{letrecs} together with the term-constructors for assignments @{text
+ − 1341
"ANil"} and @{text "ACons"}. Since there is a binding function defined for
+ − 1342
assignments, we have three free-atom functions, namely @{text
+ − 1343
"fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
+ − 1344
"fa\<^bsub>bn\<^esub>"} as follows:
1725
+ − 1345
%
+ − 1346
\begin{center}
+ − 1347
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
2347
+ − 1348
@{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
+ − 1349
@{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
1725
+ − 1350
2347
+ − 1351
@{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
+ − 1352
@{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]
1725
+ − 1353
2347
+ − 1354
@{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
+ − 1355
@{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
1725
+ − 1356
\end{tabular}
+ − 1357
\end{center}
+ − 1358
+ − 1359
\noindent
2349
+ − 1360
Recall that @{text ANil} and @{text "ACons"} have no
2347
+ − 1361
binding clause in the specification. The corresponding free-atom
2348
+ − 1362
function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
2360
+ − 1363
occurring in an assignment (in case of @{text "ACons"}, they are given in
+ − 1364
terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}).
2348
+ − 1365
The binding only takes place in @{text Let} and
+ − 1366
@{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
2345
+ − 1367
that all atoms given by @{text "set (bn as)"} have to be bound in @{text
+ − 1368
t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
2347
+ − 1369
"fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
2348
+ − 1370
free in @{text "as"}. This is
+ − 1371
in contrast with @{text "Let_rec"} where we have a recursive
+ − 1372
binder to bind all occurrences of the atoms in @{text
2345
+ − 1373
"set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
2348
+ − 1374
@{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
+ − 1375
Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the
2349
+ − 1376
list of assignments, but instead returns the free atoms, which means in this
2348
+ − 1377
example the free atoms in the argument @{text "t"}.
+ − 1378
2345
+ − 1379
An interesting point in this
2348
+ − 1380
example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any
+ − 1381
atoms, even if the binding function is specified over assignments.
+ − 1382
Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will
+ − 1383
some atoms actually become bound. This is a phenomenon that has also been pointed
2345
+ − 1384
out in \cite{ott-jfp}. For us this observation is crucial, because we would
2348
+ − 1385
not be able to lift the @{text "bn"}-functions to $\alpha$-equated terms if they act on
+ − 1386
atoms that are bound. In that case, these functions would \emph{not} respect
2345
+ − 1387
$\alpha$-equivalence.
+ − 1388
2348
+ − 1389
Next we define the $\alpha$-equivalence relations for the raw types @{text
+ − 1390
"ty"}$_{1..n}$ from the specification. We write them as
1733
+ − 1391
%
2345
+ − 1392
\begin{center}
+ − 1393
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
+ − 1394
\end{center}
1725
+ − 1395
1764
+ − 1396
\noindent
2347
+ − 1397
Like with the free-atom functions, we also need to
2345
+ − 1398
define auxiliary $\alpha$-equivalence relations
+ − 1399
%
+ − 1400
\begin{center}
+ − 1401
@{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
+ − 1402
\end{center}
2344
+ − 1403
2345
+ − 1404
\noindent
+ − 1405
for the binding functions @{text "bn"}$_{1..m}$,
+ − 1406
To simplify our definitions we will use the following abbreviations for
2348
+ − 1407
\emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples
1733
+ − 1408
%
+ − 1409
\begin{center}
1737
+ − 1410
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
2348
+ − 1411
@{text "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} & \\
+ − 1412
\multicolumn{3}{r}{@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}}\\
+ − 1413
@{text "(fa\<^isub>1,.., fa\<^isub>n) (x\<^isub>1,.., x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> .. \<union> fa\<^isub>n x\<^isub>n"}\\
1733
+ − 1414
\end{tabular}
+ − 1415
\end{center}
+ − 1416
1727
fd2913415a73
started to polish alpha-equivalence section, but needs more work
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1417
2348
+ − 1418
The $\alpha$-equivalence relations are defined as inductive predicates
+ − 1419
having a single clause for each term-constructor. Assuming a
+ − 1420
term-constructor @{text C} is of type @{text ty} and has the binding clauses
+ − 1421
@{term "bc"}$_{1..k}$, then the $\alpha$-equivalence clause has the form
1737
+ − 1422
%
+ − 1423
\begin{center}
2345
+ − 1424
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n \<approx>ty C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
2348
+ − 1425
{@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}}
+ − 1426
\end{center}
+ − 1427
+ − 1428
\noindent
+ − 1429
The task below is to specify what the premises of a binding clause are. As a
+ − 1430
special instance, we first treat the case where @{text "bc\<^isub>i"} is the
+ − 1431
empty binding clause of the form
+ − 1432
%
+ − 1433
\begin{center}
2488
+ − 1434
\mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
2348
+ − 1435
\end{center}
+ − 1436
+ − 1437
\noindent
+ − 1438
In this binding clause no atom is bound and we only have to $\alpha$-relate the bodies. For this
+ − 1439
we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
+ − 1440
whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and
+ − 1441
respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate
+ − 1442
two such tuples we define the compound $\alpha$-equivalence relation @{text "R"} as follows
+ − 1443
%
+ − 1444
\begin{equation}\label{rempty}
+ − 1445
\mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}
+ − 1446
\end{equation}
+ − 1447
+ − 1448
\noindent
+ − 1449
with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and
+ − 1450
@{text "d\<PRIME>\<^isub>i"} refer
+ − 1451
to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise
+ − 1452
we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define
+ − 1453
the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"},
+ − 1454
which can be unfolded to the series of premises
+ − 1455
%
+ − 1456
\begin{center}
+ − 1457
@{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1 \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}
+ − 1458
\end{center}
+ − 1459
+ − 1460
\noindent
+ − 1461
We will use the unfolded version in the examples below.
+ − 1462
+ − 1463
Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form
+ − 1464
%
+ − 1465
\begin{equation}\label{nonempty}
2488
+ − 1466
\mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
2348
+ − 1467
\end{equation}
+ − 1468
+ − 1469
\noindent
+ − 1470
In this case we define a premise @{text P} using the relation
+ − 1471
$\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
+ − 1472
$\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other
+ − 1473
binding modes). This premise defines $\alpha$-equivalence of two abstractions
2349
+ − 1474
involving multiple binders. As above, we first build the tuples @{text "D"} and
2348
+ − 1475
@{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
+ − 1476
compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}).
2381
+ − 1477
For $\approx_{\,\textit{set}}$ we also need
2348
+ − 1478
a compound free-atom function for the bodies defined as
+ − 1479
%
+ − 1480
\begin{center}
+ − 1481
\mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
+ − 1482
\end{center}
+ − 1483
+ − 1484
\noindent
2381
+ − 1485
with the assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.
2348
+ − 1486
The last ingredient we need are the sets of atoms bound in the bodies.
+ − 1487
For this we take
+ − 1488
+ − 1489
\begin{center}
+ − 1490
@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\
1737
+ − 1491
\end{center}
+ − 1492
+ − 1493
\noindent
2348
+ − 1494
Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This
+ − 1495
lets us formally define the premise @{text P} for a non-empty binding clause as:
+ − 1496
%
2349
+ − 1497
\begin{center}
2471
+ − 1498
\mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
2349
+ − 1499
\end{center}
2348
+ − 1500
+ − 1501
\noindent
+ − 1502
This premise accounts for $\alpha$-equivalence of the bodies of the binding
2359
+ − 1503
clause.
2349
+ − 1504
However, in case the binders have non-recursive deep binders, this premise
+ − 1505
is not enough:
2348
+ − 1506
we also have to ``propagate'' $\alpha$-equivalence inside the structure of
+ − 1507
these binders. An example is @{text "Let"} where we have to make sure the
2359
+ − 1508
right-hand sides of assignments are $\alpha$-equivalent. For this we use
2348
+ − 1509
relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
+ − 1510
Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
+ − 1511
%
+ − 1512
\begin{center}
+ − 1513
@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
+ − 1514
\end{center}
+ − 1515
+ − 1516
\noindent
2359
+ − 1517
The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})
+ − 1518
and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}.
2349
+ − 1519
All premises for @{text "bc\<^isub>i"} are then given by
2348
+ − 1520
%
+ − 1521
\begin{center}
2359
+ − 1522
@{text "prems(bc\<^isub>i) \<equiv> P \<and> L R' L'"}
2348
+ − 1523
\end{center}
+ − 1524
2349
+ − 1525
\noindent
2359
+ − 1526
The auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
+ − 1527
in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form
2348
+ − 1528
%
+ − 1529
\begin{center}
+ − 1530
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
+ − 1531
\end{center}
+ − 1532
+ − 1533
\noindent
+ − 1534
where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
2359
+ − 1535
then the corresponding $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
2348
+ − 1536
%
+ − 1537
\begin{center}
+ − 1538
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
+ − 1539
{@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}
+ − 1540
\end{center}
+ − 1541
+ − 1542
\noindent
2349
+ − 1543
In this clause the relations @{text "R"}$_{1..s}$ are given by
2348
+ − 1544
+ − 1545
\begin{center}
+ − 1546
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ − 1547
$\bullet$ & @{text "z\<^isub>i \<approx>ty z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and
+ − 1548
is a recursive argument of @{text C},\\
+ − 1549
$\bullet$ & @{text "z\<^isub>i = z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs}
+ − 1550
and is a non-recursive argument of @{text C},\\
+ − 1551
$\bullet$ & @{text "z\<^isub>i \<approx>bn\<^isub>i z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs}
+ − 1552
with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\
+ − 1553
$\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a
+ − 1554
recursive call.
+ − 1555
\end{tabular}
+ − 1556
\end{center}
+ − 1557
+ − 1558
\noindent
+ − 1559
This completes the definition of $\alpha$-equivalence. As a sanity check, we can show
+ − 1560
that the premises of empty binding clauses are a special case of the clauses for
+ − 1561
non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
2349
+ − 1562
for the existentially quantified permutation).
2359
+ − 1563
+ − 1564
Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}
2348
+ − 1565
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
+ − 1566
$\approx_{\textit{bn}}$ with the following clauses:
1739
+ − 1567
+ − 1568
\begin{center}
+ − 1569
\begin{tabular}{@ {}c @ {}}
2350
+ − 1570
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
+ − 1571
{@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
2359
+ − 1572
\makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+ − 1573
{@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}
1739
+ − 1574
\end{tabular}
+ − 1575
\end{center}
+ − 1576
+ − 1577
\begin{center}
+ − 1578
\begin{tabular}{@ {}c @ {}}
2359
+ − 1579
\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\smallskip\\
1739
+ − 1580
\infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
1771
+ − 1581
{@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
1739
+ − 1582
\end{tabular}
+ − 1583
\end{center}
+ − 1584
+ − 1585
\begin{center}
+ − 1586
\begin{tabular}{@ {}c @ {}}
2359
+ − 1587
\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\smallskip\\
1739
+ − 1588
\infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
1771
+ − 1589
{@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
1739
+ − 1590
\end{tabular}
+ − 1591
\end{center}
+ − 1592
+ − 1593
\noindent
+ − 1594
Note the difference between $\approx_{\textit{assn}}$ and
2341
+ − 1595
$\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of
2359
+ − 1596
the components in an assignment that are \emph{not} bound. This is needed in the
+ − 1597
in the clause for @{text "Let"} (which is has
1771
+ − 1598
a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant
1765
+ − 1599
to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
2360
+ − 1600
because there all components of an assignment are ``under'' the binder.
1587
+ − 1601
*}
+ − 1602
1739
+ − 1603
section {* Establishing the Reasoning Infrastructure *}
1717
+ − 1604
+ − 1605
text {*
1766
+ − 1606
Having made all necessary definitions for raw terms, we can start
2361
+ − 1607
with establishing the reasoning infrastructure for the $\alpha$-equated types
+ − 1608
@{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch
+ − 1609
in this section the proofs we need for establishing this infrastructure. One
+ − 1610
main point of our work is that we have completely automated these proofs in Isabelle/HOL.
+ − 1611
+ − 1612
First we establish that the
2359
+ − 1613
$\alpha$-equivalence relations defined in the previous section are
1766
+ − 1614
equivalence relations.
1717
+ − 1615
1766
+ − 1616
\begin{lemma}\label{equiv}
2361
+ − 1617
Given the raw types @{text "ty"}$_{1..n}$ and binding functions
+ − 1618
@{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and
+ − 1619
@{text "\<approx>bn"}$_{1..m}$ are equivalence relations and equivariant.
1717
+ − 1620
\end{lemma}
1739
+ − 1621
+ − 1622
\begin{proof}
1752
+ − 1623
The proof is by mutual induction over the definitions. The non-trivial
2176
+ − 1624
cases involve premises built up by $\approx_{\textit{set}}$,
1739
+ − 1625
$\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They
1752
+ − 1626
can be dealt with as in Lemma~\ref{alphaeq}.
1739
+ − 1627
\end{proof}
1718
+ − 1628
1739
+ − 1629
\noindent
+ − 1630
We can feed this lemma into our quotient package and obtain new types @{text
2359
+ − 1631
"ty"}$^\alpha_{1..n}$ representing $\alpha$-equated terms of types @{text "ty"}$_{1..n}$.
+ − 1632
We also obtain definitions for the term-constructors @{text
2361
+ − 1633
"C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
+ − 1634
"C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
+ − 1635
"fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text
+ − 1636
"bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the
1775
+ − 1637
user, since they are given in terms of the isomorphisms we obtained by
1754
+ − 1638
creating new types in Isabelle/HOL (recall the picture shown in the
1739
+ − 1639
Introduction).
+ − 1640
2361
+ − 1641
The first useful property for the user is the fact that distinct
+ − 1642
term-constructors are not
+ − 1643
equal, that is
1760
+ − 1644
%
+ − 1645
\begin{equation}\label{distinctalpha}
2361
+ − 1646
\mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~%
+ − 1647
@{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}}
1760
+ − 1648
\end{equation}
+ − 1649
+ − 1650
\noindent
2361
+ − 1651
whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
+ − 1652
In order to derive this fact, we use the definition of $\alpha$-equivalence
+ − 1653
and establish that
1765
+ − 1654
%
+ − 1655
\begin{equation}\label{distinctraw}
2361
+ − 1656
\mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
1765
+ − 1657
\end{equation}
1760
+ − 1658
+ − 1659
\noindent
2361
+ − 1660
holds for the corresponding raw term-constructors.
+ − 1661
In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
+ − 1662
package needs to know that the raw term-constructors @{text "C"} and @{text "D"}
2341
+ − 1663
are \emph{respectful} w.r.t.~the $\alpha$-equivalence relations (see \cite{Homeier05}).
2361
+ − 1664
Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types
+ − 1665
@{text "ty"}$_{1..r}$, respectfulness amounts to showing that
2359
+ − 1666
%
1765
+ − 1667
\begin{center}
2361
+ − 1668
@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
1765
+ − 1669
\end{center}
+ − 1670
+ − 1671
\noindent
2361
+ − 1672
holds under the assumptions that we have \mbox{@{text
+ − 1673
"x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
+ − 1674
and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
+ − 1675
@{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
+ − 1676
implication by applying the corresponding rule in our $\alpha$-equivalence
+ − 1677
definition and by establishing the following auxiliary facts
1766
+ − 1678
%
+ − 1679
\begin{equation}\label{fnresp}
+ − 1680
\mbox{%
+ − 1681
\begin{tabular}{l}
2361
+ − 1682
@{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"}\\
+ − 1683
@{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"}\\
+ − 1684
@{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
+ − 1685
@{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
1766
+ − 1686
\end{tabular}}
+ − 1687
\end{equation}
1717
+ − 1688
1766
+ − 1689
\noindent
2361
+ − 1690
They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first,
+ − 1691
second and last implication are true by how we stated our definitions, the
+ − 1692
third \emph{only} holds because of our restriction
+ − 1693
imposed on the form of the binding functions---namely \emph{not} returning
+ − 1694
any bound atoms. In Ott, in contrast, the user may
+ − 1695
define @{text "bn"}$_{1..m}$ so that they return bound
+ − 1696
atoms and in this case the third implication is \emph{not} true. A
2363
+ − 1697
result is that the lifing of the corresponding binding functions in Ott to $\alpha$-equated
2361
+ − 1698
terms is impossible.
1766
+ − 1699
2361
+ − 1700
Having established respectfulness for the raw term-constructors, the
+ − 1701
quotient package is able to automatically deduce \eqref{distinctalpha} from
+ − 1702
\eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
+ − 1703
also lift properties that characterise when two raw terms of the form
+ − 1704
%
1718
+ − 1705
\begin{center}
2361
+ − 1706
@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
1766
+ − 1707
\end{center}
+ − 1708
+ − 1709
\noindent
2341
+ − 1710
are $\alpha$-equivalent. This gives us conditions when the corresponding
+ − 1711
$\alpha$-equated terms are \emph{equal}, namely
2361
+ − 1712
%
1766
+ − 1713
\begin{center}
2361
+ − 1714
@{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
1766
+ − 1715
\end{center}
+ − 1716
+ − 1717
\noindent
2361
+ − 1718
We call these conditions as \emph{quasi-injectivity}. They correspond to
+ − 1719
the premises in our $\alpha$-equivalence relations.
+ − 1720
+ − 1721
Next we can lift the permutation
+ − 1722
operations defined in \eqref{ceqvt}. In order to make this
+ − 1723
lifting to go through, we have to show that the permutation operations are respectful.
+ − 1724
This amounts to showing that the
+ − 1725
$\alpha$-equivalence relations are equivariant, which we already established
+ − 1726
in Lemma~\ref{equiv}. As a result we can add the equations
+ − 1727
%
+ − 1728
\begin{equation}\label{calphaeqvt}
+ − 1729
@{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}
+ − 1730
\end{equation}
+ − 1731
+ − 1732
\noindent
+ − 1733
to our infrastructure. In a similar fashion we can lift the defining equations
+ − 1734
of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
+ − 1735
@{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
2363
+ − 1736
"bn\<AL>"}$_{1..m}$ and the size functions @{text "size_ty\<AL>"}$_{1..n}$.
2361
+ − 1737
The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
+ − 1738
by the datatype package of Isabelle/HOL.
1766
+ − 1739
2361
+ − 1740
Finally we can add to our infrastructure a structural induction principle
+ − 1741
for the types @{text "ty\<AL>"}$_{i..n}$ whose
+ − 1742
conclusion of the form
+ − 1743
%
+ − 1744
\begin{equation}\label{weakinduct}
+ − 1745
\mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
+ − 1746
\end{equation}
1766
+ − 1747
2361
+ − 1748
\noindent
+ − 1749
whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$
+ − 1750
have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
+ − 1751
term constructor @{text "C"}$^\alpha$ a premise of the form
+ − 1752
%
+ − 1753
\begin{equation}\label{weakprem}
+ − 1754
\mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}}
+ − 1755
\end{equation}
+ − 1756
+ − 1757
\noindent
+ − 1758
in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are
+ − 1759
the recursive arguments of @{text "C\<AL>"}.
+ − 1760
+ − 1761
By working now completely on the $\alpha$-equated level, we
+ − 1762
can first show that the free-atom functions and binding functions are
+ − 1763
equivariant, namely
+ − 1764
%
1766
+ − 1765
\begin{center}
+ − 1766
\begin{tabular}{rcl}
2361
+ − 1767
@{text "p \<bullet> (fa_ty\<AL>\<^isub>i x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"}\\
+ − 1768
@{text "p \<bullet> (fa_bn\<AL>\<^isub>j x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\
+ − 1769
@{text "p \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}
1718
+ − 1770
\end{tabular}
+ − 1771
\end{center}
1717
+ − 1772
1766
+ − 1773
\noindent
2361
+ − 1774
These properties can be established using the induction principle
+ − 1775
in \eqref{weakinduct}.
+ − 1776
Having these equivariant properties established, we can
1766
+ − 1777
show for every term-constructor @{text "C\<^sup>\<alpha>"} that
+ − 1778
+ − 1779
\begin{center}
2363
+ − 1780
@{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
1766
+ − 1781
\end{center}
+ − 1782
+ − 1783
\noindent
2363
+ − 1784
holds. This together with Property~\ref{supportsprop} allows us to prove
+ − 1785
that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported,
2361
+ − 1786
namely @{text "finite (supp x)"}. This can be again shown by induction
+ − 1787
over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of
+ − 1788
elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
2363
+ − 1789
This fact is important in a nominal setting, but also provides evidence
+ − 1790
that our notions of free-atoms and $\alpha$-equivalence are correct.
1766
+ − 1791
1767
+ − 1792
\begin{lemma}
2361
+ − 1793
For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have
+ − 1794
@{text "supp x = fa_ty\<AL>\<^isub>i x"}.
1722
+ − 1795
\end{lemma}
1766
+ − 1796
1722
+ − 1797
\begin{proof}
2361
+ − 1798
The proof is by induction. In each case
1766
+ − 1799
we unfold the definition of @{text "supp"}, move the swapping inside the
2361
+ − 1800
term-constructors and then use the quasi-injectivity lemmas in order to complete the
1770
+ − 1801
proof. For the abstraction cases we use the facts derived in Theorem~\ref{suppabs}.
1722
+ − 1802
\end{proof}
1721
+ − 1803
1766
+ − 1804
\noindent
2363
+ − 1805
To sum up this section, we can established automatically a reasoning infrastructure
2361
+ − 1806
for the types @{text "ty\<AL>"}$_{1..n}$
1766
+ − 1807
by first lifting definitions from the raw level to the quotient level and
2361
+ − 1808
then by establishing facts about these lifted definitions. All necessary proofs
1770
+ − 1809
are generated automatically by custom ML-code. This code can deal with
2363
+ − 1810
specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
1728
+ − 1811
1766
+ − 1812
\begin{figure}[t!]
+ − 1813
\begin{boxedminipage}{\linewidth}
+ − 1814
\small
+ − 1815
\begin{tabular}{l}
2361
+ − 1816
\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
1766
+ − 1817
\isacommand{nominal\_datatype}~@{text "tkind ="}\\
+ − 1818
\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
+ − 1819
\isacommand{and}~@{text "ckind ="}\\
+ − 1820
\phantom{$|$}~@{text "CKSim ty ty"}\\
+ − 1821
\isacommand{and}~@{text "ty ="}\\
+ − 1822
\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
+ − 1823
$|$~@{text "TFun string ty_list"}~%
+ − 1824
$|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+ − 1825
$|$~@{text "TArr ckind ty"}\\
+ − 1826
\isacommand{and}~@{text "ty_lst ="}\\
+ − 1827
\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
+ − 1828
\isacommand{and}~@{text "cty ="}\\
+ − 1829
\phantom{$|$}~@{text "CVar cvar"}~%
+ − 1830
$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
+ − 1831
$|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+ − 1832
$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
+ − 1833
$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
+ − 1834
$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
+ − 1835
\isacommand{and}~@{text "co_lst ="}\\
+ − 1836
\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
+ − 1837
\isacommand{and}~@{text "trm ="}\\
+ − 1838
\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
+ − 1839
$|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
+ − 1840
$|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
+ − 1841
$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
+ − 1842
$|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
+ − 1843
$|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
+ − 1844
$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
+ − 1845
\isacommand{and}~@{text "assoc_lst ="}\\
+ − 1846
\phantom{$|$}~@{text ANil}~%
+ − 1847
$|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+ − 1848
\isacommand{and}~@{text "pat ="}\\
+ − 1849
\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
+ − 1850
\isacommand{and}~@{text "vt_lst ="}\\
+ − 1851
\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
+ − 1852
\isacommand{and}~@{text "tvtk_lst ="}\\
+ − 1853
\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
+ − 1854
\isacommand{and}~@{text "tvck_lst ="}\\
+ − 1855
\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
+ − 1856
\isacommand{binder}\\
+ − 1857
@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
+ − 1858
@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+ − 1859
@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
+ − 1860
@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
+ − 1861
\isacommand{where}\\
+ − 1862
\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
+ − 1863
$|$~@{text "bv1 VTNil = []"}\\
+ − 1864
$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
+ − 1865
$|$~@{text "bv2 TVTKNil = []"}\\
+ − 1866
$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
+ − 1867
$|$~@{text "bv3 TVCKNil = []"}\\
+ − 1868
$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
+ − 1869
\end{tabular}
+ − 1870
\end{boxedminipage}
1890
+ − 1871
\caption{The nominal datatype declaration for Core-Haskell. For the moment we
1766
+ − 1872
do not support nested types; therefore we explicitly have to unfold the
+ − 1873
lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
+ − 1874
in a future version of Nominal Isabelle. Apart from that, the
+ − 1875
declaration follows closely the original in Figure~\ref{corehas}. The
+ − 1876
point of our work is that having made such a declaration in Nominal Isabelle,
+ − 1877
one obtains automatically a reasoning infrastructure for Core-Haskell.
+ − 1878
\label{nominalcorehas}}
+ − 1879
\end{figure}
+ − 1880
*}
1728
+ − 1881
1587
+ − 1882
1747
+ − 1883
section {* Strong Induction Principles *}
+ − 1884
+ − 1885
text {*
1764
+ − 1886
In the previous section we were able to provide induction principles that
2341
+ − 1887
allow us to perform structural inductions over $\alpha$-equated terms.
2363
+ − 1888
We call such induction principles \emph{weak}, because in case of the
+ − 1889
term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
2361
+ − 1890
the induction hypothesis requires us to establish the implications \eqref{weakprem}.
2363
+ − 1891
The problem with these implications is that in general they are difficult to establish.
1771
+ − 1892
The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}
1770
+ − 1893
(for example we cannot assume the variable convention for them).
1764
+ − 1894
+ − 1895
In \cite{UrbanTasson05} we introduced a method for automatically
+ − 1896
strengthening weak induction principles for terms containing single
1768
+ − 1897
binders. These stronger induction principles allow the user to make additional
1771
+ − 1898
assumptions about binders.
1768
+ − 1899
These additional assumptions amount to a formal
+ − 1900
version of the informal variable convention for binders. A natural question is
+ − 1901
whether we can also strengthen the weak induction principles involving
1771
+ − 1902
the general binders presented here. We will indeed be able to so, but for this we need an
1770
+ − 1903
additional notion for permuting deep binders.
1764
+ − 1904
1768
+ − 1905
Given a binding function @{text "bn"} we define an auxiliary permutation
1764
+ − 1906
operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
2363
+ − 1907
Assuming a clause of @{text bn} is given as
+ − 1908
%
+ − 1909
\begin{center}
+ − 1910
@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"},
+ − 1911
\end{center}
+ − 1912
+ − 1913
\noindent
+ − 1914
then we define
+ − 1915
%
+ − 1916
\begin{center}
+ − 1917
@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}
+ − 1918
\end{center}
+ − 1919
+ − 1920
\noindent
+ − 1921
with @{text "y\<^isub>i"} determined as follows:
1764
+ − 1922
%
+ − 1923
\begin{center}
+ − 1924
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ − 1925
$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
+ − 1926
$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+ − 1927
$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
+ − 1928
\end{tabular}
+ − 1929
\end{center}
+ − 1930
+ − 1931
\noindent
1771
+ − 1932
Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
2341
+ − 1933
$\alpha$-equated terms. We can then prove the following two facts
1764
+ − 1934
1770
+ − 1935
\begin{lemma}\label{permutebn}
+ − 1936
Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
2363
+ − 1937
{\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
+ − 1938
@{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
1764
+ − 1939
\end{lemma}
+ − 1940
+ − 1941
\begin{proof}
1771
+ − 1942
By induction on @{text x}. The equations follow by simple unfolding
1764
+ − 1943
of the definitions.
+ − 1944
\end{proof}
+ − 1945
1769
+ − 1946
\noindent
1768
+ − 1947
The first property states that a permutation applied to a binding function is
+ − 1948
equivalent to first permuting the binders and then calculating the bound
2347
+ − 1949
atoms. The second amounts to the fact that permuting the binders has no
+ − 1950
effect on the free-atom function. The main point of this permutation
1769
+ − 1951
function, however, is that if we have a permutation that is fresh
+ − 1952
for the support of an object @{text x}, then we can use this permutation
1770
+ − 1953
to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
1769
+ − 1954
@{text "Let"} term-constructor from the example shown
2363
+ − 1955
in \eqref{letpat} this means for a permutation @{text "r"}
1770
+ − 1956
%
+ − 1957
\begin{equation}\label{renaming}
1771
+ − 1958
\begin{array}{l}
+ − 1959
\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\
2363
+ − 1960
\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
1771
+ − 1961
\end{array}
1770
+ − 1962
\end{equation}
1769
+ − 1963
+ − 1964
\noindent
2363
+ − 1965
This fact will be crucial when establishing the strong induction principles below.
+ − 1966
+ − 1967
+ − 1968
In our running example about @{text "Let"}, the strong induction
+ − 1969
principle means that instead
1770
+ − 1970
of establishing the implication
2361
+ − 1971
%
1764
+ − 1972
\begin{center}
1771
+ − 1973
@{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
1764
+ − 1974
\end{center}
+ − 1975
+ − 1976
\noindent
1769
+ − 1977
it is sufficient to establish the following implication
1770
+ − 1978
%
+ − 1979
\begin{equation}\label{strong}
+ − 1980
\mbox{\begin{tabular}{l}
1771
+ − 1981
@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
+ − 1982
\hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
+ − 1983
\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
+ − 1984
\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
1770
+ − 1985
\end{tabular}}
+ − 1986
\end{equation}
+ − 1987
+ − 1988
\noindent
+ − 1989
While this implication contains an additional argument, namely @{text c}, and
+ − 1990
also additional universal quantifications, it is usually easier to establish.
2363
+ − 1991
The reason is that we have the freshness
1770
+ − 1992
assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily
+ − 1993
chosen by the user as long as it has finite support.
+ − 1994
+ − 1995
Let us now show how we derive the strong induction principles from the
+ − 1996
weak ones. In case of the @{text "Let"}-example we derive by the weak
+ − 1997
induction the following two properties
+ − 1998
%
+ − 1999
\begin{equation}\label{hyps}
+ − 2000
@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm}
2363
+ − 2001
@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
1770
+ − 2002
\end{equation}
+ − 2003
+ − 2004
\noindent
1771
+ − 2005
For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}
+ − 2006
assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}).
+ − 2007
By Property~\ref{avoiding} we
1770
+ − 2008
obtain a permutation @{text "r"} such that
+ − 2009
%
+ − 2010
\begin{equation}\label{rprops}
+ − 2011
@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
1771
+ − 2012
@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
1770
+ − 2013
\end{equation}
+ − 2014
+ − 2015
\noindent
+ − 2016
hold. The latter fact and \eqref{renaming} give us
2361
+ − 2017
%
1765
+ − 2018
\begin{center}
1771
+ − 2019
\begin{tabular}{l}
+ − 2020
@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
2363
+ − 2021
\hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
1771
+ − 2022
\end{tabular}
1770
+ − 2023
\end{center}
+ − 2024
+ − 2025
\noindent
2176
+ − 2026
So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
2363
+ − 2027
establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
1770
+ − 2028
To do so, we will use the implication \eqref{strong} of the strong induction
+ − 2029
principle, which requires us to discharge
1771
+ − 2030
the following four proof obligations:
2361
+ − 2031
%
1770
+ − 2032
\begin{center}
+ − 2033
\begin{tabular}{rl}
2363
+ − 2034
{\it (i)} & @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
+ − 2035
{\it (ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
+ − 2036
{\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
+ − 2037
{\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
1765
+ − 2038
\end{tabular}
+ − 2039
\end{center}
1764
+ − 2040
1770
+ − 2041
\noindent
2363
+ − 2042
The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the
1771
+ − 2043
others from the induction hypotheses in \eqref{hyps} (in the fourth case
+ − 2044
we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
1748
+ − 2045
1770
+ − 2046
Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
+ − 2047
we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
2363
+ − 2048
This completes the proof showing that the weak induction principles imply
+ − 2049
the strong induction principles.
1747
+ − 2050
*}
+ − 2051
1702
+ − 2052
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
+ − 2053
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
+ − 2054
1570
+ − 2055
text {*
2342
+ − 2056
To our knowledge the earliest usage of general binders in a theorem prover
1760
+ − 2057
is described in \cite{NaraschewskiNipkow99} about a formalisation of the
2361
+ − 2058
algorithm W. This formalisation implements binding in type-schemes using a
+ − 2059
de-Bruijn indices representation. Since type-schemes in W contain only a single
2360
+ − 2060
place where variables are bound, different indices do not refer to different binders (as in the usual
1760
+ − 2061
de-Bruijn representation), but to different bound variables. A similar idea
+ − 2062
has been recently explored for general binders in the locally nameless
1764
+ − 2063
approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist
1760
+ − 2064
of two numbers, one referring to the place where a variable is bound and the
+ − 2065
other to which variable is bound. The reasoning infrastructure for both
2163
+ − 2066
representations of bindings comes for free in theorem provers like Isabelle/HOL or
2342
+ − 2067
Coq, since the corresponding term-calculi can be implemented as ``normal''
1764
+ − 2068
datatypes. However, in both approaches it seems difficult to achieve our
+ − 2069
fine-grained control over the ``semantics'' of bindings (i.e.~whether the
+ − 2070
order of binders should matter, or vacuous binders should be taken into
+ − 2071
account). To do so, one would require additional predicates that filter out
2163
+ − 2072
unwanted terms. Our guess is that such predicates result in rather
1764
+ − 2073
intricate formal reasoning.
1740
+ − 2074
+ − 2075
Another representation technique for binding is higher-order abstract syntax
1764
+ − 2076
(HOAS), which for example is implemented in the Twelf system. This representation
1760
+ − 2077
technique supports very elegantly many aspects of \emph{single} binding, and
2342
+ − 2078
impressive work has been done that uses HOAS for mechanising the metatheory
1764
+ − 2079
of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
+ − 2080
binders of SML are represented in this work. Judging from the submitted
+ − 2081
Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
+ − 2082
binding constructs where the number of bound variables is not fixed. For
+ − 2083
example in the second part of this challenge, @{text "Let"}s involve
+ − 2084
patterns that bind multiple variables at once. In such situations, HOAS
+ − 2085
representations have to resort to the iterated-single-binders-approach with
+ − 2086
all the unwanted consequences when reasoning about the resulting terms.
1740
+ − 2087
2362
+ − 2088
Two formalisations involving general binders have been
2360
+ − 2089
performed in older
2342
+ − 2090
versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
2163
+ − 2091
\cite{BengtsonParow09, UrbanNipkow09}). Both
1764
+ − 2092
use the approach based on iterated single binders. Our experience with
+ − 2093
the latter formalisation has been disappointing. The major pain arose from
+ − 2094
the need to ``unbind'' variables. This can be done in one step with our
2363
+ − 2095
general binders described in this paper, but needs a cumbersome
1764
+ − 2096
iteration with single binders. The resulting formal reasoning turned out to
+ − 2097
be rather unpleasant. The hope is that the extension presented in this paper
+ − 2098
is a substantial improvement.
1726
+ − 2099
2163
+ − 2100
The most closely related work to the one presented here is the Ott-tool
+ − 2101
\cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty
+ − 2102
front-end for creating \LaTeX{} documents from specifications of
2343
+ − 2103
term-calculi involving general binders. For a subset of the specifications
2163
+ − 2104
Ott can also generate theorem prover code using a raw representation of
+ − 2105
terms, and in Coq also a locally nameless representation. The developers of
+ − 2106
this tool have also put forward (on paper) a definition for
2341
+ − 2107
$\alpha$-equivalence of terms that can be specified in Ott. This definition is
2163
+ − 2108
rather different from ours, not using any nominal techniques. To our
+ − 2109
knowledge there is also no concrete mathematical result concerning this
2341
+ − 2110
notion of $\alpha$-equivalence. A definition for the notion of free variables
2362
+ − 2111
is work in progress in Ott.
2163
+ − 2112
2362
+ − 2113
Although we were heavily inspired by the syntax in Ott,
+ − 2114
its definition of $\alpha$-equivalence is unsuitable for our extension of
1760
+ − 2115
Nominal Isabelle. First, it is far too complicated to be a basis for
+ − 2116
automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
+ − 2117
covers cases of binders depending on other binders, which just do not make
2341
+ − 2118
sense for our $\alpha$-equated terms. Third, it allows empty types that have no
2363
+ − 2119
meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's
2163
+ − 2120
binding clauses. In Ott you specify binding clauses with a single body; we
+ − 2121
allow more than one. We have to do this, because this makes a difference
2488
+ − 2122
for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and
+ − 2123
\isacommand{bind (res)}. Consider the examples
2163
+ − 2124
+ − 2125
\begin{center}
2341
+ − 2126
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
+ − 2127
@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
2488
+ − 2128
\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
2341
+ − 2129
@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &
2488
+ − 2130
\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"},
+ − 2131
\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
2163
+ − 2132
\end{tabular}
+ − 2133
\end{center}
+ − 2134
+ − 2135
\noindent
2363
+ − 2136
In the first term-constructor we have a single
2362
+ − 2137
body that happens to be ``spread'' over two arguments; in the second term-constructor we have
+ − 2138
two independent bodies in which the same variables are bound. As a result we
2341
+ − 2139
have
+ − 2140
+ − 2141
\begin{center}
+ − 2142
\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+ − 2143
@{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
+ − 2144
@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
+ − 2145
@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
+ − 2146
@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
+ − 2147
\end{tabular}
+ − 2148
\end{center}
+ − 2149
2362
+ − 2150
\noindent
+ − 2151
and therefore need the extra generality to be able to distinguish between
+ − 2152
both specifications.
+ − 2153
Because of how we set up our definitions, we also had to impose some restrictions
+ − 2154
(like a single binding function for a deep binder) that are not present in Ott. Our
1764
+ − 2155
expectation is that we can still cover many interesting term-calculi from
2362
+ − 2156
programming language research, for example Core-Haskell.
2163
+ − 2157
+ − 2158
Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for
+ − 2159
representing terms with general binders inside OCaml. This language is
2362
+ − 2160
implemented as a front-end that can be translated to OCaml with the help of
2163
+ − 2161
a library. He presents a type-system in which the scope of general binders
2362
+ − 2162
can be specified using special markers, written @{text "inner"} and
+ − 2163
@{text "outer"}. It seems our and his specifications can be
+ − 2164
inter-translated as long as ours use the binding mode
+ − 2165
\isacommand{bind} only.
+ − 2166
However, we have not proved this. Pottier gives a definition for
+ − 2167
$\alpha$-equivalence, which also uses a permutation operation (like ours).
+ − 2168
Still, this definition is rather different from ours and he only proves that
+ − 2169
it defines an equivalence relation. A complete
2163
+ − 2170
reasoning infrastructure is well beyond the purposes of his language.
2362
+ − 2171
2218
+ − 2172
In a slightly different domain (programming with dependent types), the
+ − 2173
paper \cite{Altenkirch10} presents a calculus with a notion of
2488
+ − 2174
$\alpha$-equivalence related to our binding mode \isacommand{bind (res)}.
2363
+ − 2175
The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
2218
+ − 2176
has a more operational flavour and calculates a partial (renaming) map.
2363
+ − 2177
In this way, the definition can deal with vacuous binders. However, to our
+ − 2178
best knowledge, no concrete mathematical result concerning this
+ − 2179
definition of $\alpha$-equivalence has been proved.
1739
+ − 2180
*}
+ − 2181
1493
+ − 2182
section {* Conclusion *}
1485
+ − 2183
+ − 2184
text {*
2362
+ − 2185
We have presented an extension of Nominal Isabelle for dealing with
+ − 2186
general binders, that is term-constructors having multiple bound
2381
+ − 2187
variables. For this extension we introduced new definitions of
2362
+ − 2188
$\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
2364
+ − 2189
To specify general binders we used the specifications from Ott, but extended them
+ − 2190
in some places and restricted
2488
+ − 2191
them in others so that they make sense in the context of $\alpha$-equated terms. We also introduced two binding modes (set and res) that do not
+ − 2192
exist in Ott.
2363
+ − 2193
We have tried out the extension with terms from Core-Haskell, type-schemes
+ − 2194
and the lambda-calculus, and our code
+ − 2195
will eventually become part of the next Isabelle distribution.\footnote{For the moment
1764
+ − 2196
it can be downloaded from the Mercurial repository linked at
1741
+ − 2197
\href{http://isabelle.in.tum.de/nominal/download}
2361
+ − 2198
{http://isabelle.in.tum.de/nominal/download}.}
1741
+ − 2199
1764
+ − 2200
We have left out a discussion about how functions can be defined over
2362
+ − 2201
$\alpha$-equated terms involving general binders. In earlier versions of Nominal
1764
+ − 2202
Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue. We
+ − 2203
hope to do better this time by using the function package that has recently
+ − 2204
been implemented in Isabelle/HOL and also by restricting function
+ − 2205
definitions to equivariant functions (for such functions it is possible to
+ − 2206
provide more automation).
1741
+ − 2207
2363
+ − 2208
There are some restrictions we imposed in this paper that we would like to lift in
1764
+ − 2209
future work. One is the exclusion of nested datatype definitions. Nested
+ − 2210
datatype definitions allow one to specify, for instance, the function kinds
+ − 2211
in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
2362
+ − 2212
version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
+ − 2213
achieve this, we need a slightly more clever implementation than we have at the moment.
1764
+ − 2214
2362
+ − 2215
A more interesting line of investigation is whether we can go beyond the
2363
+ − 2216
simple-minded form of binding functions that we adopted from Ott. At the moment, binding
1764
+ − 2217
functions can only return the empty set, a singleton atom set or unions
+ − 2218
of atom sets (similarly for lists). It remains to be seen whether
2361
+ − 2219
properties like
+ − 2220
%
+ − 2221
\begin{center}
+ − 2222
@{text "fa_ty x = bn x \<union> fa_bn x"}.
+ − 2223
\end{center}
+ − 2224
+ − 2225
\noindent
2362
+ − 2226
allow us to support more interesting binding functions.
1726
+ − 2227
1763
+ − 2228
We have also not yet played with other binding modes. For example we can
2361
+ − 2229
imagine that there is need for a binding mode
1796
5165c350ee1a
clarified comment about distinct lists in th efuture work section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2230
where instead of lists, we abstract lists of distinct elements.
5165c350ee1a
clarified comment about distinct lists in th efuture work section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2231
Once we feel confident about such binding modes, our implementation
1764
+ − 2232
can be easily extended to accommodate them.
1763
+ − 2233
2362
+ − 2234
\medskip
+ − 2235
\noindent
+ − 2236
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
+ − 2237
many discussions about Nominal Isabelle. We also thank Peter Sewell for
+ − 2238
making the informal notes \cite{SewellBestiary} available to us and
+ − 2239
also for patiently explaining some of the finer points of the work on the Ott-tool.
+ − 2240
Stephanie Weirich suggested to separate the subgrammars
+ − 2241
of kinds and types in our Core-Haskell example.
2341
+ − 2242
754
+ − 2243
*}
+ − 2244
+ − 2245
(*<*)
+ − 2246
end
1704
+ − 2247
(*>*)