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