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