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