754
+ − 1
(*<*)
+ − 2
theory Paper
1506
+ − 3
imports "../Nominal/Test" "LaTeXsugar"
754
+ − 4
begin
1493
+ − 5
1657
+ − 6
consts
+ − 7
fv :: "'a \<Rightarrow> 'b"
+ − 8
abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
+ − 9
+ − 10
definition
+ − 11
"equal \<equiv> (op =)"
+ − 12
1493
+ − 13
notation (latex output)
+ − 14
swap ("'(_ _')" [1000, 1000] 1000) and
+ − 15
fresh ("_ # _" [51, 51] 50) and
1694
+ − 16
fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
1493
+ − 17
supp ("supp _" [78] 73) and
+ − 18
uminus ("-_" [78] 73) and
1657
+ − 19
If ("if _ then _ else _" 10) and
1662
+ − 20
alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_,_,_\<^esup> _") and
+ − 21
alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_,_,_\<^esup> _") and
+ − 22
alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and
1657
+ − 23
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
+ − 24
fv ("fv'(_')" [100] 100) and
+ − 25
equal ("=") and
+ − 26
alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
1703
+ − 27
Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and
1657
+ − 28
Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
1690
+ − 29
Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
1703
+ − 30
Cons ("_::_" [78,77] 73) and
+ − 31
supp_gen ("aux _" [1000] 100)
754
+ − 32
(*>*)
+ − 33
1657
+ − 34
754
+ − 35
section {* Introduction *}
+ − 36
+ − 37
text {*
1524
+ − 38
So far, Nominal Isabelle provides a mechanism for constructing
1607
+ − 39
alpha-equated terms, for example
1485
+ − 40
1520
+ − 41
\begin{center}
1657
+ − 42
@{text "t ::= x | t t | \<lambda>x. t"}
1520
+ − 43
\end{center}
+ − 44
+ − 45
\noindent
1687
+ − 46
where free and bound variables have names. For such alpha-equated terms, Nominal Isabelle
1657
+ − 47
derives automatically a reasoning infrastructure that has been used
1550
+ − 48
successfully in formalisations of an equivalence checking algorithm for LF
+ − 49
\cite{UrbanCheneyBerghofer08}, Typed
1520
+ − 50
Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
1694
+ − 51
\cite{BengtsonParow09} and a strong normalisation result
1520
+ − 52
for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
+ − 53
used by Pollack for formalisations in the locally-nameless approach to
+ − 54
binding \cite{SatoPollack10}.
+ − 55
1535
+ − 56
However, Nominal Isabelle has fared less well in a formalisation of
1690
+ − 57
the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are,
+ − 58
respectively, of the form
1570
+ − 59
%
+ − 60
\begin{equation}\label{tysch}
+ − 61
\begin{array}{l}
1657
+ − 62
@{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}
+ − 63
@{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
1570
+ − 64
\end{array}
+ − 65
\end{equation}
1520
+ − 66
+ − 67
\noindent
1566
+ − 68
and the quantification $\forall$ binds a finite (possibly empty) set of
1550
+ − 69
type-variables. While it is possible to implement this kind of more general
+ − 70
binders by iterating single binders, this leads to a rather clumsy
+ − 71
formalisation of W. The need of iterating single binders is also one reason
+ − 72
why Nominal Isabelle and similar theorem provers that only provide
+ − 73
mechanisms for binding single variables have not fared extremely well with the
+ − 74
more advanced tasks in the POPLmark challenge \cite{challenge05}, because
+ − 75
also there one would like to bind multiple variables at once.
1520
+ − 76
1577
+ − 77
Binding multiple variables has interesting properties that cannot be captured
1587
+ − 78
easily by iterating single binders. For example in case of type-schemes we do not
+ − 79
want to make a distinction about the order of the bound variables. Therefore
1550
+ − 80
we would like to regard the following two type-schemes as alpha-equivalent
1572
+ − 81
%
+ − 82
\begin{equation}\label{ex1}
1667
+ − 83
@{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"}
1572
+ − 84
\end{equation}
1520
+ − 85
+ − 86
\noindent
1657
+ − 87
but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
1587
+ − 88
the following two should \emph{not} be alpha-equivalent
1572
+ − 89
%
+ − 90
\begin{equation}\label{ex2}
1667
+ − 91
@{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
1572
+ − 92
\end{equation}
1520
+ − 93
+ − 94
\noindent
1657
+ − 95
Moreover, we like to regard type-schemes as alpha-equivalent, if they differ
+ − 96
only on \emph{vacuous} binders, such as
1572
+ − 97
%
+ − 98
\begin{equation}\label{ex3}
1667
+ − 99
@{text "\<forall>{x}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{x, z}. x \<rightarrow> y"}
1572
+ − 100
\end{equation}
1485
+ − 101
1520
+ − 102
\noindent
1657
+ − 103
where @{text z} does not occur freely in the type. In this paper we will
+ − 104
give a general binding mechanism and associated notion of alpha-equivalence
+ − 105
that can be used to faithfully represent this kind of binding in Nominal
+ − 106
Isabelle. The difficulty of finding the right notion for alpha-equivalence
+ − 107
can be appreciated in this case by considering that the definition given by
+ − 108
Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
1524
+ − 109
1657
+ − 110
However, the notion of alpha-equivalence that is preserved by vacuous
+ − 111
binders is not always wanted. For example in terms like
1587
+ − 112
%
1535
+ − 113
\begin{equation}\label{one}
1657
+ − 114
@{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}
1535
+ − 115
\end{equation}
1520
+ − 116
+ − 117
\noindent
1524
+ − 118
we might not care in which order the assignments $x = 3$ and $y = 2$ are
1535
+ − 119
given, but it would be unusual to regard \eqref{one} as alpha-equivalent
1524
+ − 120
with
1587
+ − 121
%
1520
+ − 122
\begin{center}
1657
+ − 123
@{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}
1520
+ − 124
\end{center}
+ − 125
+ − 126
\noindent
1550
+ − 127
Therefore we will also provide a separate binding mechanism for cases in
+ − 128
which the order of binders does not matter, but the ``cardinality'' of the
1535
+ − 129
binders has to agree.
1520
+ − 130
1550
+ − 131
However, we found that this is still not sufficient for dealing with
+ − 132
language constructs frequently occurring in programming language
1690
+ − 133
research. For example in @{text "\<LET>"}s containing patterns like
1587
+ − 134
%
1535
+ − 135
\begin{equation}\label{two}
1657
+ − 136
@{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}
1535
+ − 137
\end{equation}
1520
+ − 138
+ − 139
\noindent
1535
+ − 140
we want to bind all variables from the pattern inside the body of the
+ − 141
$\mathtt{let}$, but we also care about the order of these variables, since
1566
+ − 142
we do not want to regard \eqref{two} as alpha-equivalent with
1587
+ − 143
%
1520
+ − 144
\begin{center}
1657
+ − 145
@{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
1520
+ − 146
\end{center}
+ − 147
+ − 148
\noindent
1657
+ − 149
As a result, we provide three general binding mechanisms each of which binds
+ − 150
multiple variables at once, and let the user chose which one is intended
+ − 151
when formalising a programming language calculus.
1485
+ − 152
1657
+ − 153
By providing these general binding mechanisms, however, we have to work
+ − 154
around a problem that has been pointed out by Pottier \cite{Pottier06} and
+ − 155
Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form
1587
+ − 156
%
1520
+ − 157
\begin{center}
1657
+ − 158
@{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}
1520
+ − 159
\end{center}
+ − 160
+ − 161
\noindent
1657
+ − 162
which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care
+ − 163
about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given,
+ − 164
but we do care about the information that there are as many @{text
+ − 165
"x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if
+ − 166
we represent the @{text "\<LET>"}-constructor by something like
1587
+ − 167
%
1523
+ − 168
\begin{center}
1657
+ − 169
@{text "\<LET> [x\<^isub>1,\<dots>,x\<^isub>n].s [t\<^isub>1,\<dots>,t\<^isub>n]"}
1523
+ − 170
\end{center}
1520
+ − 171
1523
+ − 172
\noindent
1703
+ − 173
where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}
+ − 174
becomes bound in @{text s}. In this representation the term
1690
+ − 175
\mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
1687
+ − 176
instance, but the lengths of two lists do not agree. To exclude such terms,
+ − 177
additional predicates about well-formed
1657
+ − 178
terms are needed in order to ensure that the two lists are of equal
+ − 179
length. This can result into very messy reasoning (see for
+ − 180
example~\cite{BengtsonParow09}). To avoid this, we will allow type
+ − 181
specifications for $\mathtt{let}$s as follows
1587
+ − 182
%
1528
+ − 183
\begin{center}
+ − 184
\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
1657
+ − 185
@{text trm} & @{text "::="} & @{text "\<dots>"}\\
+ − 186
& @{text "|"} & @{text "\<LET> a::assn s::trm"}\hspace{4mm}
+ − 187
\isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}\\[1mm]
+ − 188
@{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
+ − 189
& @{text "|"} & @{text "\<ACONS> name trm assn"}
1528
+ − 190
\end{tabular}
+ − 191
\end{center}
+ − 192
+ − 193
\noindent
1657
+ − 194
where @{text assn} is an auxiliary type representing a list of assignments
+ − 195
and @{text bn} an auxiliary function identifying the variables to be bound
1687
+ − 196
by the @{text "\<LET>"}. This function can be defined by recursion over @{text
1657
+ − 197
assn} as follows
1528
+ − 198
+ − 199
\begin{center}
1657
+ − 200
@{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm}
+ − 201
@{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"}
1528
+ − 202
\end{center}
1523
+ − 203
1528
+ − 204
\noindent
1550
+ − 205
The scope of the binding is indicated by labels given to the types, for
1657
+ − 206
example @{text "s::trm"}, and a binding clause, in this case
+ − 207
\isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}, that states
+ − 208
to bind in @{text s} all the names the function call @{text "bn(a)"} returns.
+ − 209
This style of specifying terms and bindings is heavily inspired by the
+ − 210
syntax of the Ott-tool \cite{ott-jfp}.
+ − 211
1528
+ − 212
1545
+ − 213
However, we will not be able to deal with all specifications that are
1617
+ − 214
allowed by Ott. One reason is that Ott lets the user to specify ``empty''
+ − 215
types like
1570
+ − 216
+ − 217
\begin{center}
1657
+ − 218
@{text "t ::= t t | \<lambda>x. t"}
1570
+ − 219
\end{center}
+ − 220
+ − 221
\noindent
1617
+ − 222
where no clause for variables is given. Arguably, such specifications make
+ − 223
some sense in the context of Coq's type theory (which Ott supports), but not
+ − 224
at all in a HOL-based environment where every datatype must have a non-empty
+ − 225
set-theoretic model.
1570
+ − 226
+ − 227
Another reason is that we establish the reasoning infrastructure
+ − 228
for alpha-\emph{equated} terms. In contrast, Ott produces a reasoning
+ − 229
infrastructure in Isabelle/HOL for
1545
+ − 230
\emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
1556
+ − 231
and the raw terms produced by Ott use names for bound variables,
1690
+ − 232
there is a key difference: working with alpha-equated terms means, for example,
1693
+ − 233
that the two type-schemes
1528
+ − 234
+ − 235
\begin{center}
1667
+ − 236
@{text "\<forall>{x}. x \<rightarrow> y = \<forall>{x, z}. x \<rightarrow> y"}
1528
+ − 237
\end{center}
+ − 238
+ − 239
\noindent
1703
+ − 240
are not just alpha-equal, but actually \emph{equal}! As a result, we can
1657
+ − 241
only support specifications that make sense on the level of alpha-equated
+ − 242
terms (offending specifications, which for example bind a variable according
+ − 243
to a variable bound somewhere else, are not excluded by Ott, but we have
1687
+ − 244
to).
+ − 245
+ − 246
Our insistence on reasoning with alpha-equated terms comes from the
1657
+ − 247
wealth of experience we gained with the older version of Nominal Isabelle:
+ − 248
for non-trivial properties, reasoning about alpha-equated terms is much
+ − 249
easier than reasoning with raw terms. The fundamental reason for this is
+ − 250
that the HOL-logic underlying Nominal Isabelle allows us to replace
+ − 251
``equals-by-equals''. In contrast, replacing
+ − 252
``alpha-equals-by-alpha-equals'' in a representation based on raw terms
+ − 253
requires a lot of extra reasoning work.
1535
+ − 254
1657
+ − 255
Although in informal settings a reasoning infrastructure for alpha-equated
+ − 256
terms is nearly always taken for granted, establishing it automatically in
+ − 257
the Isabelle/HOL theorem prover is a rather non-trivial task. For every
+ − 258
specification we will need to construct a type containing as elements the
+ − 259
alpha-equated terms. To do so, we use the standard HOL-technique of defining
+ − 260
a new type by identifying a non-empty subset of an existing type. The
1667
+ − 261
construction we perform in Isabelle/HOL can be illustrated by the following picture:
1657
+ − 262
1528
+ − 263
\begin{center}
1552
+ − 264
\begin{tikzpicture}
+ − 265
%\draw[step=2mm] (-4,-1) grid (4,1);
+ − 266
+ − 267
\draw[very thick] (0.7,0.4) circle (4.25mm);
+ − 268
\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);
+ − 269
\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);
+ − 270
+ − 271
\draw (-2.0, 0.845) -- (0.7,0.845);
+ − 272
\draw (-2.0,-0.045) -- (0.7,-0.045);
+ − 273
+ − 274
\draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
+ − 275
\draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
+ − 276
\draw (1.8, 0.48) node[right=-0.1mm]
+ − 277
{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+ − 278
\draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+ − 279
\draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
+ − 280
+ − 281
\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
+ − 282
\draw (-0.95, 0.3) node[above=0mm] {isomorphism};
+ − 283
+ − 284
\end{tikzpicture}
1528
+ − 285
\end{center}
+ − 286
+ − 287
\noindent
1657
+ − 288
We take as the starting point a definition of raw terms (defined as a
+ − 289
datatype in Isabelle/HOL); identify then the alpha-equivalence classes in
+ − 290
the type of sets of raw terms according to our alpha-equivalence relation
+ − 291
and finally define the new type as these alpha-equivalence classes
+ − 292
(non-emptiness is satisfied whenever the raw terms are definable as datatype
1690
+ − 293
in Isabelle/HOL and the property that our relation for alpha-equivalence is
1657
+ − 294
indeed an equivalence relation).
1556
+ − 295
1657
+ − 296
The fact that we obtain an isomorphism between the new type and the
+ − 297
non-empty subset shows that the new type is a faithful representation of
+ − 298
alpha-equated terms. That is not the case for example for terms using the
+ − 299
locally nameless representation of binders \cite{McKinnaPollack99}: in this
+ − 300
representation there are ``junk'' terms that need to be excluded by
+ − 301
reasoning about a well-formedness predicate.
1556
+ − 302
1657
+ − 303
The problem with introducing a new type in Isabelle/HOL is that in order to
+ − 304
be useful, a reasoning infrastructure needs to be ``lifted'' from the
+ − 305
underlying subset to the new type. This is usually a tricky and arduous
+ − 306
task. To ease it, we re-implemented in Isabelle/HOL the quotient package
+ − 307
described by Homeier \cite{Homeier05} for the HOL4 system. This package
+ − 308
allows us to lift definitions and theorems involving raw terms to
+ − 309
definitions and theorems involving alpha-equated terms. For example if we
+ − 310
define the free-variable function over raw lambda-terms
1577
+ − 311
+ − 312
\begin{center}
1657
+ − 313
@{text "fv(x) = {x}"}\hspace{10mm}
+ − 314
@{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]
+ − 315
@{text "fv(\<lambda>x.t) = fv(t) - {x}"}
1577
+ − 316
\end{center}
+ − 317
+ − 318
\noindent
1690
+ − 319
then with the help of the quotient package we obtain a function @{text "fv\<^sup>\<alpha>"}
1617
+ − 320
operating on quotients, or alpha-equivalence classes of lambda-terms. This
1628
+ − 321
lifted function is characterised by the equations
1577
+ − 322
+ − 323
\begin{center}
1657
+ − 324
@{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}
+ − 325
@{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]
+ − 326
@{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<alpha>(t) - {x}"}
1577
+ − 327
\end{center}
+ − 328
+ − 329
\noindent
+ − 330
(Note that this means also the term-constructors for variables, applications
+ − 331
and lambda are lifted to the quotient level.) This construction, of course,
1694
+ − 332
only works if alpha-equivalence is indeed an equivalence relation, and the
+ − 333
lifted definitions and theorems are respectful w.r.t.~alpha-equivalence.
+ − 334
For example, we will not be able to lift a bound-variable function. Although
+ − 335
this function can be defined for raw terms, it does not respect
+ − 336
alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
+ − 337
of theorems to the quotient level needs proofs of some respectfulness
+ − 338
properties (see \cite{Homeier05}). In the paper we show that we are able to
+ − 339
automate these proofs and therefore can establish a reasoning infrastructure
+ − 340
for alpha-equated terms.
1667
+ − 341
+ − 342
The examples we have in mind where our reasoning infrastructure will be
1694
+ − 343
helpful includes the term language of System @{text "F\<^isub>C"}, also
+ − 344
known as Core-Haskell (see Figure~\ref{corehas}). This term language
1703
+ − 345
involves patterns that have lists of type-, coercion- and term-variables
+ − 346
all of which are bound in @{text "\<CASE>"}-expressions. One
1694
+ − 347
difficulty is that each of these variables come with a kind or type
+ − 348
annotation. Representing such binders with single binders and reasoning
+ − 349
about them in a theorem prover would be a major pain. \medskip
1506
+ − 350
1528
+ − 351
\noindent
+ − 352
{\bf Contributions:} We provide new definitions for when terms
+ − 353
involving multiple binders are alpha-equivalent. These definitions are
1607
+ − 354
inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
1528
+ − 355
proofs, we establish a reasoning infrastructure for alpha-equated
+ − 356
terms, including properties about support, freshness and equality
1607
+ − 357
conditions for alpha-equated terms. We are also able to derive, at the moment
+ − 358
only manually, strong induction principles that
+ − 359
have the variable convention already built in.
1667
+ − 360
+ − 361
\begin{figure}
1687
+ − 362
\begin{boxedminipage}{\linewidth}
+ − 363
\begin{center}
1699
+ − 364
\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
1690
+ − 365
\multicolumn{3}{@ {}l}{Type Kinds}\\
1699
+ − 366
@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
1690
+ − 367
\multicolumn{3}{@ {}l}{Coercion Kinds}\\
1699
+ − 368
@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
1690
+ − 369
\multicolumn{3}{@ {}l}{Types}\\
1694
+ − 370
@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}
1699
+ − 371
@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
1690
+ − 372
\multicolumn{3}{@ {}l}{Coercion Types}\\
1694
+ − 373
@{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
1699
+ − 374
@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
+ − 375
& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
+ − 376
& @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
1690
+ − 377
\multicolumn{3}{@ {}l}{Terms}\\
1699
+ − 378
@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+ − 379
& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
+ − 380
& @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
1690
+ − 381
\multicolumn{3}{@ {}l}{Patterns}\\
1699
+ − 382
@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
1690
+ − 383
\multicolumn{3}{@ {}l}{Constants}\\
1699
+ − 384
& @{text C} & coercion constants\\
+ − 385
& @{text T} & value type constructors\\
+ − 386
& @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
+ − 387
& @{text K} & data constructors\smallskip\\
1690
+ − 388
\multicolumn{3}{@ {}l}{Variables}\\
1699
+ − 389
& @{text a} & type variables\\
+ − 390
& @{text c} & coercion variables\\
+ − 391
& @{text x} & term variables\\
1687
+ − 392
\end{tabular}
+ − 393
\end{center}
+ − 394
\end{boxedminipage}
1699
+ − 395
\caption{The term-language of System @{text "F\<^isub>C"}
+ − 396
\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
+ − 397
version of the term-language we made a modification by separating the
1702
+ − 398
grammars for type and coercion kinds, as well as for types and coercion
+ − 399
types. For this paper the interesting term-constructor is @{text "\<CASE>"},
+ − 400
which binds multiple type-, coercion- and term-variables.\label{corehas}}
1667
+ − 401
\end{figure}
1485
+ − 402
*}
+ − 403
1493
+ − 404
section {* A Short Review of the Nominal Logic Work *}
+ − 405
+ − 406
text {*
1556
+ − 407
At its core, Nominal Isabelle is an adaption of the nominal logic work by
+ − 408
Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
1694
+ − 409
\cite{HuffmanUrban10} (including proofs). We shall briefly review this work
+ − 410
to aid the description of what follows.
+ − 411
+ − 412
Two central notions in the nominal
+ − 413
logic work are sorted atoms and sort-respecting permutations of atoms. The
+ − 414
sorts can be used to represent different kinds of variables, such as the
1703
+ − 415
term-, coercion- and type-variables in Core-Haskell, and it is assumed that there is an
1694
+ − 416
infinite supply of atoms for each sort. However, in order to simplify the
+ − 417
description, we shall assume in what follows that there is only one sort of
+ − 418
atoms.
1493
+ − 419
+ − 420
Permutations are bijective functions from atoms to atoms that are
+ − 421
the identity everywhere except on a finite number of atoms. There is a
+ − 422
two-place permutation operation written
1617
+ − 423
%
1703
+ − 424
\begin{center}
+ − 425
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+ − 426
\end{center}
1493
+ − 427
+ − 428
\noindent
1628
+ − 429
in which the generic type @{text "\<beta>"} stands for the type of the object
1694
+ − 430
over which the permutation
1617
+ − 431
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
1690
+ − 432
the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
1570
+ − 433
and the inverse permutation of @{term p} as @{text "- p"}. The permutation
1703
+ − 434
operation is defined by induction over the type-hierarchy (see \cite{HuffmanUrban10});
+ − 435
for example as follows for products, lists, sets, functions and booleans:
1702
+ − 436
%
1703
+ − 437
\begin{equation}\label{permute}
1694
+ − 438
\mbox{\begin{tabular}{@ {}cc@ {}}
1690
+ − 439
\begin{tabular}{@ {}l@ {}}
+ − 440
@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+ − 441
@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
+ − 442
@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+ − 443
\end{tabular} &
+ − 444
\begin{tabular}{@ {}l@ {}}
+ − 445
@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
1694
+ − 446
@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
1690
+ − 447
@{thm permute_bool_def[no_vars, THEN eq_reflection]}\\
+ − 448
\end{tabular}
1694
+ − 449
\end{tabular}}
+ − 450
\end{equation}
1690
+ − 451
+ − 452
\noindent
1703
+ − 453
Concrete permutations are built up from swappings, written as \mbox{@{text "(a
+ − 454
b)"}}, which are permutations that behave as follows:
1617
+ − 455
%
1703
+ − 456
\begin{center}
+ − 457
@{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
+ − 458
\end{center}
+ − 459
1570
+ − 460
The most original aspect of the nominal logic work of Pitts is a general
1703
+ − 461
definition for the notion of the ``set of free variables of an object @{text
1570
+ − 462
"x"}''. This notion, written @{term "supp x"}, is general in the sense that
1628
+ − 463
it applies not only to lambda-terms (alpha-equated or not), but also to lists,
1570
+ − 464
products, sets and even functions. The definition depends only on the
+ − 465
permutation operation and on the notion of equality defined for the type of
+ − 466
@{text x}, namely:
1617
+ − 467
%
1703
+ − 468
\begin{equation}\label{suppdef}
+ − 469
@{thm supp_def[no_vars, THEN eq_reflection]}
+ − 470
\end{equation}
1493
+ − 471
+ − 472
\noindent
+ − 473
There is also the derived notion for when an atom @{text a} is \emph{fresh}
+ − 474
for an @{text x}, defined as
1617
+ − 475
%
1703
+ − 476
\begin{center}
+ − 477
@{thm fresh_def[no_vars]}
+ − 478
\end{center}
1493
+ − 479
+ − 480
\noindent
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 481
We also use for sets of atoms the abbreviation
1703
+ − 482
@{thm (lhs) fresh_star_def[no_vars]}, defined as
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 483
@{thm (rhs) fresh_star_def[no_vars]}.
1493
+ − 484
A striking consequence of these definitions is that we can prove
+ − 485
without knowing anything about the structure of @{term x} that
+ − 486
swapping two fresh atoms, say @{text a} and @{text b}, leave
1506
+ − 487
@{text x} unchanged.
+ − 488
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 489
\begin{property}
1506
+ − 490
@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 491
\end{property}
1506
+ − 492
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 493
\noindent
1703
+ − 494
While often the support of an object can be easily described, for
+ − 495
example\\[-6mm]
1690
+ − 496
%
+ − 497
\begin{eqnarray}
1703
+ − 498
@{term "supp a"} & = & @{term "{a}"}\\
1690
+ − 499
@{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
+ − 500
@{term "supp []"} & = & @{term "{}"}\\
+ − 501
@{term "supp (x#xs)"} & = & @{term "supp (x, xs)"}\\
1703
+ − 502
@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp (f, x)"}\label{suppfun}\\
+ − 503
@{term "supp b"} & = & @{term "{}"}\\
+ − 504
@{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
1690
+ − 505
\end{eqnarray}
+ − 506
+ − 507
\noindent
1703
+ − 508
in some cases it can be difficult to establish the support precisely, and
+ − 509
only give an approximation (see the case for function applications
+ − 510
above). Such approximations can be made precise with the notion
+ − 511
\emph{supports}, defined as follows
1693
+ − 512
+ − 513
\begin{defn}
+ − 514
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
+ − 515
not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
+ − 516
\end{defn}
1690
+ − 517
1693
+ − 518
\noindent
1703
+ − 519
The main point of this definition is that we can show the following two properties.
1693
+ − 520
1703
+ − 521
\begin{property}\label{supportsprop}
+ − 522
{\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}\\
1693
+ − 523
{\it ii)} @{thm supp_supports[no_vars]}.
+ − 524
\end{property}
+ − 525
+ − 526
Another important notion in the nominal logic work is \emph{equivariance}.
1703
+ − 527
For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
+ − 528
requires that every permutation leaves @{text f} unchanged, or equivalently that
+ − 529
a permutation applied to the application @{text "f x"} can be moved to its
1694
+ − 530
arguments. That is
1703
+ − 531
%
+ − 532
\begin{equation}\label{equivariance}
+ − 533
@{text "\<forall>p. p \<bullet> f = f"} \;\;if and only if\;\;
1694
+ − 534
@{text "\<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"}
1703
+ − 535
\end{equation}
1694
+ − 536
+ − 537
\noindent
1703
+ − 538
From the first equation and the definition of support shown in \eqref{suppdef},
+ − 539
we can be easily deduce that an equivariant function has empty support.
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 540
1703
+ − 541
In the next section we use @{text "supp"} and permutations for characterising
+ − 542
alpha-equivalence in the presence of multiple binders.
+ − 543
1493
+ − 544
*}
+ − 545
1485
+ − 546
1620
+ − 547
section {* General Binders\label{sec:binders} *}
1485
+ − 548
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 549
text {*
1587
+ − 550
In Nominal Isabelle, the user is expected to write down a specification of a
+ − 551
term-calculus and then a reasoning infrastructure is automatically derived
1617
+ − 552
from this specification (remember that Nominal Isabelle is a definitional
1587
+ − 553
extension of Isabelle/HOL, which does not introduce any new axioms).
1579
+ − 554
1657
+ − 555
In order to keep our work with deriving the reasoning infrastructure
+ − 556
manageable, we will wherever possible state definitions and perform proofs
+ − 557
on the user-level of Isabelle/HOL, as opposed to write custom ML-code that
+ − 558
generates them anew for each specification. To that end, we will consider
+ − 559
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
+ − 560
are intended to represent the abstraction, or binding, of the set @{text
+ − 561
"as"} in the body @{text "x"}.
1570
+ − 562
1657
+ − 563
The first question we have to answer is when the pairs @{text "(as, x)"} and
+ − 564
@{text "(bs, y)"} are alpha-equivalent? (At the moment we are interested in
+ − 565
the notion of alpha-equivalence that is \emph{not} preserved by adding
+ − 566
vacuous binders.) To answer this, we identify four conditions: {\it i)}
+ − 567
given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
+ − 568
set"}}, then @{text x} and @{text y} need to have the same set of free
+ − 569
variables; moreover there must be a permutation @{text p} such that {\it
1687
+ − 570
ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
1657
+ − 571
{\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
1662
+ − 572
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that
+ − 573
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
1657
+ − 574
requirements {\it i)} to {\it iv)} can be stated formally as follows:
1556
+ − 575
%
1572
+ − 576
\begin{equation}\label{alphaset}
+ − 577
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
1687
+ − 578
\multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
1657
+ − 579
& @{term "fv(x) - as = fv(y) - bs"}\\
+ − 580
@{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\
+ − 581
@{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\
+ − 582
@{text "\<and>"} & @{term "(p \<bullet> as) = bs"}\\
1572
+ − 583
\end{array}
1556
+ − 584
\end{equation}
+ − 585
+ − 586
\noindent
1657
+ − 587
Note that this relation is dependent on the permutation @{text
+ − 588
"p"}. Alpha-equivalence between two pairs is then the relation where we
+ − 589
existentially quantify over this @{text "p"}. Also note that the relation is
+ − 590
dependent on a free-variable function @{text "fv"} and a relation @{text
+ − 591
"R"}. The reason for this extra generality is that we will use
+ − 592
$\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
+ − 593
the latter case, $R$ will be replaced by equality @{text "="} and for raw terms we
+ − 594
will prove that @{text "fv"} is equal to the support of @{text
+ − 595
x} and @{text y}.
1572
+ − 596
+ − 597
The definition in \eqref{alphaset} does not make any distinction between the
1579
+ − 598
order of abstracted variables. If we want this, then we can define alpha-equivalence
+ − 599
for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
+ − 600
as follows
1572
+ − 601
%
+ − 602
\begin{equation}\label{alphalist}
+ − 603
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
1687
+ − 604
\multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
1657
+ − 605
& @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\
+ − 606
\wedge & @{term "(fv(x) - set as) \<sharp>* p"}\\
1572
+ − 607
\wedge & @{text "(p \<bullet> x) R y"}\\
1657
+ − 608
\wedge & @{term "(p \<bullet> as) = bs"}\\
1572
+ − 609
\end{array}
+ − 610
\end{equation}
+ − 611
+ − 612
\noindent
1657
+ − 613
where @{term set} is a function that coerces a list of atoms into a set of atoms.
+ − 614
Now the last clause ensures that the order of the binders matters.
1556
+ − 615
1657
+ − 616
If we do not want to make any difference between the order of binders \emph{and}
1579
+ − 617
also allow vacuous binders, then we keep sets of binders, but drop the fourth
+ − 618
condition in \eqref{alphaset}:
1572
+ − 619
%
1579
+ − 620
\begin{equation}\label{alphares}
1572
+ − 621
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
1687
+ − 622
\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
1657
+ − 623
& @{term "fv(x) - as = fv(y) - bs"}\\
+ − 624
\wedge & @{term "(fv(x) - as) \<sharp>* p"}\\
1572
+ − 625
\wedge & @{text "(p \<bullet> x) R y"}\\
+ − 626
\end{array}
+ − 627
\end{equation}
1556
+ − 628
1662
+ − 629
It might be useful to consider some examples for how these definitions of alpha-equivalence
+ − 630
pan out in practise.
1579
+ − 631
For this consider the case of abstracting a set of variables over types (as in type-schemes).
1657
+ − 632
We set @{text R} to be the equality and for @{text "fv(T)"} we define
1572
+ − 633
+ − 634
\begin{center}
1657
+ − 635
@{text "fv(x) = {x}"} \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}
1572
+ − 636
\end{center}
+ − 637
+ − 638
\noindent
1657
+ − 639
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
1687
+ − 640
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
+ − 641
@{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
1657
+ − 642
$\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
+ − 643
y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
1687
+ − 644
$\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
1657
+ − 645
that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also
+ − 646
leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is
1687
+ − 647
@{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by
1657
+ − 648
taking @{text p} to be the
+ − 649
identity permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
1687
+ − 650
$\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation
1657
+ − 651
that makes the
1687
+ − 652
sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$).
+ − 653
It can also relatively easily be shown that all tree notions of alpha-equivalence
+ − 654
coincide, if we only abstract a single atom.
1579
+ − 655
1657
+ − 656
% looks too ugly
+ − 657
%\noindent
+ − 658
%Let $\star$ range over $\{set, res, list\}$. We prove next under which
+ − 659
%conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence
+ − 660
%relations and equivariant:
+ − 661
%
+ − 662
%\begin{lemma}
+ − 663
%{\it i)} Given the fact that $x\;R\;x$ holds, then
+ − 664
%$(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given
+ − 665
%that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then
+ − 666
%$(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies
+ − 667
%$(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given
+ − 668
%that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies
+ − 669
%@{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$
+ − 670
%and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies
+ − 671
%$(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given
+ − 672
%@{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and
+ − 673
%@{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then
+ − 674
%$(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies
+ − 675
%$(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star
+ − 676
%(p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.
+ − 677
%\end{lemma}
+ − 678
+ − 679
%\begin{proof}
+ − 680
%All properties are by unfolding the definitions and simple calculations.
+ − 681
%\end{proof}
+ − 682
+ − 683
1687
+ − 684
In the rest of this section we are going to introduce a type- and term-constructors
+ − 685
for abstraction. For this we define
1657
+ − 686
%
+ − 687
\begin{equation}
+ − 688
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
+ − 689
\end{equation}
+ − 690
1579
+ − 691
\noindent
1687
+ − 692
(similarly for $\approx_{\textit{abs\_list}}$
+ − 693
and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence
+ − 694
relations and equivariant.
1579
+ − 695
1687
+ − 696
\begin{lemma}\label{alphaeq} The relations
+ − 697
$\approx_{\textit{abs\_set}}$,
+ − 698
$\approx_{\textit{abs\_list}}$
+ − 699
and $\approx_{\textit{abs\_res}}$
+ − 700
are equivalence
1662
+ − 701
relations, and if @{term "abs_set (as, x) (bs, y)"} then also
1687
+ − 702
@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for
+ − 703
the other two relations).
1657
+ − 704
\end{lemma}
+ − 705
+ − 706
\begin{proof}
+ − 707
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
+ − 708
a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
1662
+ − 709
of transitivity, we have two permutations @{text p} and @{text q}, and for the
+ − 710
proof obligation use @{text "q + p"}. All conditions are then by simple
1657
+ − 711
calculations.
+ − 712
\end{proof}
+ − 713
+ − 714
\noindent
1687
+ − 715
This lemma allows us to use our quotient package and introduce
1662
+ − 716
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
1687
+ − 717
representing alpha-equivalence classes of pairs. The elements in these types
1657
+ − 718
we will, respectively, write as:
+ − 719
+ − 720
\begin{center}
+ − 721
@{term "Abs as x"} \hspace{5mm}
+ − 722
@{term "Abs_lst as x"} \hspace{5mm}
+ − 723
@{term "Abs_res as x"}
+ − 724
\end{center}
+ − 725
1662
+ − 726
\noindent
1687
+ − 727
indicating that a set or list is abstracted in @{text x}. We will call the types
+ − 728
\emph{abstraction types} and their elements \emph{abstractions}. The important
+ − 729
property we need is a characterisation for the support of abstractions, namely
1662
+ − 730
1687
+ − 731
\begin{thm}[Support of Abstractions]\label{suppabs}
1703
+ − 732
Assuming @{text x} has finite support, then\\[-6mm]
1662
+ − 733
\begin{center}
1687
+ − 734
\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ − 735
@{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\
+ − 736
@{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
+ − 737
@{thm (lhs) supp_abs(3)[no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[no_vars]}
+ − 738
\end{tabular}
1662
+ − 739
\end{center}
1687
+ − 740
\end{thm}
1662
+ − 741
+ − 742
\noindent
1703
+ − 743
We will only show the first equation as the others
1687
+ − 744
follow similar arguments. By definition of the abstraction type @{text "abs_set"}
+ − 745
we have
+ − 746
%
+ − 747
\begin{equation}\label{abseqiff}
1703
+ − 748
@{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
1687
+ − 749
@{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+ − 750
\end{equation}
+ − 751
+ − 752
\noindent
1703
+ − 753
and also
+ − 754
%
+ − 755
\begin{equation}
+ − 756
@{thm permute_Abs[no_vars]}
+ − 757
\end{equation}
1662
+ − 758
1703
+ − 759
\noindent
+ − 760
The last fact derives from the definition of permutations acting on pairs
+ − 761
(see \eqref{permute}) and alpha-equivalence being equivariant (see Lemma~\ref{alphaeq}).
+ − 762
+ − 763
With these two facts at our disposal, we can show the following lemma
+ − 764
about swapping two atoms.
+ − 765
1662
+ − 766
\begin{lemma}
+ − 767
@{thm[mode=IfThen] abs_swap1(1)[no_vars]}
+ − 768
\end{lemma}
+ − 769
+ − 770
\begin{proof}
1687
+ − 771
By using \eqref{abseqiff}, this lemma is straightforward when observing that
+ − 772
the assumptions give us
1662
+ − 773
@{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
1687
+ − 774
and set difference are equivariant.
1662
+ − 775
\end{proof}
1587
+ − 776
1687
+ − 777
\noindent
+ − 778
This lemma gives us
+ − 779
%
+ − 780
\begin{equation}\label{halfone}
+ − 781
@{thm abs_supports(1)[no_vars]}
+ − 782
\end{equation}
+ − 783
+ − 784
\noindent
1703
+ − 785
which with Property~\ref{supportsprop} gives us one half of
+ − 786
Thm~\ref{suppabs}. The other half is a bit more involved. For this we use a
+ − 787
trick from \cite{Pitts04} and first define an auxiliary function
1687
+ − 788
%
+ − 789
\begin{center}
1703
+ − 790
@{thm supp_gen.simps[THEN eq_reflection, no_vars]}
1687
+ − 791
\end{center}
+ − 792
1703
+ − 793
\noindent
+ − 794
Using the second equation in \eqref{equivariance}, we can show that
+ − 795
@{term "supp_gen"} is equivariant and therefore has empty support. This
+ − 796
in turn means
+ − 797
%
+ − 798
\begin{center}
+ − 799
@{thm (prem 1) aux_fresh(1)[where bs="as", no_vars]}
+ − 800
\;\;implies\;\;
+ − 801
@{thm (concl) aux_fresh(1)[where bs="as", no_vars]}
+ − 802
\end{center}
1687
+ − 803
+ − 804
\noindent
1703
+ − 805
using \eqref{suppfun}. Since @{term "supp x"} is by definition equal
+ − 806
to @{term "{a. \<not> a \<sharp> x}"} we can establish that
+ − 807
%
+ − 808
\begin{equation}\label{halftwo}
+ − 809
@{thm (concl) supp_abs_subset1(1)[no_vars]}
+ − 810
\end{equation}
+ − 811
+ − 812
\noindent
+ − 813
provided @{text x} has finite support (the precondition we need in order to show
+ − 814
that for a finite set of atoms, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}).
+ − 815
+ − 816
Finally taking \eqref{halfone} and \eqref{halftwo} provides us with a proof
+ − 817
of Theorem~\ref{suppabs}. The point of these general lemmas about abstractions is that we
+ − 818
can define and prove properties about them conveniently on the Isabelle/HOL level,
+ − 819
and in addition can use them in what
+ − 820
follows next when we have to deal with binding in specifications of term-calculi.
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 821
*}
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 822
1491
+ − 823
section {* Alpha-Equivalence and Free Variables *}
+ − 824
1520
+ − 825
text {*
1703
+ − 826
Our choice of syntax for specifications of term-calculi is influenced by the existing
1637
+ − 827
datatype package of Isabelle/HOL and by the syntax of the Ott-tool
+ − 828
\cite{ott-jfp}. A specification is a collection of (possibly mutual
+ − 829
recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots,
+ − 830
@{text ty}$^\alpha_n$, and an associated collection
+ − 831
of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
+ − 832
bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
1693
+ − 833
roughly as follows:
1628
+ − 834
%
1619
+ − 835
\begin{equation}\label{scheme}
1636
+ − 836
\mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
1617
+ − 837
type \mbox{declaration part} &
1611
+ − 838
$\begin{cases}
+ − 839
\mbox{\begin{tabular}{l}
1637
+ − 840
\isacommand{nominal\_datatype} @{text ty}$^\alpha_1 = \ldots$\\
+ − 841
\isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\
1587
+ − 842
$\ldots$\\
1637
+ − 843
\isacommand{and} @{text ty}$^\alpha_n = \ldots$\\
1611
+ − 844
\end{tabular}}
+ − 845
\end{cases}$\\
1617
+ − 846
binding \mbox{function part} &
1611
+ − 847
$\begin{cases}
+ − 848
\mbox{\begin{tabular}{l}
1637
+ − 849
\isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_m$\\
1611
+ − 850
\isacommand{where}\\
1587
+ − 851
$\ldots$\\
1611
+ − 852
\end{tabular}}
+ − 853
\end{cases}$\\
1619
+ − 854
\end{tabular}}
+ − 855
\end{equation}
1587
+ − 856
+ − 857
\noindent
1637
+ − 858
Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of
1611
+ − 859
term-constructors, each of which comes with a list of labelled
1620
+ − 860
types that stand for the types of the arguments of the term-constructor.
1637
+ − 861
For example a term-constructor @{text "C\<^sup>\<alpha>"} might have
1611
+ − 862
+ − 863
\begin{center}
1637
+ − 864
@{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$ @{text "binding_clauses"}
1611
+ − 865
\end{center}
1587
+ − 866
1611
+ − 867
\noindent
1637
+ − 868
whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained in the collection
+ − 869
of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the
1636
+ − 870
corresponding argument a \emph{recursive argument}. The labels annotated on
+ − 871
the types are optional and can be used in the (possibly empty) list of
1637
+ − 872
\emph{binding clauses}. These clauses indicate the binders and their scope of
+ − 873
in a term-constructor. They come in three \emph{modes}:
1636
+ − 874
1587
+ − 875
1611
+ − 876
\begin{center}
1617
+ − 877
\begin{tabular}{l}
+ − 878
\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+ − 879
\isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+ − 880
\isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+ − 881
\end{tabular}
1611
+ − 882
\end{center}
+ − 883
+ − 884
\noindent
1636
+ − 885
The first mode is for binding lists of atoms (the order of binders matters); the second is for sets
1637
+ − 886
of binders (the order does not matter, but the cardinality does) and the last is for
1620
+ − 887
sets of binders (with vacuous binders preserving alpha-equivalence).
+ − 888
+ − 889
In addition we distinguish between \emph{shallow} binders and \emph{deep}
+ − 890
binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\;
1637
+ − 891
\isacommand{in}\; {\it label'} (similar for the other two modes). The
1620
+ − 892
restriction we impose on shallow binders is that the {\it label} must either
+ − 893
refer to a type that is an atom type or to a type that is a finite set or
1637
+ − 894
list of an atom type. Two examples for the use of shallow binders are the
+ − 895
specification of lambda-terms, where a single name is bound, and of
+ − 896
type-schemes, where a finite set of names is bound:
1611
+ − 897
+ − 898
\begin{center}
1612
+ − 899
\begin{tabular}{@ {}cc@ {}}
+ − 900
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+ − 901
\isacommand{nominal\_datatype} {\it lam} =\\
+ − 902
\hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
+ − 903
\hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
+ − 904
\hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
1617
+ − 905
\hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
1611
+ − 906
\end{tabular} &
1612
+ − 907
\begin{tabular}{@ {}l@ {}}
+ − 908
\isacommand{nominal\_datatype} {\it ty} =\\
+ − 909
\hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
+ − 910
\hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
1617
+ − 911
\isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
1619
+ − 912
\hspace{24mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\
1611
+ − 913
\end{tabular}
+ − 914
\end{tabular}
+ − 915
\end{center}
1587
+ − 916
1612
+ − 917
\noindent
1637
+ − 918
Note that in this specification \emph{name} refers to an atom type.
1628
+ − 919
If we have shallow binders that ``share'' a body, for instance $t$ in
1637
+ − 920
the following term-constructor
1620
+ − 921
+ − 922
\begin{center}
+ − 923
\begin{tabular}{ll}
1637
+ − 924
\it {\rm Foo} x::name y::name t::lam & \it
1620
+ − 925
\isacommand{bind}\;x\;\isacommand{in}\;t,\;
+ − 926
\isacommand{bind}\;y\;\isacommand{in}\;t
+ − 927
\end{tabular}
+ − 928
\end{center}
+ − 929
+ − 930
\noindent
1628
+ − 931
then we have to make sure the modes of the binders agree. We cannot
1637
+ − 932
have, for instance, in the first binding clause the mode \isacommand{bind}
+ − 933
and in the second \isacommand{bind\_set}.
1620
+ − 934
+ − 935
A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
1636
+ − 936
the atoms in one argument of the term-constructor, which can be bound in
1628
+ − 937
other arguments and also in the same argument (we will
1637
+ − 938
call such binders \emph{recursive}, see below).
1620
+ − 939
The binding functions are expected to return either a set of atoms
+ − 940
(for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
+ − 941
(for \isacommand{bind}). They can be defined by primitive recursion over the
+ − 942
corresponding type; the equations must be given in the binding function part of
1628
+ − 943
the scheme shown in \eqref{scheme}. For example for a calculus containing lets
1637
+ − 944
with tuple patterns, you might specify
1617
+ − 945
1619
+ − 946
\begin{center}
+ − 947
\begin{tabular}{l}
+ − 948
\isacommand{nominal\_datatype} {\it trm} =\\
+ − 949
\hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
+ − 950
\hspace{5mm}$\mid$ App\;{\it trm}\;{\it trm}\\
+ − 951
\hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm}
+ − 952
\;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+ − 953
\hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm}
1636
+ − 954
\;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\
1619
+ − 955
\isacommand{and} {\it pat} =\\
1637
+ − 956
\hspace{5mm}\phantom{$\mid$} PNil\\
+ − 957
\hspace{5mm}$\mid$ PVar\;{\it name}\\
+ − 958
\hspace{5mm}$\mid$ PTup\;{\it pat}\;{\it pat}\\
1636
+ − 959
\isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\
1637
+ − 960
\isacommand{where} $\textit{bn}(\textrm{PNil}) = []$\\
+ − 961
\hspace{5mm}$\mid$ $\textit{bn}(\textrm{PVar}\;x) = [\textit{atom}\; x]$\\
+ − 962
\hspace{5mm}$\mid$ $\textit{bn}(\textrm{PTup}\;p_1\;p_2) = \textit{bn}(p_1)\; @\;\textit{bn}(p_2)$\\
1619
+ − 963
\end{tabular}
+ − 964
\end{center}
1617
+ − 965
1619
+ − 966
\noindent
1637
+ − 967
In this specification the function @{text "bn"} determines which atoms of @{text p} are
+ − 968
bound in the argument @{text "t"}. Note that the second last clause the function @{text "atom"}
+ − 969
coerces a name into the generic atom type of Nominal Isabelle. This allows
+ − 970
us to treat binders of different atom type uniformly.
+ − 971
+ − 972
As will shortly become clear, we cannot return an atom in a binding function
+ − 973
that is also bound in the corresponding term-constructor. That means in the
+ − 974
example above that the term-constructors PVar and PTup must not have a
+ − 975
binding clause. In the present version of Nominal Isabelle, we also adopted
+ − 976
the restriction from the Ott-tool that binding functions can only return:
+ − 977
the empty set or empty list (as in case PNil), a singleton set or singleton
+ − 978
list containing an atom (case PVar), or unions of atom sets or appended atom
+ − 979
lists (case PTup). This restriction will simplify proofs later on.
+ − 980
The the most drastic restriction we have to impose on deep binders is that
+ − 981
we cannot have ``overlapping'' deep binders. Consider for example the
+ − 982
term-constructors:
1617
+ − 983
1620
+ − 984
\begin{center}
+ − 985
\begin{tabular}{ll}
1637
+ − 986
\it {\rm Foo} p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
1620
+ − 987
\isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\
1637
+ − 988
\it {\rm Foo}$'$x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;
1620
+ − 989
\isacommand{bind}\;bn(p)\;\isacommand{in}\;t
+ − 990
+ − 991
\end{tabular}
+ − 992
\end{center}
+ − 993
+ − 994
\noindent
1637
+ − 995
In the first case we bind all atoms from the pattern @{text p} in @{text t}
+ − 996
and also all atoms from @{text q} in @{text t}. As a result we have no way
+ − 997
to determine whether the binder came from the binding function @{text
+ − 998
"bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder
+ − 999
@{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why
1693
+ − 1000
we must exclude such specifications is that they cannot be represent by
1637
+ − 1001
the general binders described in Section \ref{sec:binders}. However
+ − 1002
the following two term-constructors are allowed
1620
+ − 1003
+ − 1004
\begin{center}
+ − 1005
\begin{tabular}{ll}
1637
+ − 1006
\it {\rm Bar} p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
1620
+ − 1007
\isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\
1637
+ − 1008
\it {\rm Bar}$'$p::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
1620
+ − 1009
\isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\
+ − 1010
\end{tabular}
+ − 1011
\end{center}
+ − 1012
+ − 1013
\noindent
1628
+ − 1014
since there is no overlap of binders.
1619
+ − 1015
1637
+ − 1016
Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
1693
+ − 1017
Whenever such a binding clause is present, we will call the binder \emph{recursive}.
1637
+ − 1018
To see the purpose for this, consider ``plain'' Lets and Let\_recs:
1636
+ − 1019
+ − 1020
\begin{center}
1637
+ − 1021
\begin{tabular}{@ {}l@ {}}
1636
+ − 1022
\isacommand{nominal\_datatype} {\it trm} =\\
+ − 1023
\hspace{5mm}\phantom{$\mid$}\ldots\\
+ − 1024
\hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm}
+ − 1025
\;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\
1637
+ − 1026
\hspace{5mm}$\mid$ Let\_rec\;{\it a::assn}\; {\it t::trm}
+ − 1027
\;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},
+ − 1028
\isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\
1636
+ − 1029
\isacommand{and} {\it assn} =\\
+ − 1030
\hspace{5mm}\phantom{$\mid$} ANil\\
+ − 1031
\hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\
+ − 1032
\isacommand{with} {\it bn::assn $\Rightarrow$ atom list}\\
+ − 1033
\isacommand{where} $bn(\textrm{ANil}) = []$\\
+ − 1034
\hspace{5mm}$\mid$ $bn(\textrm{ACons}\;x\;t\;a) = [atom\; x]\; @\; bn(a)$\\
+ − 1035
\end{tabular}
+ − 1036
\end{center}
+ − 1037
+ − 1038
\noindent
1637
+ − 1039
The difference is that with Let we only want to bind the atoms @{text
+ − 1040
"bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms
+ − 1041
inside the assignment. This requires recursive binders and also has
+ − 1042
consequences for the free variable function and alpha-equivalence relation,
+ − 1043
which we are going to explain in the rest of this section.
+ − 1044
+ − 1045
Having dealt with all syntax matters, the problem now is how we can turn
+ − 1046
specifications into actual type definitions in Isabelle/HOL and then
+ − 1047
establish a reasoning infrastructure for them. Because of the problem
+ − 1048
Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
+ − 1049
term-constructors so that binders and their bodies are next to each other, and
+ − 1050
then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
+ − 1051
@{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
+ − 1052
extract datatype definitions from the specification and then define an
1693
+ − 1053
alpha-equivalence relation over them.
1637
+ − 1054
+ − 1055
+ − 1056
The datatype definition can be obtained by just stripping off the
+ − 1057
binding clauses and the labels on the types. We also have to invent
+ − 1058
new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
+ − 1059
given by user. In our implementation we just use an affix like
1636
+ − 1060
+ − 1061
\begin{center}
1637
+ − 1062
@{text "ty\<^sup>\<alpha> \<mapsto> ty_raw"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C_raw"}
1636
+ − 1063
\end{center}
+ − 1064
+ − 1065
\noindent
1637
+ − 1066
The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
+ − 1067
non-empty and the types in the constructors only occur in positive
1693
+ − 1068
position (see \cite{} for an indepth explanation of the datatype package
1637
+ − 1069
in Isabelle/HOL). We then define the user-specified binding
+ − 1070
functions by primitive recursion over the raw datatypes. We can also
+ − 1071
easily define a permutation operation by primitive recursion so that for each
+ − 1072
term constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"} we have that
1587
+ − 1073
1628
+ − 1074
\begin{center}
1637
+ − 1075
@{text "p \<bullet> (C_raw x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C_raw (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
1628
+ − 1076
\end{center}
+ − 1077
+ − 1078
\noindent
1637
+ − 1079
From this definition we can easily show that the raw datatypes are
+ − 1080
all permutation types (Def ??) by a simple structural induction over
+ − 1081
the @{text "ty_raw"}s.
+ − 1082
1693
+ − 1083
The first non-trivial step we have to perform is the generation free-variable
1637
+ − 1084
functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
+ − 1085
we need to define the free-variable functions
+ − 1086
+ − 1087
\begin{center}
+ − 1088
@{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
+ − 1089
\end{center}
+ − 1090
+ − 1091
\noindent
1704
+ − 1092
We define them together with the auxiliary free variable functions for
1705
+ − 1093
binding functions. Given binding functions of types
+ − 1094
@{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
1628
+ − 1095
1637
+ − 1096
\begin{center}
1704
+ − 1097
@{text "fv_bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> atom set"}
1637
+ − 1098
\end{center}
1636
+ − 1099
1637
+ − 1100
\noindent
+ − 1101
The basic idea behind these free-variable functions is to collect all atoms
+ − 1102
that are not bound in a term constructor, but because of the rather
+ − 1103
complicated binding mechanisms the details are somewhat involved.
+ − 1104
+ − 1105
Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with
+ − 1106
some binding clauses, the function @{text "fv_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n)"} will be
+ − 1107
the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}.
+ − 1108
From the binding clause of this term constructor, we can determine whether the
+ − 1109
argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also
+ − 1110
whether it is a recursive or non-recursive of a binder. In these cases the value is:
1628
+ − 1111
+ − 1112
\begin{center}
1636
+ − 1113
\begin{tabular}{cp{7cm}}
+ − 1114
$\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
1704
+ − 1115
$\bullet$ & @{text "fv_bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+ − 1116
non-recursive binder with the auxiliary function @{text "bn\<^isub>j"}\\
+ − 1117
$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is
+ − 1118
a deep recursive binder with the auxiliary function @{text "bn\<^isub>j"}
1628
+ − 1119
\end{tabular}
+ − 1120
\end{center}
+ − 1121
1636
+ − 1122
\noindent
1637
+ − 1123
In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
1704
+ − 1124
one or more abstractions. Let @{text "bnds"} be the bound atoms computed
+ − 1125
as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{text "{}"}.
+ − 1126
Otherwise there are two cases: either the
+ − 1127
corresponding binders are all shallow or there is a single deep binder.
+ − 1128
In the former case we build the union of all shallow binders; in the
1636
+ − 1129
later case we just take set or list of atoms the specified binding
1704
+ − 1130
function returns. With @{text "bnds"} computed as above the value of
+ − 1131
for @{text "x\<^isub>i"} is given by:
1636
+ − 1132
+ − 1133
\begin{center}
+ − 1134
\begin{tabular}{cp{7cm}}
+ − 1135
$\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
+ − 1136
$\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
1657
+ − 1137
$\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
1636
+ − 1138
$\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\
+ − 1139
$\bullet$ & @{term "{}"} otherwise
+ − 1140
\end{tabular}
+ − 1141
\end{center}
1628
+ − 1142
1704
+ − 1143
\marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?}
1628
+ − 1144
1704
+ − 1145
\noindent Next, for each binding function @{text "bn"} we define a
+ − 1146
free variable function @{text "fv_bn"}. The basic idea behind this
+ − 1147
function is to compute all the free atoms under this binding
+ − 1148
function. So given that @{text "bn"} is a binding function for type
+ − 1149
@{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the
+ − 1150
omission of the arguments present in @{text "bn"}.
1637
+ − 1151
1704
+ − 1152
For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"},
+ − 1153
we define @{text "fv_bn"} to be the union of the values calculated
+ − 1154
for @{text "x\<^isub>j"} as follows:
1637
+ − 1155
1706
+ − 1156
\marginpar{raw for being defined}
+ − 1157
1637
+ − 1158
\begin{center}
+ − 1159
\begin{tabular}{cp{7cm}}
1704
+ − 1160
$\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\
+ − 1161
$\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"}
+ − 1162
with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\
+ − 1163
$\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\
+ − 1164
$\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\
+ − 1165
$\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype
1706
+ − 1166
with a free variable function @{text "fv_ty"}. This includes the types being
+ − 1167
defined, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\
+ − 1168
$\bullet$ & @{term "{}"} otherwise
1637
+ − 1169
\end{tabular}
+ − 1170
\end{center}
+ − 1171
1705
+ − 1172
We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
+ − 1173
we need to define
+ − 1174
+ − 1175
\begin{center}
+ − 1176
@{text "\<approx>\<^isub>1 :: ty\<^isub>1 \<Rightarrow> ty\<^isub>1 \<Rightarrow> bool \<dots> \<approx>\<^isub>n :: ty\<^isub>n \<Rightarrow> ty\<^isub>n \<Rightarrow> bool"}
+ − 1177
\end{center}
+ − 1178
+ − 1179
\noindent
+ − 1180
together with the auxiliary equivalences for binding functions. Given binding
+ − 1181
functions for types @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
+ − 1182
\begin{center}
+ − 1183
@{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
+ − 1184
\end{center}
+ − 1185
1706
+ − 1186
TODO existance of permutations.
1705
+ − 1187
1706
+ − 1188
Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
+ − 1189
of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if
+ − 1190
the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
+ − 1191
For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
+ − 1192
+ − 1193
\begin{center}
+ − 1194
\begin{tabular}{cp{7cm}}
+ − 1195
$\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\
+ − 1196
$\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a deep non-recursive binder
+ − 1197
with the auxiliary binding function @{text "bn\<^isub>m"}\\
+ − 1198
$\bullet$ & @{text "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x)) \<approx>gen \<approx>s fvs pi (bn\<^isub>m y\<^isub>j, (y\<^isub>j, s)"}
+ − 1199
provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
+ − 1200
function @{text "bn\<^isub>m"}, ...\\
+ − 1201
$\bullet$ & @{text "(x\<^isub>n, x\<^isub>j) \<approx>gen \<approx> fv_ty pi (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"}
+ − 1202
is bound in @{text "x\<^isub>j"} \\
+ − 1203
$\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
+ − 1204
$\bullet$ & @{text "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen \<approx> fv_ty pi (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "bn\<^isub>m x\<^isub>n"}
+ − 1205
is bound non-recursively in @{text "x\<^isub>j"} \\
+ − 1206
$\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes
+ − 1207
the types being defined, raw)\\
+ − 1208
$\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
+ − 1209
\end{tabular}
+ − 1210
\end{center}
1705
+ − 1211
+ − 1212
1587
+ − 1213
*}
+ − 1214
1637
+ − 1215
section {* The Lifting of Definitions and Properties *}
1587
+ − 1216
+ − 1217
text {*
1520
+ − 1218
Restrictions
+ − 1219
+ − 1220
\begin{itemize}
1572
+ − 1221
\item non-emptiness
1520
+ − 1222
\item positive datatype definitions
+ − 1223
\item finitely supported abstractions
+ − 1224
\item respectfulness of the bn-functions\bigskip
+ − 1225
\item binders can only have a ``single scope''
1577
+ − 1226
\item all bindings must have the same mode
1520
+ − 1227
\end{itemize}
+ − 1228
*}
+ − 1229
1493
+ − 1230
section {* Examples *}
1485
+ − 1231
1702
+ − 1232
text {*
+ − 1233
+ − 1234
\begin{figure}
+ − 1235
\begin{boxedminipage}{\linewidth}
+ − 1236
\small
+ − 1237
\begin{tabular}{l}
+ − 1238
\isacommand{atom\_decl}~@{text "var"}\\
+ − 1239
\isacommand{atom\_decl}~@{text "cvar"}\\
+ − 1240
\isacommand{atom\_decl}~@{text "tvar"}\\[1mm]
+ − 1241
\isacommand{nominal\_datatype}~@{text "tkind ="}\\
+ − 1242
\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
+ − 1243
\isacommand{and}~@{text "ckind ="}\\
+ − 1244
\phantom{$|$}~@{text "CKSim ty ty"}\\
+ − 1245
\isacommand{and}~@{text "ty ="}\\
+ − 1246
\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
+ − 1247
$|$~@{text "TFun string ty_list"}~%
+ − 1248
$|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+ − 1249
$|$~@{text "TArr ckind ty"}\\
+ − 1250
\isacommand{and}~@{text "ty_lst ="}\\
+ − 1251
\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
+ − 1252
\isacommand{and}~@{text "cty ="}\\
+ − 1253
\phantom{$|$}~@{text "CVar cvar"}~%
+ − 1254
$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
+ − 1255
$|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+ − 1256
$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
+ − 1257
$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
+ − 1258
$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
+ − 1259
\isacommand{and}~@{text "co_lst ="}\\
+ − 1260
\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
+ − 1261
\isacommand{and}~@{text "trm ="}\\
+ − 1262
\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
+ − 1263
$|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
+ − 1264
$|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
+ − 1265
$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
+ − 1266
$|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
+ − 1267
$|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~{text x}~\isacommand{in}~{text t}\\
+ − 1268
$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
+ − 1269
\isacommand{and}~@{text "assoc_lst ="}\\
+ − 1270
\phantom{$|$}~@{text ANil}~%
+ − 1271
$|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+ − 1272
\isacommand{and}~@{text "pat ="}\\
+ − 1273
\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
+ − 1274
\isacommand{and}~@{text "vt_lst ="}\\
+ − 1275
\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
+ − 1276
\isacommand{and}~@{text "tvtk_lst ="}\\
+ − 1277
\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
+ − 1278
\isacommand{and}~@{text "tvck_lst ="}\\
+ − 1279
\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
+ − 1280
\isacommand{binder}\\
+ − 1281
@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
+ − 1282
@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+ − 1283
@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
+ − 1284
@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
+ − 1285
\isacommand{where}\\
+ − 1286
\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
+ − 1287
$|$~@{text "bv1 VTNil = []"}\\
+ − 1288
$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
+ − 1289
$|$~@{text "bv2 TVTKNil = []"}\\
+ − 1290
$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
+ − 1291
$|$~@{text "bv3 TVCKNil = []"}\\
+ − 1292
$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
+ − 1293
\end{tabular}
+ − 1294
\end{boxedminipage}
+ − 1295
\caption{\label{nominalcorehas}}
+ − 1296
\end{figure}
+ − 1297
*}
+ − 1298
+ − 1299
+ − 1300
+ − 1301
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1302
section {* Adequacy *}
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1303
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1304
section {* Related Work *}
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1305
1570
+ − 1306
text {*
+ − 1307
Ott is better with list dot specifications; subgrammars
+ − 1308
+ − 1309
untyped;
+ − 1310
+ − 1311
*}
+ − 1312
+ − 1313
1493
+ − 1314
section {* Conclusion *}
1485
+ − 1315
+ − 1316
text {*
1520
+ − 1317
Complication when the single scopedness restriction is lifted (two
+ − 1318
overlapping permutations)
1662
+ − 1319
+ − 1320
+ − 1321
The formalisation presented here will eventually become part of the
+ − 1322
Isabelle distribution, but for the moment it can be downloaded from
+ − 1323
the Mercurial repository linked at
+ − 1324
\href{http://isabelle.in.tum.de/nominal/download}
+ − 1325
{http://isabelle.in.tum.de/nominal/download}.\medskip
1520
+ − 1326
*}
+ − 1327
+ − 1328
text {*
1493
+ − 1329
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1330
TODO: function definitions:
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1331
\medskip
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1332
1493
+ − 1333
\noindent
1528
+ − 1334
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
1506
+ − 1335
many discussions about Nominal Isabelle. We thank Peter Sewell for
+ − 1336
making the informal notes \cite{SewellBestiary} available to us and
1556
+ − 1337
also for patiently explaining some of the finer points about the abstract
1702
+ − 1338
definitions and about the implementation of the Ott-tool. We
+ − 1339
also thank Stephanie Weirich for suggesting to separate the subgrammars
+ − 1340
of kinds and types in our Core-Haskell example.
1485
+ − 1341
1577
+ − 1342
Lookup: Merlin paper by James Cheney; Mark Shinwell PhD
754
+ − 1343
1577
+ − 1344
Future work: distinct list abstraction
+ − 1345
+ − 1346
754
+ − 1347
*}
+ − 1348
1484
+ − 1349
+ − 1350
754
+ − 1351
(*<*)
+ − 1352
end
1704
+ − 1353
(*>*)