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