(*<*)+ −
theory Paper+ −
imports "../Nominal/Test" "LaTeXsugar"+ −
begin+ −
+ −
consts+ −
fv :: "'a \<Rightarrow> 'b"+ −
abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"+ −
alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"+ −
Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" + −
+ −
+ −
definition+ −
"equal \<equiv> (op =)" + −
+ −
notation (latex output)+ −
swap ("'(_ _')" [1000, 1000] 1000) and+ −
fresh ("_ # _" [51, 51] 50) and+ −
fresh_star ("_ #\<^sup>* _" [51, 51] 50) and+ −
supp ("supp _" [78] 73) and+ −
uminus ("-_" [78] 73) and+ −
If ("if _ then _ else _" 10) and+ −
alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and+ −
alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and+ −
alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and+ −
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and+ −
abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and+ −
fv ("fv'(_')" [100] 100) and+ −
equal ("=") and+ −
alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + −
Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and+ −
Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and+ −
Abs_dist ("[_]\<^raw:$\!$>\<^bsub>#list\<^esub>._") and+ −
Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and+ −
Cons ("_::_" [78,77] 73) and+ −
supp_gen ("aux _" [1000] 10) and+ −
alpha_bn ("_ \<approx>bn _")+ −
(*>*)+ −
+ −
+ −
section {* Introduction *}+ −
+ −
text {*+ −
%%% @{text "(1, (2, 3))"}+ −
+ −
So far, Nominal Isabelle provides a mechanism for constructing+ −
alpha-equated terms, for example+ −
+ −
\begin{center}+ −
@{text "t ::= x | t t | \<lambda>x. t"}+ −
\end{center}+ −
+ −
\noindent+ −
where free and bound variables have names. For such alpha-equated terms, Nominal Isabelle+ −
derives automatically a reasoning infrastructure that has been used+ −
successfully in formalisations of an equivalence checking algorithm for LF+ −
\cite{UrbanCheneyBerghofer08}, Typed+ −
Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency+ −
\cite{BengtsonParow09} and a strong normalisation result+ −
for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been+ −
used by Pollack for formalisations in the locally-nameless approach to+ −
binding \cite{SatoPollack10}.+ −
+ −
However, Nominal Isabelle has fared less well in a formalisation of+ −
the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are,+ −
respectively, of the form+ −
%+ −
\begin{equation}\label{tysch}+ −
\begin{array}{l}+ −
@{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}+ −
@{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}+ −
\end{array}+ −
\end{equation}+ −
+ −
\noindent+ −
and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of+ −
type-variables. While it is possible to implement this kind of more general+ −
binders by iterating single binders, this leads to a rather clumsy+ −
formalisation of W. The need of iterating single binders is also one reason+ −
why Nominal Isabelle and similar theorem provers that only provide+ −
mechanisms for binding single variables have not fared extremely well with the+ −
more advanced tasks in the POPLmark challenge \cite{challenge05}, because+ −
also there one would like to bind multiple variables at once.+ −
+ −
Binding multiple variables has interesting properties that cannot be captured+ −
easily by iterating single binders. For example in case of type-schemes we do not+ −
want to make a distinction about the order of the bound variables. Therefore+ −
we would like to regard the following two type-schemes as alpha-equivalent+ −
%+ −
\begin{equation}\label{ex1}+ −
@{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"} + −
\end{equation}+ −
+ −
\noindent+ −
but assuming that @{text x}, @{text y} and @{text z} are distinct variables,+ −
the following two should \emph{not} be alpha-equivalent+ −
%+ −
\begin{equation}\label{ex2}+ −
@{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"} + −
\end{equation}+ −
+ −
\noindent+ −
Moreover, we like to regard type-schemes as alpha-equivalent, if they differ+ −
only on \emph{vacuous} binders, such as+ −
%+ −
\begin{equation}\label{ex3}+ −
@{text "\<forall>{x}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{x, z}. x \<rightarrow> y"}+ −
\end{equation}+ −
+ −
\noindent+ −
where @{text z} does not occur freely in the type. In this paper we will+ −
give a general binding mechanism and associated notion of alpha-equivalence+ −
that can be used to faithfully represent this kind of binding in Nominal+ −
Isabelle. The difficulty of finding the right notion for alpha-equivalence+ −
can be appreciated in this case by considering that the definition given by+ −
Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).+ −
+ −
However, the notion of alpha-equivalence that is preserved by vacuous+ −
binders is not always wanted. For example in terms like+ −
%+ −
\begin{equation}\label{one}+ −
@{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}+ −
\end{equation}+ −
+ −
\noindent+ −
we might not care in which order the assignments $x = 3$ and $y = 2$ are+ −
given, but it would be unusual to regard \eqref{one} as alpha-equivalent + −
with+ −
%+ −
\begin{center}+ −
@{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}+ −
\end{center}+ −
+ −
\noindent+ −
Therefore we will also provide a separate binding mechanism for cases in+ −
which the order of binders does not matter, but the ``cardinality'' of the+ −
binders has to agree.+ −
+ −
However, we found that this is still not sufficient for dealing with+ −
language constructs frequently occurring in programming language+ −
research. For example in @{text "\<LET>"}s containing patterns like+ −
%+ −
\begin{equation}\label{two}+ −
@{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}+ −
\end{equation}+ −
+ −
\noindent+ −
we want to bind all variables from the pattern inside the body of the+ −
$\mathtt{let}$, but we also care about the order of these variables, since+ −
we do not want to regard \eqref{two} as alpha-equivalent with+ −
%+ −
\begin{center}+ −
@{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}+ −
\end{center}+ −
+ −
\noindent+ −
As a result, we provide three general binding mechanisms each of which binds+ −
multiple variables at once, and let the user chose which one is intended+ −
when formalising a term-calculus.+ −
+ −
By providing these general binding mechanisms, however, we have to work+ −
around a problem that has been pointed out by Pottier \cite{Pottier06} and+ −
Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form+ −
%+ −
\begin{center}+ −
@{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}+ −
\end{center}+ −
+ −
\noindent+ −
which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care+ −
about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given,+ −
but we do care about the information that there are as many @{text+ −
"x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if+ −
we represent the @{text "\<LET>"}-constructor by something like+ −
%+ −
\begin{center}+ −
@{text "\<LET> [x\<^isub>1,\<dots>,x\<^isub>n].s [t\<^isub>1,\<dots>,t\<^isub>n]"}+ −
\end{center}+ −
+ −
\noindent+ −
where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}+ −
becomes bound in @{text s}. In this representation the term + −
\mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal+ −
instance, but the lengths of two lists do not agree. To exclude such terms, + −
additional predicates about well-formed+ −
terms are needed in order to ensure that the two lists are of equal+ −
length. This can result into very messy reasoning (see for+ −
example~\cite{BengtsonParow09}). To avoid this, we will allow type+ −
specifications for $\mathtt{let}$s as follows+ −
%+ −
\begin{center}+ −
\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}+ −
@{text trm} & @{text "::="} & @{text "\<dots>"}\\ + −
& @{text "|"} & @{text "\<LET> as::assn s::trm"}\hspace{4mm} + −
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]+ −
@{text assn} & @{text "::="} & @{text "\<ANIL>"}\\+ −
& @{text "|"} & @{text "\<ACONS> name trm assn"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
where @{text assn} is an auxiliary type representing a list of assignments+ −
and @{text bn} an auxiliary function identifying the variables to be bound+ −
by the @{text "\<LET>"}. This function can be defined by recursion over @{text+ −
assn} as follows+ −
+ −
\begin{center}+ −
@{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm} + −
@{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} + −
\end{center}+ −
+ −
\noindent+ −
The scope of the binding is indicated by labels given to the types, for+ −
example @{text "s::trm"}, and a binding clause, in this case+ −
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding+ −
clause states to bind in @{text s} all the names the function @{text+ −
"bn(as)"} returns. This style of specifying terms and bindings is heavily+ −
inspired by the syntax of the Ott-tool \cite{ott-jfp}.+ −
+ −
However, we will not be able to cope with all specifications that are+ −
allowed by Ott. One reason is that Ott lets the user to specify ``empty'' + −
types like+ −
+ −
\begin{center}+ −
@{text "t ::= t t | \<lambda>x. t"}+ −
\end{center}+ −
+ −
\noindent+ −
where no clause for variables is given. Arguably, such specifications make+ −
some sense in the context of Coq's type theory (which Ott supports), but not+ −
at all in a HOL-based environment where every datatype must have a non-empty+ −
set-theoretic model \cite{Berghofer99}.+ −
+ −
Another reason is that we establish the reasoning infrastructure+ −
for alpha-\emph{equated} terms. In contrast, Ott produces a reasoning + −
infrastructure in Isabelle/HOL for+ −
\emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms+ −
and the raw terms produced by Ott use names for bound variables,+ −
there is a key difference: working with alpha-equated terms means, for example, + −
that the two type-schemes+ −
+ −
\begin{center}+ −
@{text "\<forall>{x}. x \<rightarrow> y = \<forall>{x, z}. x \<rightarrow> y"} + −
\end{center}+ −
+ −
\noindent+ −
are not just alpha-equal, but actually \emph{equal}! As a result, we can+ −
only support specifications that make sense on the level of alpha-equated+ −
terms (offending specifications, which for example bind a variable according+ −
to a variable bound somewhere else, are not excluded by Ott, but we have+ −
to). + −
+ −
Our insistence on reasoning with alpha-equated terms comes from the+ −
wealth of experience we gained with the older version of Nominal Isabelle:+ −
for non-trivial properties, reasoning about alpha-equated terms is much+ −
easier than reasoning with raw terms. The fundamental reason for this is+ −
that the HOL-logic underlying Nominal Isabelle allows us to replace+ −
``equals-by-equals''. In contrast, replacing+ −
``alpha-equals-by-alpha-equals'' in a representation based on raw terms+ −
requires a lot of extra reasoning work.+ −
+ −
Although in informal settings a reasoning infrastructure for alpha-equated+ −
terms is nearly always taken for granted, establishing it automatically in+ −
the Isabelle/HOL theorem prover is a rather non-trivial task. For every+ −
specification we will need to construct a type containing as elements the+ −
alpha-equated terms. To do so, we use the standard HOL-technique of defining+ −
a new type by identifying a non-empty subset of an existing type. The+ −
construction we perform in Isabelle/HOL can be illustrated by the following picture:+ −
+ −
\begin{center}+ −
\begin{tikzpicture}+ −
%\draw[step=2mm] (-4,-1) grid (4,1);+ −
+ −
\draw[very thick] (0.7,0.4) circle (4.25mm);+ −
\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);+ −
\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);+ −
+ −
\draw (-2.0, 0.845) -- (0.7,0.845);+ −
\draw (-2.0,-0.045) -- (0.7,-0.045);+ −
+ −
\draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};+ −
\draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};+ −
\draw (1.8, 0.48) node[right=-0.1mm]+ −
{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};+ −
\draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};+ −
\draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};+ −
+ −
\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);+ −
\draw (-0.95, 0.3) node[above=0mm] {isomorphism};+ −
+ −
\end{tikzpicture}+ −
\end{center}+ −
+ −
\noindent+ −
We take as the starting point a definition of raw terms (defined as a+ −
datatype in Isabelle/HOL); identify then the alpha-equivalence classes in+ −
the type of sets of raw terms according to our alpha-equivalence relation+ −
and finally define the new type as these alpha-equivalence classes+ −
(non-emptiness is satisfied whenever the raw terms are definable as datatype+ −
in Isabelle/HOL and the property that our relation for alpha-equivalence is+ −
indeed an equivalence relation).+ −
+ −
The fact that we obtain an isomorphism between the new type and the+ −
non-empty subset shows that the new type is a faithful representation of+ −
alpha-equated terms. That is not the case for example for terms using the+ −
locally nameless representation of binders \cite{McKinnaPollack99}: in this+ −
representation there are ``junk'' terms that need to be excluded by+ −
reasoning about a well-formedness predicate.+ −
+ −
The problem with introducing a new type in Isabelle/HOL is that in order to+ −
be useful, a reasoning infrastructure needs to be ``lifted'' from the+ −
underlying subset to the new type. This is usually a tricky and arduous+ −
task. To ease it, we re-implemented in Isabelle/HOL the quotient package+ −
described by Homeier \cite{Homeier05} for the HOL4 system. This package+ −
allows us to lift definitions and theorems involving raw terms to+ −
definitions and theorems involving alpha-equated terms. For example if we+ −
define the free-variable function over raw lambda-terms+ −
+ −
\begin{center}+ −
@{text "fv(x) = {x}"}\hspace{10mm}+ −
@{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]+ −
@{text "fv(\<lambda>x.t) = fv(t) - {x}"}+ −
\end{center}+ −
+ −
\noindent+ −
then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}+ −
operating on quotients, or alpha-equivalence classes of lambda-terms. This+ −
lifted function is characterised by the equations+ −
+ −
\begin{center}+ −
@{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}+ −
@{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]+ −
@{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<alpha>(t) - {x}"}+ −
\end{center}+ −
+ −
\noindent+ −
(Note that this means also the term-constructors for variables, applications+ −
and lambda are lifted to the quotient level.) This construction, of course,+ −
only works if alpha-equivalence is indeed an equivalence relation, and the+ −
``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence.+ −
For example, we will not be able to lift a bound-variable function. Although+ −
this function can be defined for raw terms, it does not respect+ −
alpha-equivalence and therefore cannot be lifted. To sum up, every lifting+ −
of theorems to the quotient level needs proofs of some respectfulness+ −
properties (see \cite{Homeier05}). In the paper we show that we are able to+ −
automate these proofs and as a result can automatically establish a reasoning + −
infrastructure for alpha-equated terms.+ −
+ −
The examples we have in mind where our reasoning infrastructure will be+ −
helpful includes the term language of System @{text "F\<^isub>C"}, also+ −
known as Core-Haskell (see Figure~\ref{corehas}). This term language+ −
involves patterns that have lists of type-, coercion- and term-variables,+ −
all of which are bound in @{text "\<CASE>"}-expressions. One+ −
feature is that we do not know in advance how many variables need to+ −
be bound. Another is that each bound variable comes with a kind or type+ −
annotation. Representing such binders with single binders and reasoning+ −
about them in a theorem prover would be a major pain. \medskip+ −
+ −
\noindent+ −
{\bf Contributions:} We provide new definitions for when terms+ −
involving multiple binders are alpha-equivalent. These definitions are+ −
inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic+ −
proofs, we establish a reasoning infrastructure for alpha-equated+ −
terms, including properties about support, freshness and equality+ −
conditions for alpha-equated terms. We are also able to derive, for the moment + −
only manually, strong induction principles that + −
have the variable convention already built in.+ −
+ −
\begin{figure}+ −
\begin{boxedminipage}{\linewidth}+ −
\begin{center}+ −
\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}+ −
\multicolumn{3}{@ {}l}{Type Kinds}\\+ −
@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\+ −
\multicolumn{3}{@ {}l}{Coercion Kinds}\\+ −
@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\+ −
\multicolumn{3}{@ {}l}{Types}\\+ −
@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} + −
@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\+ −
\multicolumn{3}{@ {}l}{Coercion Types}\\+ −
@{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}+ −
@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\+ −
& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\+ −
& @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\+ −
\multicolumn{3}{@ {}l}{Terms}\\+ −
@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\+ −
& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\+ −
& @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\+ −
\multicolumn{3}{@ {}l}{Patterns}\\+ −
@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\+ −
\multicolumn{3}{@ {}l}{Constants}\\+ −
& @{text C} & coercion constants\\+ −
& @{text T} & value type constructors\\+ −
& @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\+ −
& @{text K} & data constructors\smallskip\\+ −
\multicolumn{3}{@ {}l}{Variables}\\+ −
& @{text a} & type variables\\+ −
& @{text c} & coercion variables\\+ −
& @{text x} & term variables\\+ −
\end{tabular}+ −
\end{center}+ −
\end{boxedminipage}+ −
\caption{The term-language of System @{text "F\<^isub>C"}+ −
\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this+ −
version of the term-language we made a modification by separating the+ −
grammars for type kinds and coercion kinds, as well as for types and coercion+ −
types. For this paper the interesting term-constructor is @{text "\<CASE>"},+ −
which binds multiple type-, coercion- and term-variables.\label{corehas}}+ −
\end{figure}+ −
*}+ −
+ −
section {* A Short Review of the Nominal Logic Work *}+ −
+ −
text {*+ −
At its core, Nominal Isabelle is an adaption of the nominal logic work by+ −
Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in+ −
\cite{HuffmanUrban10} (including proofs). We shall briefly review this work+ −
to aid the description of what follows. + −
+ −
Two central notions in the nominal logic work are sorted atoms and+ −
sort-respecting permutations of atoms. We will use the letters @{text "a,+ −
b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for+ −
permutations. The sorts of atoms can be used to represent different kinds of+ −
variables, such as the term-, coercion- and type-variables in Core-Haskell.+ −
It is assumed that there is an infinite supply of atoms for each+ −
sort. However, in the interest of brevity, we shall restrict ourselves + −
in what follows to only one sort of atoms.+ −
+ −
Permutations are bijective functions from atoms to atoms that are + −
the identity everywhere except on a finite number of atoms. There is a + −
two-place permutation operation written+ −
%+ −
\begin{center}+ −
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+ −
\end{center}+ −
+ −
\noindent + −
in which the generic type @{text "\<beta>"} stands for the type of the object + −
over which the permutation + −
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},+ −
the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, + −
and the inverse permutation of @{term p} as @{text "- p"}. The permutation+ −
operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10};+ −
for example permutations acting on products, lists, sets, functions and booleans is+ −
given by:+ −
%+ −
\begin{equation}\label{permute}+ −
\mbox{\begin{tabular}{@ {}cc@ {}}+ −
\begin{tabular}{@ {}l@ {}}+ −
@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]+ −
@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\+ −
@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\+ −
\end{tabular} &+ −
\begin{tabular}{@ {}l@ {}}+ −
@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\+ −
@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\+ −
@{thm permute_bool_def[no_vars, THEN eq_reflection]}\\+ −
\end{tabular}+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
Concrete permutations in Nominal Isabelle are built up from swappings, + −
written as \mbox{@{text "(a b)"}}, which are permutations that behave + −
as follows:+ −
%+ −
\begin{center}+ −
@{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}+ −
\end{center}+ −
+ −
The most original aspect of the nominal logic work of Pitts is a general+ −
definition for the notion of the ``set of free variables of an object @{text+ −
"x"}''. This notion, written @{term "supp x"}, is general in the sense that+ −
it applies not only to lambda-terms (alpha-equated or not), but also to lists,+ −
products, sets and even functions. The definition depends only on the+ −
permutation operation and on the notion of equality defined for the type of+ −
@{text x}, namely:+ −
%+ −
\begin{equation}\label{suppdef}+ −
@{thm supp_def[no_vars, THEN eq_reflection]}+ −
\end{equation}+ −
+ −
\noindent+ −
There is also the derived notion for when an atom @{text a} is \emph{fresh}+ −
for an @{text x}, defined as+ −
%+ −
\begin{center}+ −
@{thm fresh_def[no_vars]}+ −
\end{center}+ −
+ −
\noindent+ −
We use for sets of atoms the abbreviation + −
@{thm (lhs) fresh_star_def[no_vars]}, defined as + −
@{thm (rhs) fresh_star_def[no_vars]}.+ −
A striking consequence of these definitions is that we can prove+ −
without knowing anything about the structure of @{term x} that+ −
swapping two fresh atoms, say @{text a} and @{text b}, leave + −
@{text x} unchanged. + −
+ −
\begin{property}\label{swapfreshfresh}+ −
@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}+ −
\end{property}+ −
+ −
While often the support of an object can be relatively easily + −
described, for example for atoms, products, lists, function applications, + −
booleans and permutations as follows\\[-6mm]+ −
%+ −
\begin{eqnarray}+ −
@{term "supp a"} & = & @{term "{a}"}\\+ −
@{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\+ −
@{term "supp []"} & = & @{term "{}"}\\+ −
@{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\+ −
@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\label{suppfun}\\+ −
@{term "supp b"} & = & @{term "{}"}\\+ −
@{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}+ −
\end{eqnarray}+ −
+ −
\noindent + −
in some cases it can be difficult to characterise the support precisely, and+ −
only an approximation can be established (see \eqref{suppfun} above). Reasoning about+ −
such approximations can be simplified with the notion \emph{supports}, defined + −
as follows:+ −
+ −
\begin{defn}+ −
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}+ −
not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.+ −
\end{defn}+ −
+ −
\noindent+ −
The main point of @{text supports} is that we can establish the following + −
two properties.+ −
+ −
\begin{property}\label{supportsprop}+ −
{\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}\\ + −
{\it ii)} @{thm supp_supports[no_vars]}.+ −
\end{property}+ −
+ −
Another important notion in the nominal logic work is \emph{equivariance}.+ −
For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant + −
it is required that every permutation leaves @{text f} unchanged, that is+ −
%+ −
\begin{equation}\label{equivariancedef}+ −
@{term "\<forall>p. p \<bullet> f = f"}+ −
\end{equation}+ −
+ −
\noindent or equivalently that a permutation applied to the application+ −
@{text "f x"} can be moved to the argument @{text x}. That means for equivariant+ −
functions @{text f} we have for all permutations @{text p}+ −
%+ −
\begin{equation}\label{equivariance}+ −
@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;+ −
@{text "p \<bullet> (f x) = f (p \<bullet> x)"}+ −
\end{equation}+ −
+ −
\noindent+ −
From property \eqref{equivariancedef} and the definition of @{text supp}, we + −
can be easily deduce that equivariant functions have empty support. There is+ −
also a similar notion for equivariant relations, say @{text R}, namely the property+ −
that+ −
%+ −
\begin{center}+ −
@{text "x R y"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}+ −
\end{center}+ −
+ −
Finally, the nominal logic work provides us with general means to rename + −
binders. While in the older version of Nominal Isabelle, we used extensively + −
Property~\ref{swapfreshfresh} for renaming single binders, this property + −
proved unwieldy for dealing with multiple binders. For such binders the + −
following generalisations turned out to be easier to use.+ −
+ −
\begin{property}\label{supppermeq}+ −
@{thm[mode=IfThen] supp_perm_eq[no_vars]}+ −
\end{property}+ −
+ −
\begin{property}\label{avoiding}+ −
For a finite set @{text as} and a finitely supported @{text x} with+ −
@{term "as \<sharp>* x"} and also a finitely supported @{text c}, there+ −
exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and+ −
@{term "supp x \<sharp>* p"}.+ −
\end{property}+ −
+ −
\noindent+ −
The idea behind the second property is that given a finite set @{text as}+ −
of binders (being bound, or fresh, in @{text x} is ensured by the+ −
assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that+ −
the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen+ −
as long as it is finitely supported) and also @{text "p"} does not affect anything+ −
in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last + −
fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders + −
@{text as} in @{text x}, because @{term "p \<bullet> x = x"}.+ −
+ −
Most properties given in this section are described in detail in \cite{HuffmanUrban10}+ −
and of course all are formalised in Isabelle/HOL. In the next sections we will make + −
extensively use of these properties in order to define alpha-equivalence in + −
the presence of multiple binders.+ −
*}+ −
+ −
+ −
section {* General Binders\label{sec:binders} *}+ −
+ −
text {*+ −
In Nominal Isabelle, the user is expected to write down a specification of a+ −
term-calculus and then a reasoning infrastructure is automatically derived+ −
from this specification (remember that Nominal Isabelle is a definitional+ −
extension of Isabelle/HOL, which does not introduce any new axioms).+ −
+ −
In order to keep our work with deriving the reasoning infrastructure+ −
manageable, we will wherever possible state definitions and perform proofs+ −
on the user-level of Isabelle/HOL, as opposed to write custom ML-code that+ −
generates them anew for each specification. To that end, we will consider+ −
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs+ −
are intended to represent the abstraction, or binding, of the set of atoms @{text+ −
"as"} in the body @{text "x"}.+ −
+ −
The first question we have to answer is when two pairs @{text "(as, x)"} and+ −
@{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in+ −
the notion of alpha-equivalence that is \emph{not} preserved by adding+ −
vacuous binders.) To answer this, we identify four conditions: {\it i)}+ −
given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom+ −
set"}}, then @{text x} and @{text y} need to have the same set of free+ −
variables; moreover there must be a permutation @{text p} such that {\it+ −
ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but+ −
{\it iii)} ``moves'' their bound names so that we obtain modulo a relation,+ −
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that+ −
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The+ −
requirements {\it i)} to {\it iv)} can be stated formally as follows:+ −
%+ −
\begin{equation}\label{alphaset}+ −
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}+ −
\multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]+ −
& @{term "fv(x) - as = fv(y) - bs"}\\+ −
@{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\+ −
@{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\+ −
@{text "\<and>"} & @{term "(p \<bullet> as) = bs"}\\ + −
\end{array}+ −
\end{equation}+ −
+ −
\noindent+ −
Note that this relation is dependent on the permutation @{text+ −
"p"}. Alpha-equivalence between two pairs is then the relation where we+ −
existentially quantify over this @{text "p"}. Also note that the relation is+ −
dependent on a free-variable function @{text "fv"} and a relation @{text+ −
"R"}. The reason for this extra generality is that we will use+ −
$\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In+ −
the latter case, $R$ will be replaced by equality @{text "="} and we+ −
will prove that @{text "fv"} is equal to @{text "supp"}.+ −
+ −
The definition in \eqref{alphaset} does not make any distinction between the+ −
order of abstracted variables. If we want this, then we can define alpha-equivalence + −
for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} + −
as follows+ −
%+ −
\begin{equation}\label{alphalist}+ −
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}+ −
\multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]+ −
& @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\+ −
\wedge & @{term "(fv(x) - set as) \<sharp>* p"}\\+ −
\wedge & @{text "(p \<bullet> x) R y"}\\+ −
\wedge & @{term "(p \<bullet> as) = bs"}\\ + −
\end{array}+ −
\end{equation}+ −
+ −
\noindent+ −
where @{term set} is a function that coerces a list of atoms into a set of atoms.+ −
Now the last clause ensures that the order of the binders matters (since @{text as}+ −
and @{text bs} are lists of atoms).+ −
+ −
If we do not want to make any difference between the order of binders \emph{and}+ −
also allow vacuous binders, then we keep sets of binders, but drop the fourth + −
condition in \eqref{alphaset}:+ −
%+ −
\begin{equation}\label{alphares}+ −
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}+ −
\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]+ −
& @{term "fv(x) - as = fv(y) - bs"}\\+ −
\wedge & @{term "(fv(x) - as) \<sharp>* p"}\\+ −
\wedge & @{text "(p \<bullet> x) R y"}\\+ −
\end{array}+ −
\end{equation}+ −
+ −
It might be useful to consider some examples for how these definitions of alpha-equivalence+ −
pan out in practice.+ −
For this consider the case of abstracting a set of variables over types (as in type-schemes). + −
We set @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we define+ −
+ −
\begin{center}+ −
@{text "fv(x) = {x}"} \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}+ −
\end{center}+ −
+ −
\noindent+ −
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and+ −
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and+ −
@{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to $\approx_{\textit{set}}$ and+ −
$\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>+ −
y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}+ −
$\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation+ −
that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also+ −
leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is+ −
@{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by + −
taking @{text p} to be the+ −
identity permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}+ −
$\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation + −
that makes the+ −
sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$).+ −
It can also relatively easily be shown that all tree notions of alpha-equivalence+ −
coincide, if we only abstract a single atom. + −
+ −
In the rest of this section we are going to introduce three abstraction + −
types. For this we define + −
%+ −
\begin{equation}+ −
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}+ −
\end{equation}+ −
+ −
\noindent+ −
(similarly for $\approx_{\textit{abs\_res}}$ + −
and $\approx_{\textit{abs\_list}}$). We can show that these relations are equivalence + −
relations and equivariant.+ −
+ −
\begin{lemma}\label{alphaeq} + −
The relations $\approx_{\textit{abs\_set}}$, $\approx_{\textit{abs\_list}}$+ −
and $\approx_{\textit{abs\_res}}$ are equivalence relations, and if @{term+ −
"abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>+ −
bs, p \<bullet> y)"} (similarly for the other two relations).+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have+ −
a permutation @{text p} and for the proof obligation take @{term "-p"}. In case + −
of transitivity, we have two permutations @{text p} and @{text q}, and for the+ −
proof obligation use @{text "q + p"}. All conditions are then by simple+ −
calculations. + −
\end{proof}+ −
+ −
\noindent+ −
This lemma allows us to use our quotient package and introduce + −
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}+ −
representing alpha-equivalence classes of pairs of type + −
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}+ −
(in the third case). + −
The elements in these types will be, respectively, written as:+ −
+ −
\begin{center}+ −
@{term "Abs as x"} \hspace{5mm} + −
@{term "Abs_res as x"} \hspace{5mm}+ −
@{term "Abs_lst as x"} + −
\end{center}+ −
+ −
\noindent+ −
indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will+ −
call the types \emph{abstraction types} and their elements+ −
\emph{abstractions}. The important property we need to derive is the support of + −
abstractions, namely:+ −
+ −
\begin{thm}[Support of Abstractions]\label{suppabs} + −
Assuming @{text x} has finite support, then\\[-6mm] + −
\begin{center}+ −
\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\+ −
@{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\+ −
@{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}+ −
\end{tabular}+ −
\end{center}+ −
\end{thm}+ −
+ −
\noindent+ −
Below we will show the first equation. The others + −
follow by similar arguments. By definition of the abstraction type @{text "abs_set"} + −
we have + −
%+ −
\begin{equation}\label{abseqiff}+ −
@{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; + −
@{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}+ −
\end{equation}+ −
+ −
\noindent+ −
and also+ −
%+ −
\begin{equation}\label{absperm}+ −
@{thm permute_Abs[no_vars]}+ −
\end{equation}+ −
+ −
\noindent+ −
The second fact derives from the definition of permutations acting on pairs + −
\eqref{permute} and alpha-equivalence being equivariant + −
(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show + −
the following lemma about swapping two atoms.+ −
+ −
\begin{lemma}+ −
@{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
This lemma is straightforward using \eqref{abseqiff} and observing that+ −
the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.+ −
Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).+ −
\end{proof}+ −
+ −
\noindent+ −
This lemma together with \eqref{absperm} allows us to show+ −
%+ −
\begin{equation}\label{halfone}+ −
@{thm abs_supports(1)[no_vars]}+ −
\end{equation}+ −
+ −
\noindent+ −
which by Property~\ref{supportsprop} gives us ``one half'' of+ −
Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish + −
it, we use a trick from \cite{Pitts04} and first define an auxiliary + −
function @{text aux}, taking an abstraction as argument:+ −
%+ −
\begin{center}+ −
@{thm supp_gen.simps[THEN eq_reflection, no_vars]}+ −
\end{center}+ −
+ −
\noindent+ −
Using the second equation in \eqref{equivariance}, we can show that + −
@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =+ −
(supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. + −
This in turn means+ −
%+ −
\begin{center}+ −
@{term "supp (supp_gen (Abs as x)) \<subseteq> supp (Abs as x)"}+ −
\end{center}+ −
+ −
\noindent+ −
using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,+ −
we further obtain+ −
%+ −
\begin{equation}\label{halftwo}+ −
@{thm (concl) supp_abs_subset1(1)[no_vars]}+ −
\end{equation}+ −
+ −
\noindent+ −
since for finite sets of atoms, @{text "bs"}, we have + −
@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.+ −
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes + −
Theorem~\ref{suppabs}. + −
+ −
The method of first considering abstractions of the+ −
form @{term "Abs as x"} etc is motivated by the fact that + −
we can conveniently establish at the Isabelle/HOL level+ −
properties about them. It would be+ −
laborious to write custom ML-code that derives automatically such properties + −
for every term-constructor that binds some atoms. Also the generality of+ −
the definitions for alpha-equivalence will help us in the next section.+ −
*}+ −
+ −
section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}+ −
+ −
text {*+ −
Our choice of syntax for specifications is influenced by the existing+ −
datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the+ −
Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a+ −
collection of (possibly mutual recursive) type declarations, say @{text+ −
"ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of+ −
binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The+ −
syntax in Nominal Isabelle for such specifications is roughly as follows:+ −
%+ −
\begin{equation}\label{scheme}+ −
\mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}+ −
type \mbox{declaration part} &+ −
$\begin{cases}+ −
\mbox{\begin{tabular}{l}+ −
\isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\+ −
\isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\+ −
$\ldots$\\ + −
\isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\ + −
\end{tabular}}+ −
\end{cases}$\\+ −
binding \mbox{function part} &+ −
$\begin{cases}+ −
\mbox{\begin{tabular}{l}+ −
\isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\+ −
\isacommand{where}\\+ −
$\ldots$\\+ −
\end{tabular}}+ −
\end{cases}$\\+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of + −
term-constructors, each of which come with a list of labelled + −
types that stand for the types of the arguments of the term-constructor.+ −
For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with+ −
+ −
\begin{center}+ −
@{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$ @{text "binding_clauses"} + −
\end{center}+ −
+ −
\noindent+ −
whereby some of the @{text ty}$'_{1..l}$ (or their components) can be contained+ −
in the collection of @{text ty}$^\alpha_{1..n}$ declared in+ −
\eqref{scheme}. + −
In this case we will call the corresponding argument a+ −
\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. + −
%The types of such recursive + −
%arguments need to satisfy a ``positivity''+ −
%restriction, which ensures that the type has a set-theoretic semantics + −
%\cite{Berghofer99}. + −
The labels+ −
annotated on the types are optional. Their purpose is to be used in the+ −
(possibly empty) list of \emph{binding clauses}, which indicate the binders+ −
and their scope in a term-constructor. They come in three \emph{modes}:+ −
+ −
\begin{center}+ −
\begin{tabular}{l}+ −
\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\+ −
\isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\+ −
\isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
The first mode is for binding lists of atoms (the order of binders matters);+ −
the second is for sets of binders (the order does not matter, but the+ −
cardinality does) and the last is for sets of binders (with vacuous binders+ −
preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding+ −
clause will be called \emph{bodies} (there can be more than one); the + −
``\isacommand{bind}-part'' will be called \emph{binders}. + −
+ −
In contrast to Ott, we allow multiple labels in binders and bodies. For example+ −
we have binding clauses of the form:+ −
+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
@{text "Foo x::name y::name t::lam s::lam"} & + −
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"} + −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
Similarly for the other binding modes.+ −
There are a few restrictions we need to impose: First, a body can only occur in+ −
\emph{one} binding clause of a term constructor. + −
+ −
For binders we distinguish between \emph{shallow} and \emph{deep} binders.+ −
Shallow binders are of the form \isacommand{bind}\; {\it labels}\;+ −
\isacommand{in}\; {\it labels'} (similar for the other two modes). The+ −
restrictions we impose on shallow binders are that in case of+ −
\isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must+ −
either refer to atom types or to sets of atom types; in case of+ −
\isacommand{bind} we allow labels to refer to atom types or lists of atom types. + −
Two examples for the use of shallow binders are the specification of+ −
lambda-terms, where a single name is bound, and type-schemes, where a finite+ −
set of names is bound:+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}cc@ {}}+ −
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}+ −
\isacommand{nominal\_datatype} @{text lam} =\\+ −
\hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\+ −
\hspace{5mm}$\mid$~@{text "App lam lam"}\\+ −
\hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\+ −
\hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\+ −
\end{tabular} &+ −
\begin{tabular}{@ {}l@ {}}+ −
\isacommand{nominal\_datatype}~@{text ty} =\\+ −
\hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\+ −
\hspace{5mm}$\mid$~@{text "TFun ty ty"}\\+ −
\isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\+ −
\hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\+ −
\end{tabular}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
Note that for @{text lam} it does not matter which binding mode we use. The reason is that + −
we bind only a single @{text name}. However, having \isacommand{bind\_set}, or even + −
\isacommand{bind}, in the second+ −
case changes the semantics of the specification. + −
Note also that in these specifications @{text "name"} refers to an atom type, and+ −
@{text "fset"} to the type of finite sets. + −
+ −
A \emph{deep} binder uses an auxiliary binding function that ``picks'' out+ −
the atoms in one argument of the term-constructor, which can be bound in + −
other arguments and also in the same argument (we will+ −
call such binders \emph{recursive}, see below). + −
The corresponding binding functions are expected to return either a set of atoms+ −
(for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms+ −
(for \isacommand{bind}). They can be defined by primitive recursion over the+ −
corresponding type; the equations must be given in the binding function part of+ −
the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s + −
with tuple patterns might be specified as:+ −
%+ −
\begin{equation}\label{letpat}+ −
\mbox{%+ −
\begin{tabular}{l}+ −
\isacommand{nominal\_datatype} @{text trm} =\\+ −
\hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\+ −
\hspace{5mm}$\mid$~@{term "App trm trm"}\\+ −
\hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} + −
\;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\+ −
\hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} + −
\;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\+ −
\isacommand{and} @{text pat} =\\+ −
\hspace{5mm}\phantom{$\mid$}~@{text PNil}\\+ −
\hspace{5mm}$\mid$~@{text "PVar name"}\\+ −
\hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ + −
\isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\+ −
\isacommand{where}~@{text "bn(PNil) = []"}\\+ −
\hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\+ −
\hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\\ + −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
In this specification the function @{text "bn"} determines which atoms of @{text p} are+ −
bound in the argument @{text "t"}. Note that in the second-last @{text bn}-clause the + −
function @{text "atom"}+ −
coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. + −
This allows+ −
us to treat binders of different atom type uniformly. + −
+ −
The most drastic restriction we have to impose on deep binders is that + −
we cannot have more than one binding function for one binder. Consider for example the + −
term-constructors:+ −
+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
@{text "Foo\<^isub>1 p::pat q::pat t::trm"} & + −
\isacommand{bind} @{text "bn(p) bn(q)"} \isacommand{in} @{text t}\\+ −
@{text "Foo\<^isub>2 x::name p::pat t::trm"} & + −
\isacommand{bind} @{text "x bn(p)"} \isacommand{in} @{text t}\\ + −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t}+ −
and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way+ −
to determine whether the binder came from the binding function @{text+ −
"bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why+ −
we must exclude such specifications is that they cannot be represented by+ −
the general binders described in Section \ref{sec:binders}. However+ −
the following two term-constructors are allowed+ −
+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
@{text "Bar\<^isub>1 p::pat t::trm s::trm"} & + −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t s"}\\+ −
@{text "Bar\<^isub>2 p::pat t::trm"} & + −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
since there is no overlap of binders. Unlike shallow binders, we restrict deep+ −
binders to occur in only one binding clause. Therefore @{text "Bar\<^isub>2"} cannot + −
be reformulated as+ −
+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
@{text "Bar\<^isub>3 p::pat t::trm"} & + −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p"}, + −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
Note that in the @{text "Bar\<^isub>2"}, we wrote \isacommand{bind}~@{text+ −
"bn(p)"}~\isacommand{in}~@{text "p.."}. Whenever such a binding clause + −
is present, where the argument in the binder also occurs in the body, we will + −
call the corresponding binder \emph{recursive}. To see the+ −
purpose of such recursive binders, compare ``plain'' @{text "Let"}s and+ −
@{text "Let_rec"}s in the following specification:+ −
%+ −
\begin{equation}\label{letrecs}+ −
\mbox{%+ −
\begin{tabular}{@ {}l@ {}}+ −
\isacommand{nominal\_datatype}~@{text "trm ="}\\+ −
\hspace{5mm}\phantom{$\mid$}\ldots\\+ −
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} + −
\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\+ −
\hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}+ −
\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\+ −
\isacommand{and} @{text "ass"} =\\+ −
\hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\+ −
\hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\+ −
\isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\+ −
\isacommand{where}~@{text "bn(ANil) = []"}\\+ −
\hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
The difference is that with @{text Let} we only want to bind the atoms @{text+ −
"bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms+ −
inside the assignment. This difference has consequences for the free-variable + −
function and alpha-equivalence relation, which we are going to describe in the + −
rest of this section.+ −
+ −
We also need to restrict the form of the binding functions. As will shortly+ −
become clear, we cannot return an atom in a binding function that is also+ −
bound in the corresponding term-constructor. That means in the example+ −
\eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may+ −
not have a binding clause (all arguments are used to define @{text "bn"}).+ −
In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}+ −
may have binding clause involving the argument @{text t} (the only one that+ −
is \emph{not} used in the definition of the binding function). In the version of+ −
Nominal Isabelle described here, we also adopted the restriction from the+ −
Ott-tool that binding functions can only return: the empty set or empty list+ −
(as in case @{text PNil}), a singleton set or singleton list containing an+ −
atom (case @{text PVar}), or unions of atom sets or appended atom lists+ −
(case @{text PTup}). This restriction will simplify some automatic proofs+ −
later on.+ −
+ −
In order to simplify some later definitions, we shall assume specifications + −
of term-calculi are \emph{completed}. By this we mean that + −
for every argument of a term-constructor that is \emph{not} + −
already part of a binding clause, we add implicitly a special \emph{empty} binding+ −
clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "label"}. In case+ −
of the lambda-calculus, the completion produces+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}+ −
\isacommand{nominal\_datatype} @{text lam} =\\+ −
\hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}+ −
\;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\+ −
\hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}+ −
\;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1"},+ −
\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>2"}\\+ −
\hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}+ −
\;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent + −
The point of completion is that we can make definitions over the binding+ −
clauses and be sure to have captured all arguments of a term constructor. + −
+ −
Having dealt with all syntax matters, the problem now is how we can turn+ −
specifications into actual type definitions in Isabelle/HOL and then+ −
establish a reasoning infrastructure for them. As+ −
Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just + −
re-arranging the arguments of+ −
term-constructors so that binders and their bodies are next to each other will + −
result in inadequate representations. Therefore we will first+ −
extract datatype definitions from the specification and then define + −
expicitly an alpha-equivalence relation over them.+ −
+ −
+ −
The datatype definition can be obtained by stripping off the + −
binding clauses and the labels from the types. We also have to invent+ −
new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}+ −
given by the user. In our implementation we just use the affix ``@{text "_raw"}''.+ −
But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate + −
that a notion is defined over alpha-equivalence classes and leave it out + −
for the corresponding notion defined on the ``raw'' level. So for example + −
we have+ −
+ −
\begin{center}+ −
@{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}+ −
\end{center}+ −
+ −
\noindent+ −
where @{term ty} is the type used in the quotient construction for + −
@{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. + −
+ −
The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are + −
non-empty and the types in the constructors only occur in positive + −
position (see \cite{Berghofer99} for an indepth description of the datatype package+ −
in Isabelle/HOL). We then define the user-specified binding + −
functions, called @{term "bn"}, by primitive recursion over the corresponding + −
raw datatype. We can also easily define permutation operations by + −
primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"} + −
we have that+ −
%+ −
\begin{equation}\label{ceqvt}+ −
@{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}+ −
\end{equation}+ −
+ −
The first non-trivial step we have to perform is the generation free-variable + −
functions from the specifications. For atomic types we define the auxilary+ −
free variable functions:+ −
+ −
\begin{center}+ −
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\+ −
@{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\+ −
@{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent + −
Like the coercion function @{text atom}, @{text "atoms"} coerces + −
the set of atoms to a set of the generic atom type.+ −
It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.+ −
+ −
Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} we define now the+ −
free-variable functions+ −
+ −
\begin{center}+ −
@{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}+ −
\end{center}+ −
+ −
\noindent+ −
We define them together with auxiliary free-variable functions for+ −
the binding functions. Given binding functions + −
@{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define+ −
%+ −
\begin{center}+ −
@{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}+ −
\end{center}+ −
+ −
\noindent+ −
The reason for this setup is that in a deep binder not all atoms have to be+ −
bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function+ −
that calculates those unbound atoms. + −
+ −
While the idea behind these free-variable functions is clear (they just+ −
collect all atoms that are not bound), because of our rather complicated+ −
binding mechanisms their definitions are somewhat involved. Given a+ −
term-constructor @{text "C"} of type @{text ty} and some associated binding+ −
clauses @{text bcs}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be+ −
the union of the values, @{text v}, calculated by the rules for empty, shallow and+ −
deep binding clauses: + −
%+ −
\begin{equation}\label{deepbinderA}+ −
\mbox{%+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}+ −
\multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ + −
$\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\+ −
% + −
\multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ + −
$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\ + −
& \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\ + −
& provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the + −
binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\+ −
\end{tabular}}+ −
\end{equation}+ −
\begin{equation}\label{deepbinderB}+ −
\mbox{%+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}+ −
\multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ + −
$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x) \<union> (fv_bn x)"}\\+ −
$\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\+ −
& provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first + −
clause applies for @{text x} being a non-recursive deep binder (that is + −
@{text "x \<noteq> y"}$_{1..m}$), the second for a recursive deep binder+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
Similarly for the other binding modes. Note that in a non-recursive deep+ −
binder, we have to add all atoms that are left unbound by the binding+ −
function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume+ −
for the constructor @{text "C"} the binding function is of the form @{text+ −
"bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}. We again define a value+ −
@{text v} which is exactly as in \eqref{deepbinderA}/\eqref{deepbinderB} for shallow and deep+ −
binding clauses, except for empty binding clauses are defined as follows: + −
%+ −
\begin{equation}\label{bnemptybinder}+ −
\mbox{%+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
\multicolumn{2}{@ {}l}{\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ + −
$\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"}+ −
and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\+ −
$\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in @{text "rhs"}+ −
with a recursive call @{text "bn y"}\\+ −
$\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"},+ −
but without a recursive call\\+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
The reason why we only have to treat the empty binding clauses specially in+ −
the definition of @{text "fv_bn"} is that binding functions can only use arguments+ −
that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot+ −
be lifted to alpha-equated terms.+ −
+ −
+ −
To see how these definitions work in practice, let us reconsider the term-constructors + −
@{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. + −
For this specification we need to define three free-variable functions, namely+ −
@{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:+ −
%+ −
\begin{center}+ −
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}+ −
@{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t - set (bn as)) \<union> fv\<^bsub>bn\<^esub> as"}\\+ −
@{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]+ −
+ −
@{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\+ −
@{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]+ −
+ −
@{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\+ −
@{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}+ −
and @{text "ACons"}, the corresponding free-variable function @{text+ −
"fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The+ −
binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text+ −
"Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in+ −
@{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text+ −
"fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are+ −
free in @{text "as"}. This is what the purpose of the function @{text+ −
"fv\<^bsub>bn\<^esub>"} is. In contrast, in @{text "Let_rec"} we have a+ −
recursive binder where we want to also bind all occurrences of the atoms+ −
in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text+ −
"set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from+ −
@{text "fv\<^bsub>assn\<^esub> as"}. An interesting point in this example is+ −
that an assignment ``alone'' does not have any bound variables. Only in the+ −
context of a @{text Let} or @{text "Let_rec"} will some atoms become bound. + −
This is a phenomenon + −
that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because+ −
we would not be able to lift a @{text "bn"}-function that is defined over + −
arguments that are either binders or bodies. In that case @{text "bn"} would+ −
not respect alpha-equivalence. We can also see that+ −
%+ −
\begin{equation}\label{bnprop}+ −
@{text "fv_ty x = bn x \<union> fv_bn x"}.+ −
\end{equation}+ −
+ −
\noindent+ −
holds for any @{text "bn"}-function defined for the type @{text "ty"}.+ −
+ −
Next we define alpha-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them+ −
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, + −
we also need to define auxiliary alpha-equivalence relations for the binding functions. + −
Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.+ −
To simplify our definitions we will use the following abbreviations for + −
relations and free-variable acting on products.+ −
%+ −
\begin{center}+ −
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{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"}\\+ −
@{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
+ −
The relations for alpha-equivalence are inductively defined predicates, whose clauses have+ −
conclusions of the form + −
%+ −
\begin{center}+ −
@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} + −
\end{center}+ −
+ −
\noindent+ −
For what follows, let us assume @{text C} is of type @{text ty}. The task+ −
is to specify what the premises of these clauses are. Again for this we+ −
analyse the binding clauses and produce a corresponding premise.+ −
*}+ −
(*<*)+ −
consts alpha_ty ::'a+ −
consts alpha_trm ::'a+ −
consts fv_trm :: 'a+ −
consts alpha_trm2 ::'a+ −
consts fv_trm2 :: 'a+ −
notation (latex output) + −
alpha_ty ("\<approx>ty") and+ −
alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and+ −
fv_trm ("fv\<^bsub>trm\<^esub>") and+ −
alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and+ −
fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>") + −
(*>*)+ −
text {*+ −
\begin{equation}\label{alpha}+ −
\mbox{%+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
\multicolumn{2}{@ {}l}{Empty binding clauses of the form + −
\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "x\<^isub>i"}:}\\ + −
$\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} + −
are recursive arguments of @{text "C"}\\+ −
$\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are + −
non-recursive arguments\smallskip\\+ −
\multicolumn{2}{@ {}l}{Shallow binders of the form + −
\isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ + −
$\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},+ −
@{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is+ −
@{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then+ −
\begin{center}+ −
@{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}+ −
\end{center}\\+ −
\multicolumn{2}{@ {}l}{Deep binders of the form + −
\isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ + −
$\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},+ −
@{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is+ −
@{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then for recursive deep binders+ −
\begin{center}+ −
@{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}+ −
\end{center}\\+ −
$\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
Similarly for the other binding modes.+ −
From this definition it is clear why we have to impose the restriction+ −
of excluding overlapping deep binders, as these would need to be translated into separate+ −
abstractions.+ −
+ −
+ −
+ −
The alpha-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions + −
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"}}+ −
and need to generate appropriate premises. We generate first premises according to the first three+ −
rules given above. Only the ``left-over'' pairs @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated + −
differently. They depend on whether @{text "x\<^isub>i"} occurs in @{text "rhs"} of the + −
clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:+ −
+ −
\begin{center}+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
$\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}+ −
and the type of @{text "x\<^isub>i"} is @{text ty} and @{text "x\<^isub>i"} is a recursive argument + −
in the term-constructor\\+ −
$\bullet$ & @{text "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}+ −
and @{text "x\<^isub>i"} is not a recursive argument in the term-constructor\\+ −
$\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs}+ −
with the recursive call @{text "bn x\<^isub>i"}\\+ −
$\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not+ −
in a recursive call involving a @{text "bn"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}+ −
we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and+ −
$\approx_{\textit{bn}}$, with the clauses as follows:+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}c @ {}}+ −
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}+ −
{@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fv_trm p (bn as', t')"}}\smallskip\\+ −
\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}+ −
{@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fv_trm2 p (bn as', (as', t'))"}}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}c @ {}}+ −
\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\+ −
\infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}+ −
{@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}c @ {}}+ −
\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\+ −
\infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}+ −
{@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
Note the difference between $\approx_{\textit{assn}}$ and+ −
$\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of + −
the components in an assignment that are \emph{not} bound. Therefore we have+ −
a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is + −
a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant + −
to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, + −
because there everything from the assignment is under the binder. + −
*}+ −
+ −
section {* Establishing the Reasoning Infrastructure *}+ −
+ −
text {*+ −
Having made all necessary definitions for raw terms, we can start+ −
introducing the reasoning infrastructure for the alpha-equated types the+ −
user originally specified. We sketch in this section the facts we need for establishing+ −
this reasoning infrastructure. First we have to show that the+ −
alpha-equivalence relations defined in the previous section are indeed+ −
equivalence relations.+ −
+ −
\begin{lemma}\label{equiv} + −
Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions+ −
@{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and + −
@{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.+ −
\end{lemma}+ −
+ −
\begin{proof} + −
The proof is by mutual induction over the definitions. The non-trivial+ −
cases involve premises build up by $\approx_{\textit{set}}$, + −
$\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They + −
can be dealt with as in Lemma~\ref{alphaeq}.+ −
\end{proof}+ −
+ −
\noindent + −
We can feed this lemma into our quotient package and obtain new types @{text+ −
"ty\<AL>\<^bsub>1..n\<^esub>"} representing alpha-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain + −
definitions for the term-constructors @{text+ −
"C"}$^\alpha_{1..m}$ from the raw term-constructors @{text+ −
"C"}$_{1..m}$, and similar definitions for the free-variable functions @{text+ −
"fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text+ −
"bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the + −
user, since they are given in terms of the isomorphisms we obtained by + −
creating new types in Isabelle/HOL (recall the picture shown in the + −
Introduction).+ −
+ −
The first useful property to the user is the fact that term-constructors are + −
distinct, that is+ −
%+ −
\begin{equation}\label{distinctalpha}+ −
\mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} + −
@{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.} + −
\end{equation}+ −
+ −
\noindent+ −
By definition of alpha-equivalence we can show that+ −
for the raw term-constructors+ −
%+ −
\begin{equation}\label{distinctraw}+ −
\mbox{@{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"}.}+ −
\end{equation}+ −
+ −
\noindent+ −
In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient+ −
package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} + −
are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).+ −
Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types+ −
@{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that+ −
+ −
\begin{center}+ −
@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}+ −
\end{center} + −
+ −
\noindent+ −
are alpha-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments+ −
and @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments of @{text "C\<^isub>i"}. We can prove this by + −
analysing the definition of @{text "\<approx>ty"}. For this proof to succeed we have to establish + −
the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined + −
for the type @{text ty\<^isub>i}, we have that+ −
%+ −
\begin{center}+ −
@{text "x \<approx>ty\<^isub>i y"} implies @{text "x \<approx>bn\<^isub>i y"}+ −
\end{center}+ −
+ −
\noindent+ −
This can be established by induction on the definition of @{text "\<approx>ty\<^isub>i"}. + −
+ −
Having established respectfulness for every raw term-constructor, the + −
quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.+ −
In fact we can from now on lift facts from the raw level to the alpha-equated level+ −
as long as they contain raw term-constructors only. The + −
induction principles derived by the datatype package in Isabelle/HOL for the types @{text+ −
"ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure+ −
induction principles that establish+ −
+ −
\begin{center}+ −
@{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>1 y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^esub>\<^isub>n y\<^isub>n "}+ −
\end{center} + −
+ −
\noindent+ −
for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties+ −
defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of + −
these induction principles look+ −
as follows+ −
+ −
\begin{center}+ −
@{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<AL>\<^esub>\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<AL>\<^esub>\<^isub>j x\<^isub>j \<Rightarrow> P\<^bsub>ty\<AL>\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} + −
\end{center}+ −
+ −
\noindent+ −
where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. + −
Next we lift the permutation operations defined in \eqref{ceqvt} for+ −
the raw term-constructors @{text "C"}. These facts contain, in addition + −
to the term-constructors, also permutation operations. In order to make the + −
lifting to go through, + −
we have to know that the permutation operations are respectful + −
w.r.t.~alpha-equivalence. This amounts to showing that the + −
alpha-equivalence relations are equivariant, which we already established + −
in Lemma~\ref{equiv}. As a result we can establish the equations+ −
+ −
\begin{equation}\label{calphaeqvt}+ −
@{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}+ −
\end{equation}+ −
+ −
\noindent+ −
for our infrastructure. In a similar fashion we can lift the equations+ −
characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the + −
binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for these+ −
lifting are the properties:+ −
%+ −
\begin{equation}\label{fnresp}+ −
\mbox{%+ −
\begin{tabular}{l}+ −
@{text "x \<approx>ty\<^isub>j y"} implies @{text "fv_ty\<^isub>j x = fv_ty\<^isub>j y"}\\+ −
@{text "x \<approx>ty\<^isub>k y"} implies @{text "fv_bn\<^isub>k x = fv_bn\<^isub>k y"}\\+ −
@{text "x \<approx>ty\<^isub>k y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"}+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
which can be established by induction on @{text "\<approx>ty"}. Whereas the first+ −
property is always true by the way how we defined the free-variable+ −
functions for types, the second and third do \emph{not} hold in general. There is, in principle, + −
the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound+ −
variable. Then the third property is just not true. However, our + −
restrictions imposed on the binding functions+ −
exclude this possibility.+ −
+ −
Having the facts \eqref{fnresp} at our disposal, we can lift the+ −
definitions that characterise when two terms of the form+ −
+ −
\begin{center}+ −
@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}+ −
\end{center}+ −
+ −
\noindent+ −
are alpha-equivalent. This gives us conditions when the corresponding+ −
alpha-equated terms are \emph{equal}, namely+ −
+ −
\begin{center}+ −
@{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}+ −
\end{center}+ −
+ −
\noindent+ −
We call these conditions as \emph{quasi-injectivity}. Except for one function, which+ −
we have to lift in the next section, we completed+ −
the lifting part of establishing the reasoning infrastructure. + −
+ −
By working now completely on the alpha-equated level, we can first show that + −
the free-variable functions and binding functions+ −
are equivariant, namely+ −
+ −
\begin{center}+ −
\begin{tabular}{rcl}+ −
@{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\+ −
@{text "p \<bullet> (fv_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fv_bn\<^sup>\<alpha> (p \<bullet> x)"}\\+ −
@{text "p \<bullet> (bn\<^sup>\<alpha> x)"} & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
These properties can be established by structural induction over the @{text x}+ −
(using the induction principles we lifted above for the types @{text "ty\<AL>\<^bsub>1..n\<^esub>"}).+ −
+ −
Until now we have not yet derived anything about the support of the + −
alpha-equated terms. This however will be necessary in order to derive+ −
the strong induction principles in the next section.+ −
Using the equivariance properties in \eqref{ceqvt} we can+ −
show for every term-constructor @{text "C\<^sup>\<alpha>"} that + −
+ −
\begin{center}+ −
@{text "(supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}+ −
\end{center}+ −
+ −
\noindent+ −
holds. This together with Property~\ref{supportsprop} allows us to show+ −
+ −
\begin{center}+ −
@{text "finite (supp x\<^isub>i)"}+ −
\end{center}+ −
+ −
\noindent+ −
by a structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types + −
@{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in + −
@{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\<AL>\<^bsub>1..n\<^esub>"}.+ −
+ −
\begin{lemma} + −
For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that + −
@{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds.+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case+ −
we unfold the definition of @{text "supp"}, move the swapping inside the + −
term-constructors and the use then quasi-injectivity lemmas in order to complete the+ −
proof. For the abstraction cases we use the facts derived in Theorem~\ref{suppabs}.+ −
\end{proof}+ −
+ −
\noindent+ −
To sum up, we can established automatically a reasoning infrastructure+ −
for the types @{text "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"} + −
by first lifting definitions from the raw level to the quotient level and+ −
then establish facts about these lifted definitions. All necessary proofs+ −
are generated automatically by custom ML-code. This code can deal with + −
specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell. + −
+ −
\begin{figure}[t!]+ −
\begin{boxedminipage}{\linewidth}+ −
\small+ −
\begin{tabular}{l}+ −
\isacommand{atom\_decl}~@{text "var"}\\+ −
\isacommand{atom\_decl}~@{text "cvar"}\\+ −
\isacommand{atom\_decl}~@{text "tvar"}\\[1mm]+ −
\isacommand{nominal\_datatype}~@{text "tkind ="}\\+ −
\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ + −
\isacommand{and}~@{text "ckind ="}\\+ −
\phantom{$|$}~@{text "CKSim ty ty"}\\+ −
\isacommand{and}~@{text "ty ="}\\+ −
\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\+ −
$|$~@{text "TFun string ty_list"}~%+ −
$|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\+ −
$|$~@{text "TArr ckind ty"}\\+ −
\isacommand{and}~@{text "ty_lst ="}\\+ −
\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\+ −
\isacommand{and}~@{text "cty ="}\\+ −
\phantom{$|$}~@{text "CVar cvar"}~%+ −
$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\+ −
$|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\+ −
$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\+ −
$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\+ −
$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\+ −
\isacommand{and}~@{text "co_lst ="}\\+ −
\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\+ −
\isacommand{and}~@{text "trm ="}\\+ −
\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\+ −
$|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\+ −
$|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\+ −
$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\+ −
$|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\+ −
$|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\+ −
$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\+ −
\isacommand{and}~@{text "assoc_lst ="}\\+ −
\phantom{$|$}~@{text ANil}~%+ −
$|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\+ −
\isacommand{and}~@{text "pat ="}\\+ −
\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\+ −
\isacommand{and}~@{text "vt_lst ="}\\+ −
\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\+ −
\isacommand{and}~@{text "tvtk_lst ="}\\+ −
\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\+ −
\isacommand{and}~@{text "tvck_lst ="}\\ + −
\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\+ −
\isacommand{binder}\\+ −
@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%+ −
@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\+ −
@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%+ −
@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\+ −
\isacommand{where}\\+ −
\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\+ −
$|$~@{text "bv1 VTNil = []"}\\+ −
$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\+ −
$|$~@{text "bv2 TVTKNil = []"}\\+ −
$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\+ −
$|$~@{text "bv3 TVCKNil = []"}\\+ −
$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\+ −
\end{tabular}+ −
\end{boxedminipage}+ −
\caption{The nominal datatype declaration for Core-Haskell. For the moment we+ −
do not support nested types; therefore we explicitly have to unfold the + −
lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved+ −
in a future version of Nominal Isabelle. Apart from that, the + −
declaration follows closely the original in Figure~\ref{corehas}. The+ −
point of our work is that having made such a declaration in Nominal Isabelle,+ −
one obtains automatically a reasoning infrastructure for Core-Haskell.+ −
\label{nominalcorehas}}+ −
\end{figure}+ −
*}+ −
+ −
+ −
section {* Strong Induction Principles *}+ −
+ −
text {*+ −
In the previous section we were able to provide induction principles that + −
allow us to perform structural inductions over alpha-equated terms. + −
We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},+ −
the induction hypothesis requires us to establish the implication+ −
%+ −
\begin{equation}\label{weakprem}+ −
@{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} + −
\end{equation}+ −
+ −
\noindent+ −
where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. + −
The problem with this implication is that in general it is not easy to establish it.+ −
The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"} + −
(for example we cannot assume the variable convention for them).+ −
+ −
In \cite{UrbanTasson05} we introduced a method for automatically+ −
strengthening weak induction principles for terms containing single+ −
binders. These stronger induction principles allow the user to make additional+ −
assumptions about binders. + −
These additional assumptions amount to a formal+ −
version of the informal variable convention for binders. A natural question is+ −
whether we can also strengthen the weak induction principles involving+ −
the general binders presented here. We will indeed be able to so, but for this we need an + −
additional notion for permuting deep binders. + −
+ −
Given a binding function @{text "bn"} we define an auxiliary permutation + −
operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.+ −
Assuming a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then+ −
we define %+ −
\begin{center}+ −
@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"}+ −
\end{center}+ −
+ −
\noindent+ −
with @{text "y\<^isub>i"} determined as follows:+ −
%+ −
\begin{center}+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\+ −
$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\+ −
$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to + −
alpha-equated terms. We can then prove the following two facts+ −
+ −
\begin{lemma}\label{permutebn} + −
Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}+ −
{\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}+ −
@{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.+ −
\end{lemma}+ −
+ −
\begin{proof} + −
By induction on @{text x}. The equations follow by simple unfolding + −
of the definitions. + −
\end{proof}+ −
+ −
\noindent+ −
The first property states that a permutation applied to a binding function is+ −
equivalent to first permuting the binders and then calculating the bound+ −
variables. The second amounts to the fact that permuting the binders has no + −
effect on the free-variable function. The main point of this permutation+ −
function, however, is that if we have a permutation that is fresh + −
for the support of an object @{text x}, then we can use this permutation + −
to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the + −
@{text "Let"} term-constructor from the example shown + −
\eqref{letpat} this means for a permutation @{text "r"}:+ −
%+ −
\begin{equation}\label{renaming}+ −
\begin{array}{l}+ −
\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\ + −
\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bnpat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}+ −
\end{array}+ −
\end{equation}+ −
+ −
\noindent+ −
This fact will be crucial when establishing the strong induction principles. + −
In our running example about @{text "Let"}, they state that instead + −
of establishing the implication + −
+ −
\begin{center}+ −
@{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}+ −
\end{center}+ −
+ −
\noindent+ −
it is sufficient to establish the following implication+ −
%+ −
\begin{equation}\label{strong}+ −
\mbox{\begin{tabular}{l}+ −
@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\+ −
\hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\+ −
\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\+ −
\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent + −
While this implication contains an additional argument, namely @{text c}, and + −
also additional universal quantifications, it is usually easier to establish.+ −
The reason is that we can make the freshness + −
assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily + −
chosen by the user as long as it has finite support.+ −
+ −
Let us now show how we derive the strong induction principles from the+ −
weak ones. In case of the @{text "Let"}-example we derive by the weak + −
induction the following two properties+ −
%+ −
\begin{equation}\label{hyps}+ −
@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} + −
@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}+ −
\end{equation} + −
+ −
\noindent+ −
For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} + −
assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). + −
By Property~\ref{avoiding} we+ −
obtain a permutation @{text "r"} such that + −
%+ −
\begin{equation}\label{rprops}+ −
@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}+ −
@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}+ −
\end{equation}+ −
+ −
\noindent+ −
hold. The latter fact and \eqref{renaming} give us+ −
+ −
\begin{center}+ −
\begin{tabular}{l}+ −
@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\+ −
\hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we are can equally+ −
establish+ −
+ −
\begin{center}+ −
@{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}+ −
\end{center}+ −
+ −
\noindent+ −
To do so, we will use the implication \eqref{strong} of the strong induction+ −
principle, which requires us to discharge+ −
the following four proof obligations:+ −
+ −
\begin{center}+ −
\begin{tabular}{rl}+ −
{\it i)} & @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\+ −
{\it ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\+ −
{\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\+ −
{\it iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it i)}; the + −
others from the induction hypotheses in \eqref{hyps} (in the fourth case+ −
we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).+ −
+ −
Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},+ −
we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.+ −
This completes the proof showing that the strong induction principle derives from+ −
the weak induction principle. For the moment we can derive the difficult cases of + −
the strong induction principles only by hand, but they are very schematically + −
so that with little effort we can even derive them for + −
Core-Haskell given in Figure~\ref{nominalcorehas}. + −
*}+ −
+ −
+ −
section {* Related Work *}+ −
+ −
text {*+ −
To our knowledge, the earliest usage of general binders in a theorem prover+ −
is described in \cite{NaraschewskiNipkow99} about a formalisation of the+ −
algorithm W. This formalisation implements binding in type schemes using a+ −
de-Bruijn indices representation. Since type schemes of W contain only a single+ −
binder, different indices do not refer to different binders (as in the usual+ −
de-Bruijn representation), but to different bound variables. A similar idea+ −
has been recently explored for general binders in the locally nameless+ −
approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist+ −
of two numbers, one referring to the place where a variable is bound and the+ −
other to which variable is bound. The reasoning infrastructure for both+ −
representations of bindings comes for free in the theorem provers, like Isabelle/HOL or+ −
Coq, as the corresponding term-calculi can be implemented as ``normal''+ −
datatypes. However, in both approaches it seems difficult to achieve our+ −
fine-grained control over the ``semantics'' of bindings (i.e.~whether the+ −
order of binders should matter, or vacuous binders should be taken into+ −
account). To do so, one would require additional predicates that filter out+ −
unwanted terms. Our guess is that such predicates results in rather+ −
intricate formal reasoning.+ −
+ −
Another representation technique for binding is higher-order abstract syntax+ −
(HOAS), which for example is implemented in the Twelf system. This representation+ −
technique supports very elegantly many aspects of \emph{single} binding, and+ −
impressive work is in progress that uses HOAS for mechanising the metatheory+ −
of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple+ −
binders of SML are represented in this work. Judging from the submitted+ −
Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with+ −
binding constructs where the number of bound variables is not fixed. For+ −
example in the second part of this challenge, @{text "Let"}s involve+ −
patterns that bind multiple variables at once. In such situations, HOAS+ −
representations have to resort to the iterated-single-binders-approach with+ −
all the unwanted consequences when reasoning about the resulting terms.+ −
+ −
Two formalisations involving general binders have also been performed in older+ −
versions of Nominal Isabelle \cite{BengtsonParow09, UrbanNipkow09}. Both+ −
use the approach based on iterated single binders. Our experience with+ −
the latter formalisation has been disappointing. The major pain arose from+ −
the need to ``unbind'' variables. This can be done in one step with our+ −
general binders, for example @{term "Abs as x"}, but needs a cumbersome+ −
iteration with single binders. The resulting formal reasoning turned out to+ −
be rather unpleasant. The hope is that the extension presented in this paper+ −
is a substantial improvement.+ −
+ −
The most closely related work to the one presented here is the Ott-tool \cite{ott-jfp}. This tool is a+ −
nifty front-end for creating \LaTeX{} documents from specifications of+ −
term-calculi involving general binders. For a subset of the specifications, Ott can also generate+ −
theorem prover code using a raw representation of terms, and in Coq also a+ −
locally nameless representation. The developers of this tool have also put+ −
forward (on paper) a definition for alpha-equivalence of terms that can be+ −
specified in Ott. This definition is rather different from ours, not using+ −
any nominal techniques. Although we were heavily inspired by their syntax,+ −
their definition of alpha-equivalence is unsuitable for our extension of+ −
Nominal Isabelle. First, it is far too complicated to be a basis for+ −
automated proofs implemented on the ML-level of Isabelle/HOL. Second, it+ −
covers cases of binders depending on other binders, which just do not make+ −
sense for our alpha-equated terms. Third, it allows empty types that have no+ −
meaning in a HOL-based theorem prover.+ −
+ −
Because of how we set up our definitions, we had to impose restrictions,+ −
like excluding overlapping deep binders, that are not present in Ott. Our+ −
expectation is that we can still cover many interesting term-calculi from+ −
programming language research, for example Core-Haskell. For providing support+ −
of neat features in Ott, such as subgrammars, the existing datatype+ −
infrastructure in Isabelle/HOL is unfortunately not powerful enough. On the+ −
other hand, we are not aware that Ott can make the distinction between our+ −
three different binding modes. Also, definitions for notions like the free+ −
variables of a term are work in progress in Ott.+ −
*}+ −
+ −
section {* Conclusion *}+ −
+ −
text {*+ −
We have presented an extension of Nominal Isabelle for deriving+ −
automatically a convenient reasoning infrastructure that can deal with+ −
general binders, that is term-constructors binding multiple variables at+ −
once. This extension has been tried out with the Core-Haskell+ −
term-calculus. For such general binders, we can also extend+ −
earlier work that derives strong induction principles which have the usual+ −
variable convention already built in. For the moment we can do so only with manual help,+ −
but future work will automate them completely. The code underlying the presented+ −
extension will become part of the Isabelle distribution, but for the moment+ −
it can be downloaded from the Mercurial repository linked at+ −
\href{http://isabelle.in.tum.de/nominal/download}+ −
{http://isabelle.in.tum.de/nominal/download}.+ −
+ −
We have left out a discussion about how functions can be defined over+ −
alpha-equated terms that involve general binders. In earlier versions of Nominal+ −
Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue. We+ −
hope to do better this time by using the function package that has recently+ −
been implemented in Isabelle/HOL and also by restricting function+ −
definitions to equivariant functions (for such functions it is possible to+ −
provide more automation).+ −
+ −
There are some restrictions we imposed in this paper, that we would like to lift in+ −
future work. One is the exclusion of nested datatype definitions. Nested+ −
datatype definitions allow one to specify, for instance, the function kinds+ −
in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded+ −
version @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}. For+ −
them we need a more clever implementation than we have at the moment. + −
+ −
More+ −
interesting is lifting our restriction about overlapping deep binders. Given+ −
our current setup, we cannot deal with specifications such as+ −
+ −
+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
@{text "Foo r::pat s::pat t::trm"} & + −
\isacommand{bind} @{text "bn(r)"} \isacommand{in} @{text t},\;+ −
\isacommand{bind} @{text "bn(s)"} \isacommand{in} @{text t}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
where the deep binders @{text "bn(r)"} and @{text "bn(s)"} overlap. + −
The difficulty is that we would need to implement such overlapping bindings + −
with alpha-equivalences like+ −
+ −
\begin{center}+ −
@{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)"}+ −
\end{center}+ −
+ −
\noindent+ −
or+ −
+ −
\begin{center}+ −
@{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)"}+ −
\end{center}+ −
+ −
\noindent+ −
Both versions require two permutations (for each binding). But unfortunately the + −
first version cannot work since it leaves some atoms unbound that should be + −
bound by the respective other binder. This problem is avoided in the second+ −
version, but at the expense that the two permutations can interfere with each + −
other. We have not yet been able to find a way to avoid such interferences. + −
On the other hand, such bindings can be made sense of informally \cite{SewellBestiary}.+ −
This suggest there should be an approriate notion of alpha-equivalence.+ −
+ −
Another interesting line of investigation is whether we can go beyond the + −
simple-minded form for binding functions that we adopted from Ott. At the moment, binding+ −
functions can only return the empty set, a singleton atom set or unions+ −
of atom sets (similarly for lists). It remains to be seen whether + −
properties like \eqref{bnprop} provide us with means to support more interesting+ −
binding functions. + −
+ −
+ −
We have also not yet played with other binding modes. For example we can+ −
imagine that there is need for a binding mode \isacommand{bind\_\#list} with+ −
an associated abstraction of the form+ −
%+ −
\begin{center}+ −
@{term "Abs_dist as x"}+ −
\end{center}+ −
+ −
\noindent+ −
where instead of lists, we abstract lists of distinct elements.+ −
Once we feel confident about such binding modes, our implementation + −
can be easily extended to accommodate them.+ −
+ −
\medskip+ −
\noindent+ −
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for + −
many discussions about Nominal Isabelle. We thank Peter Sewell for + −
making the informal notes \cite{SewellBestiary} available to us and + −
also for patiently explaining some of the finer points of the work on the Ott-tool. We+ −
also thank Stephanie Weirich for suggesting to separate the subgrammars+ −
of kinds and types in our Core-Haskell example. + −
*}+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −