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