(*<*)+ −
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"+ −
+ −
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+ −
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_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and+ −
Cons ("_::_" [78,77] 73) and+ −
supp_gen ("aux _" [1000] 10) and+ −
alpha_bn ("_ \<approx>bn _")+ −
+ −
(*>*)+ −
+ −
+ −
section {* Introduction *}+ −
+ −
text {*+ −
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 call @{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+ −
lifted 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 therefore can 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+ −
difficulty 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, at 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 order to simplify the description, 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 (see \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 also 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\\[-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 an equivariant function has empty support.+ −
+ −
Finally, the nominal logic work provides us with convenient 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 pinders 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}+ −
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"}.+ −
+ −
All properties given in this section are formalised in Isabelle/HOL and + −
most of proofs are described in \cite{HuffmanUrban10} to which we refer the+ −
reader. 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 @{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? (At 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.+ −
+ −
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 practise.+ −
For this consider the case of abstracting a set of variables over types (as in type-schemes). + −
We set @{text R} to be the equality 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. + −
+ −
% looks too ugly+ −
%\noindent+ −
%Let $\star$ range over $\{set, res, list\}$. We prove next under which + −
%conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence + −
%relations and equivariant:+ −
%+ −
%\begin{lemma}+ −
%{\it i)} Given the fact that $x\;R\;x$ holds, then + −
%$(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given+ −
%that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then+ −
%$(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies+ −
%$(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given+ −
%that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies + −
%@{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$+ −
%and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies+ −
%$(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given+ −
%@{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and+ −
%@{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then+ −
%$(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies+ −
%$(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star + −
%(p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.+ −
%\end{lemma}+ −
+ −
%\begin{proof}+ −
%All properties are by unfolding the definitions and simple calculations. + −
%\end{proof}+ −
+ −
+ −
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\_list}}$ + −
and $\approx_{\textit{abs\_res}}$). 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. The elements in these types + −
will be, respectively, written as:+ −
+ −
\begin{center}+ −
@{term "Abs as x"} \hspace{5mm} + −
@{term "Abs_lst as x"} \hspace{5mm}+ −
@{term "Abs_res as x"}+ −
\end{center}+ −
+ −
\noindent+ −
indicating that a set (or list) @{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 what the + −
support of abstractions is, 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}+ −
@{thm permute_Abs[no_vars]}+ −
\end{equation}+ −
+ −
\noindent+ −
The second fact derives from the definition of permutations acting on pairs + −
(see \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 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+ −
Thm~\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 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, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.+ −
+ −
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes of+ −
Theorem~\ref{suppabs}. The method of first considering abstractions of the+ −
form @{term "Abs as x"} etc is motivated by the fact that properties about them+ −
can be conveninetly established at the Isabelle/HOL level. It would be+ −
difficult 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 also 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"}$^\alpha_1$, \ldots, + −
@{text ty}$^\alpha_n$, and an associated collection+ −
of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text+ −
bn}$^\alpha_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}$^\alpha_1 = \ldots$\\+ −
\isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\+ −
$\ldots$\\ + −
\isacommand{and} @{text ty}$^\alpha_n = \ldots$\\ + −
\end{tabular}}+ −
\end{cases}$\\+ −
binding \mbox{function part} &+ −
$\begin{cases}+ −
\mbox{\begin{tabular}{l}+ −
\isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_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 comes 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 have+ −
+ −
\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) are 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>"}. There are ``positivity''+ −
restrictions imposed in the type of such recursive arguments, which ensure+ −
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 label}\\+ −
\isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\+ −
\isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\+ −
\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 the \emph{body} of the abstraction; the+ −
``\isacommand{bind}-part'' will be the \emph{binder} of the binding clause.+ −
+ −
In addition we distinguish between \emph{shallow} and \emph{deep}+ −
binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\;+ −
\isacommand{in}\; {\it label'} (similar for the other two modes). The+ −
restriction we impose on shallow binders is that the {\it label} must either+ −
refer to a type that is an atom type or to a type that is a finite set or+ −
list of an atom type. 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 in this specification \emph{name} refers to an atom type.+ −
If we have shallow binders that ``share'' a body, for instance $t$ in+ −
the following term-constructor+ −
+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
@{text "Foo x::name y::name t::lam"} & + −
\isacommand{bind} @{text x} \isacommand{in} @{text t},\;+ −
\isacommand{bind} @{text y} \isacommand{in} @{text t} + −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
then we have to make sure the modes of the binders agree. We cannot+ −
have, for instance, in the first binding clause the mode \isacommand{bind} + −
and in the second \isacommand{bind\_set}.+ −
+ −
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 lets + −
with tuple patterns might be specified as:+ −
+ −
\begin{center}+ −
\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{with}~@{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{center}+ −
+ −
\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 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. + −
+ −
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 above that the term-constructors @{text PVar} and @{text PTup} must not have a+ −
binding clause. 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 definitions and + −
proofs later on.+ −
+ −
The most drastic restriction we have to impose on deep binders is that + −
we cannot have ``overlapping'' deep binders. Consider for example the + −
term-constructors:+ −
+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
@{text "Foo p::pat q::pat t::trm"} & + −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;+ −
\isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text t}\\+ −
@{text "Foo' x::name p::pat t::trm"} & + −
\isacommand{bind} @{text x} \isacommand{in} @{text t},\;+ −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t} + −
+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
In the first case we might bind all atoms from the pattern @{text p} in @{text t}+ −
and also all atoms from @{text q} in @{text t}. As a result 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 represent 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 p::pat t::trm s::trm"} & + −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;+ −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\+ −
@{text "Bar' 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}+ −
+ −
\noindent+ −
since there is no overlap of binders.+ −
+ −
Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.+ −
Whenever such a binding clause is present, we will call the binder \emph{recursive}.+ −
To see the purpose for such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s:+ −
%+ −
\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 t},+ −
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text as}\\+ −
\isacommand{and} {\it assn} =\\+ −
\hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\+ −
\hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\+ −
\isacommand{with} @{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.+ −
+ −
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. Because of the problem+ −
Pottier and Cheney pointed out, we cannot in general re-arrange arguments of+ −
term-constructors so that binders and their bodies are next to each other, and+ −
then use the type constructors @{text "abs_set"}, @{text "abs_res"} and+ −
@{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first+ −
extract datatype definitions from the specification and then define + −
independently an alpha-equivalence relation over them.+ −
+ −
+ −
The datatype definition can be obtained by stripping off the + −
binding clauses and the labels on 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 user. In our implementation we just use the affix ``@{text "_raw"}''.+ −
But for the purpose of this paper, we just 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{center}+ −
@{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}+ −
\end{center}+ −
+ −
% TODO: we did not define permutation types+ −
%\noindent+ −
%From this definition we can easily show that the raw datatypes are + −
%all permutation types (Def ??) by a simple structural induction over+ −
%the @{text "ty"}s.+ −
+ −
The first non-trivial step we have to perform is the generation free-variable + −
functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}+ −
we need to define free-variable functions+ −
+ −
\begin{center}+ −
@{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}+ −
\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 need to define+ −
%+ −
\begin{center}+ −
@{text "fv_bn\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}+ −
\end{center}+ −
+ −
\noindent+ −
The reason for this setup is that in a deep binder not all atoms have to be+ −
bound, as we shall see in an example below. We need therefore the function+ −
that returns us those unbound atoms. + −
+ −
While the idea behind these+ −
free-variable functions is clear (they just collect all atoms that are not bound),+ −
because of the rather complicated binding mechanisms their definitions are+ −
somewhat involved.+ −
Given a term-constructor @{text "C"} of type @{text ty} with argument types+ −
\mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function+ −
@{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values+ −
calculated next for each argument. + −
First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses, + −
we can determine whether the argument is a shallow or deep+ −
binder, and in the latter case also whether it is a recursive or+ −
non-recursive binder. + −
+ −
\begin{center}+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
$\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\+ −
$\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep+ −
non-recursive binder with the auxiliary binding function @{text "bn"}\\+ −
$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is+ −
a deep recursive binder with the auxiliary binding function @{text "bn"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
The first clause states that shallow binders do not contribute to the+ −
free variables; in the second clause, we have to collect all+ −
variables that are left unbound by the binding function @{text "bn"}---this+ −
is done with function @{text "fv_bn"}; in the third clause, since the + −
binder is recursive, we need to bind all variables specified by + −
@{text "bn"}---therefore we subtract @{text "bn x\<^isub>i"} from the free+ −
variables of @{text "x\<^isub>i"}.+ −
+ −
In case the argument is \emph{not} a binder, we need to consider + −
whether the @{text "x\<^isub>i"} is the body of one or more binding clauses. + −
In this case we first calculate the set @{text "bnds"} as follows: + −
either the corresponding binders are all shallow or there is a single deep binder.+ −
In the former case we take @{text bnds} to be the union of all shallow + −
binders; in the latter case, we just take the set of atoms specified by the + −
binding function. The value for @{text "x\<^isub>i"} is then given by:+ −
+ −
\begin{equation}\label{deepbody}+ −
\mbox{%+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
$\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\+ −
$\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\+ −
$\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\+ −
$\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes+ −
corresponding to the types specified by the user\\+ −
% $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype+ −
% with a free-variable function @{text "fv\<^isup>\<alpha>"}\\+ −
$\bullet$ & @{term "{}"} otherwise+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent + −
Like the coercion function @{text atom} used above, @{text "atoms as"} coerces + −
the set @{text as} to the generic atom type.+ −
It is defined as @{text "atom as \<equiv> {atom a | a \<in> as}"}.+ −
+ −
The last case we need to consider is when @{text "x\<^isub>i"} is neither+ −
a binder nor a body of an abstraction. In this case it is defined + −
as in \eqref{deepbody}, except that we do not need to subtract the + −
set @{text bnds}.+ −
+ −
Next, we need to define a free-variable function @{text "fv_bn\<^isub>j"} for + −
each binding function @{text "bn\<^isub>j"}. The idea behind this+ −
function is to compute the set of free atoms that are not bound by + −
@{text "bn\<^isub>j"}. Because of the restrictions we imposed on the + −
form of binding functions, this can be done automatically by recursively + −
building up the the set of free variables from the arguments that are + −
not bound. Let us assume one clause of the binding function is + −
@{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j"} is the + −
union of the values calculated for @{text "x\<^isub>i"} of type @{text "ty\<^isub>i"}+ −
as follows:+ −
+ −
\begin{center}+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
\multicolumn{2}{l}{@{text "x\<^isub>i"} occurs in @{text "rhs"}:}\\ + −
$\bullet$ & @{term "{}"} provided @{term "x\<^isub>i"} is a single atom,+ −
atom list or atom set\\+ −
$\bullet$ & @{text "fv_bn x\<^isub>i"} in case @{text "rhs"} contains the + −
recursive call @{text "bn x\<^isub>i"}\medskip\\+ −
%+ −
\multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\+ −
$\bullet$ & @{text "atom x\<^isub>i"} provided @{term "x\<^isub>i"} is an atom\\+ −
$\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\+ −
$\bullet$ & @{term "atoms (set x\<^isub>i)"} provided @{term "x\<^isub>i"} is a list of atoms\\+ −
$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is one of the raw+ −
types corresponding to the types specified by the user\\+ −
% $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>i - bnds"} provided @{term "x\<^isub>i"} is not in @{text "rhs"}+ −
% and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\+ −
$\bullet$ & @{term "{}"} otherwise+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
To see how these definitions work in practise, let us reconsider the term-constructors + −
@{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}. + −
For this specification we need to define three 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>bn\<^esub> as \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\+ −
@{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} &\\+ −
\multicolumn{3}{r}{@{text "(fv\<^bsub>assn\<^esub> as - set (bn as)) \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}}\\[1mm]+ −
+ −
@{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\+ −
@{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 "="} & @{text "[]"}\\+ −
@{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 no 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 occurences of the atoms+ −
@{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text+ −
"set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from+ −
@{text "fv\<^bsub>trm\<^esub> t"}. 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+ −
(the term-constructors that have binding clauses). This is a phenomenon + −
that has also been pointed out in \cite{ott-jfp}. We can also see that+ −
given a @{text "bn"}-function for a type @{text "ty"}, then we have+ −
%+ −
\begin{equation}\label{bnprop}+ −
@{text "fv_ty x = bn x \<union> fv_bn x"}.+ −
\end{equation}+ −
+ −
Next we define alpha-equivalence 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 @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}.+ −
To simplify our definitions we will use the following abbreviations for + −
relations and free-variable acting on products.+ −
%+ −
\begin{center}+ −
\begin{tabular}{rcl}+ −
@{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 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume + −
@{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}).+ −
The task now is to specify what the premises of these clauses are. For this we+ −
consider the pairs @{text "(x\<^isub>i, y\<^isub>i)"}. We will analyse these pairs according to + −
``clusters'' of the binding clauses. There are the following cases:+ −
*}+ −
(*<*)+ −
consts alpha_ty ::'a+ −
notation alpha_ty ("\<approx>ty")+ −
(*>*)+ −
text {*+ −
\begin{itemize}+ −
\item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the + −
@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding binders. For the binding mode+ −
\isacommand{bind\_set} we generate the premise+ −
\begin{center}+ −
@{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty\<^isub>i p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}+ −
\end{center}+ −
+ −
Similarly for the other modes.+ −
+ −
\item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep non-recursive binders with type @{text "ty"}+ −
and with @{text bn} being the auxiliary binding function. We assume + −
@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}. + −
For the binding mode \isacommand{bind\_set} we generate the two premises+ −
+ −
\begin{center}+ −
@{text "x\<^isub>i \<approx>bn y\<^isub>i"}\\+ −
@{term "\<exists>p. (bn x\<^isub>i, (u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (v\<^isub>1,\<xi>,v\<^isub>m))"}+ −
\end{center}+ −
+ −
\noindent+ −
where @{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"}. Similarly for the other modes.+ −
+ −
\item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep recursive binders with type @{text "ty"}+ −
and with @{text bn} being the auxiliary binding function. We assume + −
@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}. + −
For the binding mode \isacommand{bind\_set} we generate the premise+ −
+ −
\begin{center}+ −
@{term "\<exists>p. (bn x\<^isub>i, (x\<^isub>i, u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (y\<^isub>i, v\<^isub>1,\<xi>,v\<^isub>m))"}+ −
\end{center}+ −
+ −
\noindent+ −
where @{text R} is @{text "\<approx>ty \<otimes> \<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is+ −
@{text "fv_ty \<oplus> fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other modes.+ −
\end{itemize}+ −
+ −
\noindent+ −
The only cases that are not covered by these rules is if @{text "(x\<^isub>i, y\<^isub>i)"} is+ −
neither a binder nor a body. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided+ −
the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are + −
recursive arguments of the term constructor. If they are non-recursive arguments+ −
then we generate @{text "x\<^isub>i = y\<^isub>i"}.+ −
+ −
TODO + −
+ −
The alpha-equivalence relations for binding functions are similar to the alpha-equivalences+ −
for their respective types, the difference is that they ommit checking the arguments that+ −
are bound. We assumed that there are no bindings in the type on which the binding function+ −
is defined so, there are no permutations involved. For a binding function clause + −
@{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent+ −
@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:+ −
\begin{center}+ −
\begin{tabular}{cp{7cm}}+ −
$\bullet$ & @{text "x\<^isub>j"} is not of a type being defined and occurs in @{text "rhs"}\\+ −
$\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not of a type being defined+ −
and does not occur in @{text "rhs"}\\+ −
$\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is of a type being defined+ −
occuring in @{text "rhs"} under the binding function @{text "bn\<^isub>m"}\\+ −
$\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
*}+ −
+ −
section {* The Lifting of Definitions and Properties *}+ −
+ −
text {*+ −
To define the quotient types we first need to show that the defined+ −
relations are equivalence relations.+ −
+ −
\begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"}+ −
defined as above are equivalence relations and are equivariant.+ −
\end{lemma}+ −
\begin{proof} Reflexivity by induction on the raw datatype. Symmetry,+ −
transitivity and equivariance by induction on the alpha equivalence+ −
relation. Using lemma \ref{alphaeq}, the conditions follow by simple+ −
calculations. \end{proof}+ −
+ −
\noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift+ −
the raw definitions to the quotient type, we need to prove that they+ −
\emph{respect} the relation. We follow the definition of respectfullness given+ −
by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition+ −
is that when a function (or constructor) is given arguments that are+ −
alpha-equivalent the results are also alpha equivalent. For arguments that are+ −
not of any of the relations taken into account, equivalence is replaced by+ −
equality. In particular the respectfullness condition for a @{text "bn"}+ −
function means that for alpha equivalent raw terms it returns the same bound+ −
names. Thanks to the restrictions on the binding functions introduced in+ −
Section~\ref{sec:alpha} we can show that are respectful.+ −
+ −
\begin{lemma} The functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"}, @{text "fv_ty\<^isub>1 \<dots> fv_ty\<^isub>n"},+ −
the raw constructors, the raw permutations and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are+ −
respectful w.r.t. the relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>n"}.+ −
\end{lemma}+ −
\begin{proof} Respectfullness of permutations is a direct consequence of+ −
equivariance. All other properties by induction on the alpha-equivalence+ −
relation. For @{text "bn"} the thesis follows by simple calculations thanks+ −
to the restrictions on the binding functions. For @{text "fv"} functions it+ −
follows using respectfullness of @{text "bn"}. For type constructors it is a+ −
simple calculation thanks to the way alpha-equivalence was defined. For @{text+ −
"alpha_bn"} after a second induction on the second relation by simple+ −
calculations. \end{proof}+ −
+ −
With these respectfullness properties we can use the quotient package+ −
to define the above constants on the quotient level. We can then automatically+ −
lift the theorems that talk about the raw constants to theorems on the quotient+ −
level. The following lifted properties are proved:+ −
+ −
\begin{center}+ −
\begin{tabular}{cp{7cm}}+ −
%skipped permute_zero and permute_add, since we do not have a permutation+ −
%definition+ −
$\bullet$ & permutation defining equations \\+ −
$\bullet$ & @{term "bn"} defining equations \\+ −
$\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\+ −
$\bullet$ & induction. The induction principle that we obtain by lifting+ −
is the weak induction principle, just on the term structure \\+ −
$\bullet$ & quasi-injectivity. This means the equations that specify+ −
when two constructors are equal and comes from lifting the alpha+ −
equivalence defining relations\\+ −
$\bullet$ & distinctness\\+ −
%may be skipped+ −
$\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
Until now we have not said anything about the support of the+ −
defined type. This is because we could not use the general definition of+ −
support in lifted theorems, since it does not preserve the relation.+ −
Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"},+ −
since the @{term "x"} is bound. On the raw level, before the binding is+ −
introduced the term has the support equal to @{text "{x}"}. + −
+ −
To show the support equations for the lifted types we want to use the+ −
Theorem \ref{suppabs}, so we start with showing that they have a finite+ −
support.+ −
+ −
\begin{lemma} The types @{text "ty\<^isup>\<alpha>\<^isub>1 \<dots> ty\<^isup>\<alpha>\<^isub>n"} have finite support.+ −
\end{lemma}+ −
\begin{proof}+ −
By induction on the lifted types. For each constructor its support is+ −
supported by the union of the supports of all arguments. By induction+ −
hypothesis we know that each of the recursive arguments has finite+ −
support. We also know that atoms and finite atom sets and lists that+ −
occur in the constructors have finite support. A union of finite+ −
sets is finite thus the support of the constructor is finite.+ −
\end{proof}+ −
+ −
% Very vague...+ −
\begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"}+ −
of this type:+ −
\begin{center}+ −
@{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}.+ −
\end{center}+ −
\end{lemma}+ −
\begin{proof}+ −
We will show this by induction together with equations that characterize+ −
@{term "fv_bn\<^isup>\<alpha>\<^isub>"} in terms of @{term "alpha_bn\<^isup>\<alpha>"}. For each of @{text "fv_bn\<^isup>\<alpha>"}+ −
functions this equaton is:+ −
\begin{center}+ −
@{term "{a. infinite {b. \<not> alpha_bn\<^isup>\<alpha> ((a \<rightleftharpoons> b) \<bullet> x) x}} = fv_bn\<^isup>\<alpha> x"}+ −
\end{center}+ −
+ −
In the induction we need to show these equations together with the goal+ −
for the appropriate constructors. We first transform the right hand sides.+ −
The free variable functions are applied to theirs respective constructors+ −
so we can apply the lifted free variable defining equations to obtain+ −
free variable functions applied to subterms minus binders. Using the+ −
induction hypothesis we can replace free variable functions applied to+ −
subterms by support. Using Theorem \ref{suppabs} we replace the differences+ −
by supports of appropriate abstractions.+ −
+ −
Unfolding the definition of supports on both sides of the equations we+ −
obtain by simple calculations the equalities.+ −
\end{proof}+ −
+ −
With the above equations we can substitute free variables for support in+ −
the lifted free variable equations, which gives us the support equations+ −
for the term constructors. With this we can show that for each binding in+ −
a constructors the bindings can be renamed. To rename a shallow binder+ −
or a deep recursive binder a permutation is sufficient. This is not the+ −
case for a deep non-recursive bindings. Take the term+ −
@{text "Let (ACons x (Vr x) ANil) (Vr x)"}, representing the language construct+ −
@{text "let x = x in x"}. To rename the binder the permutation cannot+ −
be applied to the whole assignment since it would rename the free @{term "x"}+ −
as well. To avoid this we introduce a new construction operation+ −
that applies a permutation under a binding function.+ −
+ −
For each binding function @{text "bn\<^isub>j :: ty\<^isub>i \<Rightarrow> \<dots>"} we define a permutation operation+ −
@{text "\<bullet>bn\<^isub>j\<^isub> :: perm \<Rightarrow> ty\<^isub>i \<Rightarrow> ty\<^isub>i"}. This operation permutes only the arguments+ −
that are bound by the binding function while also descending in the recursive subcalls.+ −
For each term constructor @{text "C x\<^isub>1 \<dots> x\<^isub>n"} the @{text "\<bullet>bn\<^isub>j"} operation applied+ −
to a permutation @{text "\<pi>"} and to this constructor equals the constructor applied+ −
to the values for each argument. Provided @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, the value+ −
for an argument @{text "x\<^isub>j"} is:+ −
\begin{center}+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
$\bullet$ & @{text "x\<^isub>i"} provided @{text "x\<^isub>i"} is not in @{text "rhs"}\\+ −
$\bullet$ & @{text "\<pi> \<bullet> x\<^isub>i"} provided @{text "x\<^isub>i"} is in @{text "rhs"} without a binding function\\+ −
$\bullet$ & @{text "\<pi> \<bullet>bn\<^isub>k x\<^isub>i"} provided @{text "bn\<^isub>k x\<^isub>i"} is @{text "rhs"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
The definition of @{text "\<bullet>bn"} is respectful (simple induction) so we can lift it+ −
and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this defnition is correct is:+ −
+ −
%% We could get this from ExLet/perm_bn lemma.+ −
\begin{lemma} For every bn function @{text "bn\<^isup>\<alpha>\<^isub>i"},+ −
\begin{center}+ −
@{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i l = bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i l)"}+ −
\end{center}+ −
\end{lemma}+ −
\begin{proof} By induction on the lifted type it follows from the definitions of+ −
permutations on the lifted type and the lifted defining eqautions of @{text "\<bullet>bn"}.+ −
\end{proof}+ −
+ −
+ −
+ −
*}+ −
+ −
(* @{thm "ACons_subst[no_vars]"}*)+ −
+ −
text {*+ −
%%% FIXME: The restricions should have already been described in previous sections?+ −
Restrictions+ −
+ −
\begin{itemize}+ −
\item non-emptiness+ −
\item positive datatype definitions+ −
\item finitely supported abstractions+ −
\item respectfulness of the bn-functions\bigskip+ −
\item binders can only have a ``single scope''+ −
\item all bindings must have the same mode+ −
\end{itemize}+ −
*}+ −
+ −
section {* Examples *}+ −
+ −
text {*+ −
+ −
\begin{figure}+ −
\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{\label{nominalcorehas}}+ −
\end{figure}+ −
*}+ −
+ −
+ −
+ −
+ −
section {* Adequacy *}+ −
+ −
section {* Related Work *}+ −
+ −
text {*+ −
To our knowledge the earliest usage of general binders in a theorem prover setting is + −
in the paper \cite{NaraschewskiNipkow99}, which describes a formalisation of + −
the algorithm W. This formalisation implements binding in type schemes using a + −
a de-Bruijn indices representation. Also recently an extension for general binders + −
has been proposed for the locally nameless approach to binding \cite{chargueraud09}. .+ −
But we have not yet seen it to be employed in a non-trivial formal verification.+ −
In both approaches, it seems difficult to achieve our fine-grained control over the+ −
``semantics'' of bindings (whether the order should matter, or vacous binders + −
should be taken into account). To do so, it is necessary to introduce predicates + −
that filter out some unwanted terms. This very likely results in intricate + −
formal reasoning.+ −
+ −
Higher-Order Abstract Syntax (HOAS) approaches to representing binders are+ −
nicely supported in the Twelf theorem prover and work is in progress to use+ −
HOAS in a mechanisation of the metatheory of SML+ −
\cite{LeeCraryHarper07}. HOAS supports elegantly reasoning about+ −
term-calculi with single binders. We are not aware how more complicated+ −
binders from SML are represented in HOAS, but we know that HOAS cannot+ −
easily deal with binding constructs where the number of bound variables is+ −
not fixed. An example is the second part of the POPLmark challenge where+ −
@{text "Let"}s involving patterns need to be formalised. In such situations+ −
HOAS needs to use essentially has to represent multiple binders with+ −
iterated single binders.+ −
+ −
An attempt of representing general binders in the old version of Isabelle + −
based also on iterating single binders is described in \cite{BengtsonParow09}. + −
The reasoning there turned out to be quite complex. + −
+ −
Ott is better with list dot specifications; subgrammars, is untyped; + −
+ −
*}+ −
+ −
+ −
section {* Conclusion *}+ −
+ −
text {*+ −
Complication when the single scopedness restriction is lifted (two + −
overlapping permutations)+ −
+ −
Future work: distinct list abstraction+ −
+ −
TODO: function definitions:+ −
+ −
+ −
The formalisation presented here will eventually 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}.\medskip+ −
*}+ −
+ −
text {*+ −
\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 about the abstract + −
definitions and about the implementation of the Ott-tool. We+ −
also thank Stephanie Weirich for suggesting to separate the subgrammars+ −
of kinds and types in our Core-Haskell example.+ −
+ −
+ −
+ −
+ −
*}+ −
+ −
+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −