substitution definition with 'next_name'.
(*<*)+ −
theory Paper+ −
imports "../Nominal/Nominal2" "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" + −
Abs_print :: "'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_set ("_ \<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 ("fa'(_')" [100] 100) and+ −
equal ("=") and+ −
alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + −
Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and+ −
Abs_lst ("[_]\<^bsub>list\<^esub>._") and+ −
Abs_dist ("[_]\<^bsub>#list\<^esub>._") and+ −
Abs_res ("[_]\<^bsub>res\<^esub>._") and+ −
Abs_print ("_\<^bsub>set\<^esub>._") and+ −
Cons ("_::_" [78,77] 73) and+ −
supp_set ("aux _" [1000] 10) and+ −
alpha_bn ("_ \<approx>bn _")+ −
+ −
consts alpha_trm ::'a+ −
consts fa_trm :: 'a+ −
consts alpha_trm2 ::'a+ −
consts fa_trm2 :: 'a+ −
consts ast :: 'a+ −
consts ast' :: 'a+ −
notation (latex output) + −
alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and+ −
fa_trm ("fa\<^bsub>trm\<^esub>") and+ −
alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and+ −
fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and+ −
ast ("'(as, t')") and+ −
ast' ("'(as', t\<PRIME> ')")+ −
+ −
(*>*)+ −
+ −
+ −
section {* Introduction *}+ −
+ −
text {*+ −
+ −
So far, Nominal Isabelle provided a mechanism for constructing+ −
$\alpha$-equated terms, for example lambda-terms+ −
+ −
\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 the 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}. x \<rightarrow> y"} + −
\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 @{text "x = 3"} and+ −
\mbox{@{text "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> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s) [t\<^isub>1,\<dots>,t\<^isub>n]"}+ −
\end{center}+ −
+ −
\noindent+ −
where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text+ −
"x\<^isub>i"} becomes bound in @{text s}. In this representation the term+ −
\mbox{@{text "\<LET> (\<lambda>x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal+ −
instance, but the lengths of the 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 in very messy+ −
reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will+ −
allow type specifications for @{text "\<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 that all the names the function @{text+ −
"bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily+ −
inspired by the syntax of the Ott-tool \cite{ott-jfp}. Though, Ott+ −
has only one binding mode, namely the one where the order of+ −
binders matters. Consequently, type-schemes with binding sets+ −
of names cannot be modelled in Ott.+ −
+ −
However, we will not be able to cope with all specifications that are+ −
allowed by Ott. One reason is that Ott lets the user 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 with $\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); then identify 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 three new definitions for when terms+ −
involving general 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 strong + −
induction principles that have the variable convention already built in.+ −
The method behind our specification of general binders is taken + −
from the Ott-tool, but we introduce crucial restrictions, and also extensions, so + −
that our specifications make sense for reasoning about $\alpha$-equated terms. The main improvement over Ott is that we introduce three binding modes,+ −
provide precise definitions for $\alpha$-equivalence and for free+ −
variables of our terms, and provide automated proofs inside the+ −
Isabelle theorem prover.+ −
+ −
+ −
\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 System @{text "F\<^isub>C"}+ −
\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this+ −
version of @{text "F\<^isub>C"} 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 purpose of atoms is to represent variables, be they bound or free. + −
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}, leaves + −
@{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+ −
%+ −
\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}+ −
Given a set @{text "as"} of atoms.+ −
{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", 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 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"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}+ −
\end{center}+ −
+ −
Finally, the nominal logic work provides us with general means for renaming + −
binders. While in the older version of Nominal Isabelle, we used extensively + −
Property~\ref{swapfreshfresh} to rename single binders, this property + −
proved too 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 + −
extensive use of these properties in order to define $\alpha$-equivalence in + −
the presence of multiple binders.+ −
*}+ −
+ −
+ −
section {* General Bindings\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 question, we identify four conditions: {\it (i)}+ −
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom+ −
set"}}, then @{text x} and @{text y} need to have the same set of free+ −
atoms; moreover there must be a permutation @{text p} such that {\it+ −
(ii)} @{text p} leaves the free atoms 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 that {\it (iv)}+ −
@{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@ {\hspace{4mm}}r}+ −
\multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]+ −
& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\+ −
@{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\+ −
@{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\+ −
@{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ + −
\end{array}+ −
\end{equation}+ −
+ −
\noindent+ −
Note that this relation depends 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-atom function @{text "fa"} 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, @{text R} will be replaced by equality @{text "="} and we+ −
will prove that @{text "fa"} is equal to @{text "supp"}.+ −
+ −
The definition in \eqref{alphaset} does not make any distinction between the+ −
order of abstracted atoms. 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@ {\hspace{4mm}}r}+ −
\multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]+ −
& @{term "fa(x) - (set as) = fa(y) - (set bs)"} & \mbox{\it (i)}\\+ −
\wedge & @{term "(fa(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\+ −
\wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\+ −
\wedge & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ + −
\end{array}+ −
\end{equation}+ −
+ −
\noindent+ −
where @{term set} is the 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@ {\hspace{4mm}}r}+ −
\multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]+ −
& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\+ −
\wedge & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\+ −
\wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\+ −
\end{array}+ −
\end{equation}+ −
+ −
It might be useful to consider first some examples about how these definitions+ −
of $\alpha$-equivalence pan out in practice. For this consider the case of+ −
abstracting a set of atoms over types (as in type-schemes). We set+ −
@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we+ −
define+ −
+ −
\begin{center}+ −
@{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(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 three 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_set (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 for introducing + −
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_set 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 in an abstraction.+ −
+ −
\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+ −
Assuming that @{text "x"} has finite support, 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_set.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_set as x)) \<subseteq> supp (Abs_set 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_set 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 {* Specifying General Bindings\label{sec:spec} *}+ −
+ −
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 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 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 bodies}\\+ −
\isacommand{bind (set)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\+ −
\isacommand{bind (res)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\+ −
\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). As indicated, the labels in the ``\isacommand{in}-part'' of a binding+ −
clause will be called \emph{bodies}; the+ −
``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to+ −
Ott, we allow multiple labels in binders and bodies. For example we allow+ −
binding clauses of the form:+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}ll@ {}}+ −
@{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} & + −
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\+ −
@{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} & + −
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, + −
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
Similarly for the other binding modes. + −
%Interestingly, in case of \isacommand{bind (set)}+ −
%and \isacommand{bind (res)} the binding clauses above will make a difference to the semantics+ −
%of the specifications (the corresponding $\alpha$-equivalence will differ). We will + −
%show this later with an example.+ −
+ −
There are also some restrictions we need to impose on our binding clauses in comparison to+ −
the ones of Ott. The+ −
main idea behind these restrictions is that we obtain a sensible notion of+ −
$\alpha$-equivalence where it is ensured that within a given scope an + −
atom occurrence cannot be both bound and free at the same time. The first+ −
restriction is that a body can only occur in+ −
\emph{one} binding clause of a term constructor (this ensures that the bound+ −
atoms of a body cannot be free at the same time by specifying an+ −
alternative binder for the same body). For binders we distinguish between+ −
\emph{shallow} and \emph{deep} binders. Shallow binders are just+ −
labels. The restriction we need to impose on them is that in case of+ −
\isacommand{bind (set)} and \isacommand{bind (res)} the labels must either+ −
refer to atom types or to sets of atom types; in case of \isacommand{bind}+ −
the labels must 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{-2mm}}}+ −
\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{21mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\+ −
\end{tabular}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
In these specifications @{text "name"} refers to an atom type, and @{text+ −
"fset"} to the type of finite sets.+ −
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 \isacommand{bind} in the second case makes a+ −
difference to the semantics of the specification (which we will define in the next section).+ −
+ −
+ −
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 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 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)"}\smallskip\\ + −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
In this specification the function @{text "bn"} determines which atoms of+ −
the pattern @{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.+ −
+ −
As said above, for deep binders we allow binding clauses such as+ −
%+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
@{text "Bar p::pat t::trm"} & + −
\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
where the argument of the deep binder also occurs in the body. We call such+ −
binders \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 associated+ −
notions of free-atoms and $\alpha$-equivalence.+ −
+ −
To make sure that atoms bound by deep binders cannot be free at the+ −
same time, we cannot have more than one binding function for a deep binder. + −
Consequently we exclude specifications such as+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}+ −
@{text "Baz\<^isub>1 p::pat t::trm"} & + −
\isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\+ −
@{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & + −
\isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},+ −
\isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick + −
out different atoms to become bound, respectively be free, in @{text "p"}.+ −
(Since the Ott-tool does not derive a reasoning infrastructure for + −
$\alpha$-equated terms, it can permit such specifications.)+ −
+ −
We also need to restrict the form of the binding functions in order + −
to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated + −
terms. The main restriction is that we cannot return an atom in a binding function that is also+ −
bound in the corresponding term-constructor. That means in \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 a binding clause involving the argument @{text t} (the only one that+ −
is \emph{not} used in the definition of the binding function). This restriction+ −
is sufficient for having the binding function over $\alpha$-equated terms.+ −
+ −
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 definitions and proofs+ −
later on.+ −
+ −
In order to simplify our definitions of free atoms and $\alpha$-equivalence, + −
we shall assume specifications + −
of term-calculi are implicitly \emph{completed}. By this we mean that + −
for every argument of a term-constructor that is \emph{not} + −
already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding+ −
clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. 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 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. + −
*}+ −
+ −
section {* Alpha-Equivalence and Free Atoms\label{sec:alpha} *}+ −
+ −
text {*+ −
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 in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}. + −
Therefore we will first+ −
extract ``raw'' datatype definitions from the specification and then define + −
explicitly an $\alpha$-equivalence relation over them. We subsequently+ −
quotient the datatypes according to our $\alpha$-equivalence.+ −
+ −
+ −
The ``raw'' 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 in-depth description of the datatype package+ −
in Isabelle/HOL). We subsequently define each of the user-specified binding + −
functions @{term "bn"}$_{1..m}$ by recursion over the corresponding + −
raw datatype. We can also easily define permutation operations by + −
recursion so that for each term constructor @{text "C"} 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 of+ −
free-atom functions from the specification. For the + −
\emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions+ −
%+ −
\begin{equation}\label{fvars}+ −
@{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}+ −
\end{equation}+ −
+ −
\noindent+ −
by mutual recursion.+ −
We define these functions together with auxiliary free-atom functions for+ −
the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ + −
we define+ −
%+ −
\begin{center}+ −
@{text "fa_bn\<^isub>1, \<dots>, fa_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 free atoms in a deep binder.+ −
+ −
While the idea behind these free-atom 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 "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text+ −
"fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text+ −
"fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding+ −
clause means. We only show the details for the mode \isacommand{bind (set)} (the other modes are similar). + −
Suppose the binding clause @{text bc\<^isub>i} is of the form + −
%+ −
\begin{center}+ −
\mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}+ −
\end{center}+ −
+ −
\noindent+ −
in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,+ −
and the binders @{text b}$_{1..p}$+ −
either refer to labels of atom types (in case of shallow binders) or to binding + −
functions taking a single label as argument (in case of deep binders). Assuming + −
@{text "D"} stands for the set of free atoms of the bodies, @{text B} for the + −
set of binding atoms in the binders and @{text "B'"} for the set of free atoms in + −
non-recursive deep binders,+ −
then the free atoms of the binding clause @{text bc\<^isub>i} are+ −
%+ −
\begin{equation}\label{fadef}+ −
\mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.+ −
\end{equation}+ −
+ −
\noindent+ −
The set @{text D} is formally defined as+ −
%+ −
\begin{center}+ −
@{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}+ −
\end{center} + −
+ −
\noindent+ −
where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the + −
specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function + −
we are defining by recursion + −
(see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.+ −
+ −
In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions+ −
for atom types to which shallow binders may refer+ −
%+ −
\begin{center}+ −
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\+ −
@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\+ −
@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent + −
Like the function @{text atom}, the function @{text "atoms"} coerces + −
a set of atoms to a set of the generic atom type. It is defined as + −
@{text "atoms as \<equiv> {atom a | a \<in> as}"}. + −
The set @{text B} is then formally defined as+ −
%+ −
\begin{center}+ −
@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}+ −
\end{center} + −
+ −
\noindent + −
where we use the auxiliary binding functions for shallow binders. + −
The set @{text "B'"} collects all free atoms in non-recursive deep+ −
binders. Let us assume these binders in @{text "bc\<^isub>i"} are+ −
%+ −
\begin{center}+ −
@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}+ −
\end{center}+ −
+ −
\noindent+ −
with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the + −
@{text "l"}$_{1..r}$ being among the bodies @{text+ −
"d"}$_{1..q}$. The set @{text "B'"} is defined as+ −
%+ −
\begin{center}+ −
@{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}+ −
\end{center} + −
+ −
\noindent+ −
This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.+ −
+ −
Note that for non-recursive deep binders, we have to add in \eqref{fadef}+ −
the set of atoms that are left unbound by the binding functions @{text+ −
"bn"}$_{1..m}$. We used for the definition of+ −
this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual+ −
recursion. Assume the user specified a @{text bn}-clause of the form+ −
%+ −
\begin{center}+ −
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}+ −
\end{center}+ −
+ −
\noindent+ −
where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of+ −
the arguments we calculate the free atoms as follows:+ −
%+ −
\begin{center}+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
$\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"} + −
(that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\\+ −
$\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}+ −
with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\+ −
$\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"},+ −
but without a recursive call.+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.+ −
+ −
To see how these definitions work in practice, let us reconsider the+ −
term-constructors @{text "Let"} and @{text "Let_rec"} shown in+ −
\eqref{letrecs} together with the term-constructors for assignments @{text+ −
"ANil"} and @{text "ACons"}. Since there is a binding function defined for+ −
assignments, we have three free-atom functions, namely @{text+ −
"fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text+ −
"fa\<^bsub>bn\<^esub>"} as follows:+ −
%+ −
\begin{center}+ −
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}+ −
@{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\+ −
@{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]+ −
+ −
@{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\+ −
@{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]+ −
+ −
@{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\+ −
@{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
Recall that @{text ANil} and @{text "ACons"} have no+ −
binding clause in the specification. The corresponding free-atom+ −
function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms+ −
occurring in an assignment (in case of @{text "ACons"}, they are given in+ −
terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). + −
The binding only takes place in @{text Let} and+ −
@{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies+ −
that all atoms given by @{text "set (bn as)"} have to be bound in @{text+ −
t}. Therefore we have to subtract @{text "set (bn as)"} from @{text+ −
"fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are+ −
free in @{text "as"}. This is+ −
in contrast with @{text "Let_rec"} where we have a recursive+ −
binder to bind all occurrences of the atoms in @{text+ −
"set (bn as)"} also inside @{text "as"}. Therefore we have to subtract+ −
@{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. + −
Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the + −
list of assignments, but instead returns the free atoms, which means in this + −
example the free atoms in the argument @{text "t"}. + −
+ −
An interesting point in this+ −
example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any+ −
atoms, even if the binding function is specified over assignments. + −
Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will+ −
some atoms actually become bound. This is a phenomenon that has also been pointed+ −
out in \cite{ott-jfp}. For us this observation is crucial, because we would + −
not be able to lift the @{text "bn"}-functions to $\alpha$-equated terms if they act on + −
atoms that are bound. In that case, these functions would \emph{not} respect+ −
$\alpha$-equivalence.+ −
+ −
Next we define the $\alpha$-equivalence relations for the raw types @{text+ −
"ty"}$_{1..n}$ from the specification. We write them as+ −
%+ −
\begin{center}+ −
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. + −
\end{center}+ −
+ −
\noindent+ −
Like with the free-atom functions, we also need to+ −
define auxiliary $\alpha$-equivalence relations + −
%+ −
\begin{center}+ −
@{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}+ −
\end{center}+ −
+ −
\noindent+ −
for the binding functions @{text "bn"}$_{1..m}$, + −
To simplify our definitions we will use the following abbreviations for+ −
\emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples+ −
%+ −
\begin{center}+ −
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
@{text "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} & \\+ −
\multicolumn{3}{r}{@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}}\\+ −
@{text "(fa\<^isub>1,.., fa\<^isub>n) (x\<^isub>1,.., x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> .. \<union> fa\<^isub>n x\<^isub>n"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
+ −
The $\alpha$-equivalence relations are defined as inductive predicates+ −
having a single clause for each term-constructor. Assuming a+ −
term-constructor @{text C} is of type @{text ty} and has the binding clauses+ −
@{term "bc"}$_{1..k}$, then the $\alpha$-equivalence clause has the form+ −
%+ −
\begin{center}+ −
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n \<approx>ty C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}+ −
{@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}} + −
\end{center}+ −
+ −
\noindent+ −
The task below is to specify what the premises of a binding clause are. As a+ −
special instance, we first treat the case where @{text "bc\<^isub>i"} is the+ −
empty binding clause of the form+ −
%+ −
\begin{center}+ −
\mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}+ −
\end{center}+ −
+ −
\noindent+ −
In this binding clause no atom is bound and we only have to $\alpha$-relate the bodies. For this+ −
we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"} + −
whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and+ −
respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate+ −
two such tuples we define the compound $\alpha$-equivalence relation @{text "R"} as follows+ −
%+ −
\begin{equation}\label{rempty}+ −
\mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}+ −
\end{equation}+ −
+ −
\noindent+ −
with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and + −
@{text "d\<PRIME>\<^isub>i"} refer+ −
to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise+ −
we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define+ −
the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"},+ −
which can be unfolded to the series of premises+ −
%+ −
\begin{center}+ −
@{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1 \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}+ −
\end{center}+ −
+ −
\noindent+ −
We will use the unfolded version in the examples below.+ −
+ −
Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form + −
%+ −
\begin{equation}\label{nonempty}+ −
\mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}+ −
\end{equation}+ −
+ −
\noindent+ −
In this case we define a premise @{text P} using the relation+ −
$\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly+ −
$\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other+ −
binding modes). This premise defines $\alpha$-equivalence of two abstractions+ −
involving multiple binders. As above, we first build the tuples @{text "D"} and+ −
@{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding+ −
compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). + −
For $\approx_{\,\textit{set}}$ we also need+ −
a compound free-atom function for the bodies defined as+ −
%+ −
\begin{center}+ −
\mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}+ −
\end{center}+ −
+ −
\noindent+ −
with the assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.+ −
The last ingredient we need are the sets of atoms bound in the bodies.+ −
For this we take+ −
+ −
\begin{center}+ −
@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\+ −
\end{center}+ −
+ −
\noindent+ −
Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This + −
lets us formally define the premise @{text P} for a non-empty binding clause as:+ −
%+ −
\begin{center}+ −
\mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.+ −
\end{center}+ −
+ −
\noindent+ −
This premise accounts for $\alpha$-equivalence of the bodies of the binding+ −
clause. + −
However, in case the binders have non-recursive deep binders, this premise+ −
is not enough:+ −
we also have to ``propagate'' $\alpha$-equivalence inside the structure of+ −
these binders. An example is @{text "Let"} where we have to make sure the+ −
right-hand sides of assignments are $\alpha$-equivalent. For this we use + −
relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).+ −
Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are+ −
%+ −
\begin{center}+ −
@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.+ −
\end{center}+ −
+ −
\noindent+ −
The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})+ −
and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}. + −
All premises for @{text "bc\<^isub>i"} are then given by+ −
%+ −
\begin{center}+ −
@{text "prems(bc\<^isub>i) \<equiv> P \<and> L R' L'"}+ −
\end{center} + −
+ −
\noindent + −
The auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ + −
in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form+ −
%+ −
\begin{center}+ −
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}+ −
\end{center}+ −
+ −
\noindent+ −
where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,+ −
then the corresponding $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form+ −
%+ −
\begin{center}+ −
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}+ −
{@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}+ −
\end{center}+ −
+ −
\noindent+ −
In this clause the relations @{text "R"}$_{1..s}$ are given by + −
+ −
\begin{center}+ −
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}+ −
$\bullet$ & @{text "z\<^isub>i \<approx>ty z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and + −
is a recursive argument of @{text C},\\+ −
$\bullet$ & @{text "z\<^isub>i = z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs}+ −
and is a non-recursive argument of @{text C},\\+ −
$\bullet$ & @{text "z\<^isub>i \<approx>bn\<^isub>i z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs}+ −
with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\+ −
$\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a+ −
recursive call.+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
This completes the definition of $\alpha$-equivalence. As a sanity check, we can show+ −
that the premises of empty binding clauses are a special case of the clauses for + −
non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}+ −
for the existentially quantified permutation).+ −
+ −
Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}+ −
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and+ −
$\approx_{\textit{bn}}$ with the following clauses:+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}c @ {}}+ −
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}+ −
{@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\+ −
\makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}+ −
{@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}c @ {}}+ −
\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\smallskip\\+ −
\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"}}{}\smallskip\\+ −
\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. This is needed in the + −
in the clause for @{text "Let"} (which is has+ −
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 all components of an assignment are ``under'' the binder. + −
*}+ −
+ −
section {* Establishing the Reasoning Infrastructure *}+ −
+ −
text {*+ −
Having made all necessary definitions for raw terms, we can start+ −
with establishing the reasoning infrastructure for the $\alpha$-equated types+ −
@{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch+ −
in this section the proofs we need for establishing this infrastructure. One+ −
main point of our work is that we have completely automated these proofs in Isabelle/HOL.+ −
+ −
First we establish that the+ −
$\alpha$-equivalence relations defined in the previous section are + −
equivalence relations.+ −
+ −
\begin{lemma}\label{equiv} + −
Given the raw types @{text "ty"}$_{1..n}$ and binding functions+ −
@{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and + −
@{text "\<approx>bn"}$_{1..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 built 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"}$^\alpha_{1..n}$ representing $\alpha$-equated terms of types @{text "ty"}$_{1..n}$. + −
We also obtain definitions for the term-constructors @{text+ −
"C"}$^\alpha_{1..k}$ from the raw term-constructors @{text+ −
"C"}$_{1..k}$, and similar definitions for the free-atom functions @{text+ −
"fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text+ −
"bn"}$^\alpha_{1..m}$. 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 for the user is the fact that distinct + −
term-constructors are not + −
equal, that is+ −
%+ −
\begin{equation}\label{distinctalpha}+ −
\mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~% + −
@{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}} + −
\end{equation}+ −
+ −
\noindent+ −
whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.+ −
In order to derive this fact, we use the definition of $\alpha$-equivalence+ −
and establish that+ −
%+ −
\begin{equation}\label{distinctraw}+ −
\mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}+ −
\end{equation}+ −
+ −
\noindent+ −
holds for the corresponding raw term-constructors.+ −
In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient+ −
package needs to know that the raw term-constructors @{text "C"} and @{text "D"} + −
are \emph{respectful} w.r.t.~the $\alpha$-equivalence relations (see \cite{Homeier05}).+ −
Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types+ −
@{text "ty"}$_{1..r}$, respectfulness amounts to showing that+ −
%+ −
\begin{center}+ −
@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}+ −
\end{center} + −
+ −
\noindent+ −
holds under the assumptions that we have \mbox{@{text+ −
"x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}+ −
and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and+ −
@{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this+ −
implication by applying the corresponding rule in our $\alpha$-equivalence+ −
definition and by establishing the following auxiliary facts + −
%+ −
\begin{equation}\label{fnresp}+ −
\mbox{%+ −
\begin{tabular}{l}+ −
@{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"}\\+ −
@{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"}\\+ −
@{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\+ −
@{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\+ −
\end{tabular}}+ −
\end{equation}+ −
+ −
\noindent+ −
They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first,+ −
second and last implication are true by how we stated our definitions, the + −
third \emph{only} holds because of our restriction+ −
imposed on the form of the binding functions---namely \emph{not} returning + −
any bound atoms. In Ott, in contrast, the user may + −
define @{text "bn"}$_{1..m}$ so that they return bound+ −
atoms and in this case the third implication is \emph{not} true. A + −
result is that the lifing of the corresponding binding functions in Ott to $\alpha$-equated+ −
terms is impossible.+ −
+ −
Having established respectfulness for the raw term-constructors, the + −
quotient package is able to automatically deduce \eqref{distinctalpha} from + −
\eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can + −
also lift properties that characterise when two raw terms of the form+ −
%+ −
\begin{center}+ −
@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}+ −
\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>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}+ −
\end{center}+ −
+ −
\noindent+ −
We call these conditions as \emph{quasi-injectivity}. They correspond to+ −
the premises in our $\alpha$-equivalence relations.+ −
+ −
Next we can lift the permutation + −
operations defined in \eqref{ceqvt}. In order to make this + −
lifting to go through, we have to show that the permutation operations are respectful. + −
This amounts to showing that the + −
$\alpha$-equivalence relations are equivariant, which we already established + −
in Lemma~\ref{equiv}. As a result we can add the equations+ −
%+ −
\begin{equation}\label{calphaeqvt}+ −
@{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}+ −
\end{equation}+ −
+ −
\noindent+ −
to our infrastructure. In a similar fashion we can lift the defining equations+ −
of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and+ −
@{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text+ −
"bn\<AL>"}$_{1..m}$ and the size functions @{text "size_ty\<AL>"}$_{1..n}$.+ −
The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$+ −
by the datatype package of Isabelle/HOL.+ −
+ −
Finally we can add to our infrastructure a structural induction principle + −
for the types @{text "ty\<AL>"}$_{i..n}$ whose + −
conclusion of the form+ −
%+ −
\begin{equation}\label{weakinduct}+ −
\mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}+ −
\end{equation} + −
+ −
\noindent+ −
whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ + −
have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each+ −
term constructor @{text "C"}$^\alpha$ a premise of the form+ −
%+ −
\begin{equation}\label{weakprem}+ −
\mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}} + −
\end{equation}+ −
+ −
\noindent + −
in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are + −
the recursive arguments of @{text "C\<AL>"}. + −
+ −
By working now completely on the $\alpha$-equated level, we+ −
can first show that the free-atom functions and binding functions are+ −
equivariant, namely+ −
%+ −
\begin{center}+ −
\begin{tabular}{rcl}+ −
@{text "p \<bullet> (fa_ty\<AL>\<^isub>i x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"}\\+ −
@{text "p \<bullet> (fa_bn\<AL>\<^isub>j x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\+ −
@{text "p \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
These properties can be established using the induction principle+ −
in \eqref{weakinduct}.+ −
Having these equivariant properties established, we can+ −
show for every term-constructor @{text "C\<^sup>\<alpha>"} that + −
+ −
\begin{center}+ −
@{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}+ −
\end{center}+ −
+ −
\noindent+ −
holds. This together with Property~\ref{supportsprop} allows us to prove+ −
that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported, + −
namely @{text "finite (supp x)"}. This can be again shown by induction + −
over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of + −
elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.+ −
This fact is important in a nominal setting, but also provides evidence + −
that our notions of free-atoms and $\alpha$-equivalence are correct.+ −
+ −
\begin{lemma} + −
For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have+ −
@{text "supp x = fa_ty\<AL>\<^isub>i x"}.+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
The proof is by induction. In each case+ −
we unfold the definition of @{text "supp"}, move the swapping inside the + −
term-constructors and then use the 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 this section, we can established automatically a reasoning infrastructure+ −
for the types @{text "ty\<AL>"}$_{1..n}$ + −
by first lifting definitions from the raw level to the quotient level and+ −
then by establishing facts about these lifted definitions. All necessary proofs+ −
are generated automatically by custom ML-code. This code can deal with + −
specifications such as 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 cvar 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 the + −
term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},+ −
the induction hypothesis requires us to establish the implications \eqref{weakprem}.+ −
The problem with these implications is that in general they are difficult to establish.+ −
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 given as + −
%+ −
\begin{center}+ −
@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, + −
\end{center}+ −
+ −
\noindent + −
then we define + −
%+ −
\begin{center}+ −
@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} + −
\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>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}+ −
@{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> 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+ −
atoms. The second amounts to the fact that permuting the binders has no + −
effect on the free-atom 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 + −
in \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>\<AL>\<^bsub>bn_pat\<^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 below.+ −
+ −
+ −
In our running example about @{text "Let"}, the strong induction+ −
principle means 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 have 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>\<AL>\<^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>\<AL>\<^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 can equally+ −
establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.+ −
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>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\+ −
{\it (ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^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 weak induction principles imply + −
the strong induction principles. + −
*}+ −
+ −
+ −
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 in W contain only a single+ −
place where variables are bound, 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 theorem provers like Isabelle/HOL or+ −
Coq, since 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 result 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 has been done 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 been + −
performed in older+ −
versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W + −
\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 described in this paper, 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} and the C$\alpha$ml language \cite{Pottier06}. Ott 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. To our+ −
knowledge there is also no concrete mathematical result concerning this+ −
notion of $\alpha$-equivalence. A definition for the notion of free variables+ −
is work in progress in Ott.+ −
+ −
Although we were heavily inspired by the syntax in Ott,+ −
its 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. We also had to generalise slightly Ott's + −
binding clauses. In Ott you specify binding clauses with a single body; we + −
allow more than one. We have to do this, because this makes a difference + −
for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and + −
\isacommand{bind (res)}. Consider the examples+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}+ −
@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} & + −
\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\+ −
@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} & + −
\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, + −
\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
In the first term-constructor we have a single+ −
body that happens to be ``spread'' over two arguments; in the second term-constructor we have+ −
two independent bodies in which the same variables are bound. As a result we + −
have+ −
+ −
\begin{center}+ −
\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}+ −
@{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & + −
@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\+ −
@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & + −
@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
and therefore need the extra generality to be able to distinguish between + −
both specifications.+ −
Because of how we set up our definitions, we also had to impose some restrictions+ −
(like a single binding function for a deep binder) 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. + −
+ −
Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for + −
representing terms with general binders inside OCaml. This language is+ −
implemented as a front-end that can be translated to OCaml with the help of+ −
a library. He presents a type-system in which the scope of general binders+ −
can be specified using special markers, written @{text "inner"} and + −
@{text "outer"}. It seems our and his specifications can be+ −
inter-translated as long as ours use the binding mode + −
\isacommand{bind} only.+ −
However, we have not proved this. Pottier gives a definition for + −
$\alpha$-equivalence, which also uses a permutation operation (like ours).+ −
Still, this definition is rather different from ours and he only proves that+ −
it defines an equivalence relation. A complete+ −
reasoning infrastructure is well beyond the purposes of his language. + −
+ −
In a slightly different domain (programming with dependent types), the + −
paper \cite{Altenkirch10} presents a calculus with a notion of + −
$\alpha$-equivalence related to our binding mode \isacommand{bind (res)}.+ −
The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it+ −
has a more operational flavour and calculates a partial (renaming) map. + −
In this way, the definition can deal with vacuous binders. However, to our+ −
best knowledge, no concrete mathematical result concerning this+ −
definition of $\alpha$-equivalence has been proved. + −
*}+ −
+ −
section {* Conclusion *}+ −
+ −
text {*+ −
We have presented an extension of Nominal Isabelle for dealing with+ −
general binders, that is term-constructors having multiple bound + −
variables. For this extension we introduced new definitions of + −
$\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.+ −
To specify general binders we used the specifications from Ott, but extended them + −
in some places and restricted+ −
them in others so that they make sense in the context of $\alpha$-equated terms. We also introduced two binding modes (set and res) that do not + −
exist in Ott. + −
We have tried out the extension with terms from Core-Haskell, type-schemes + −
and the lambda-calculus, and our code+ −
will eventually become part of the next Isabelle distribution.\footnote{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 involving 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"} (see Figure~\ref{nominalcorehas}). To+ −
achieve this, we need a slightly more clever implementation than we have at the moment. + −
+ −
A more interesting line of investigation is whether we can go beyond the + −
simple-minded form of 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+ −
%+ −
\begin{center}+ −
@{text "fa_ty x = bn x \<union> fa_bn x"}.+ −
\end{center}+ −
+ −
\noindent+ −
allow us 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 + −
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 also 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.+ −
Stephanie Weirich suggested to separate the subgrammars+ −
of kinds and types in our Core-Haskell example. + −
+ −
*}+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −