--- a/Paper/Paper.thy Thu Jul 01 14:18:36 2010 +0100
+++ b/Paper/Paper.thy Fri Jul 02 01:54:19 2010 +0100
@@ -946,13 +946,14 @@
%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 binding clauses: the
+ There are also some restrictions we need to impose on binding clauses. 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 a
- variable occurence cannot be bound and free at the same time. First, a body can only occur in
+ variable occurence 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
variables of a body cannot be free at the same time by specifying an
- alternative binder for the body). For binders we distinguish between
+ 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
@@ -1040,7 +1041,7 @@
\end{center}
\noindent
- where the argument of the deep binder is also in the body. We call such
+ 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:
@@ -1070,8 +1071,8 @@
function and $\alpha$-equivalence relation, which we are going to define later.
To make sure that variables bound by deep binders cannot be free at the
- same time, we have to impose some further restrictions. First,
- we cannot have more than one binding function for one binder. So we exclude:
+ same time, we cannot have more than one binding function for one binder.
+ Consequently we exclude specifications such as
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@@ -1084,12 +1085,12 @@
\end{center}
\noindent
- Otherwise it is be possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
- out different atoms to become bound in @{text "p"}.
+ 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"}.
-
- We also need to restrict the form of the binding functions. As will shortly
- become clear, we cannot return an atom in a binding function that is also
+ We also need to restrict the form of the binding functions in order
+ to ensure the @{text "bn"}-functions can be lifted defined for $\alpha$-equated
+ terms. As a result we cannot return an atom in a binding function that is also
bound in the corresponding term-constructor. That means in the example
\eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
not have a binding clause (all arguments are used to define @{text "bn"}).
@@ -1168,22 +1169,18 @@
non-empty and the types in the constructors only occur in positive
position (see \cite{Berghofer99} for an indepth description of the datatype package
in Isabelle/HOL). We then define the user-specified binding
- functions, called @{term "bn"}, by recursion over the corresponding
+ functions @{term "bn"} by recursion over the corresponding
raw datatype. We can also easily define permutation operations by
- recursion so that for each term constructor @{text "C"} with the
- argument types @{text "ty"}$_{1..n}$ we have that
+ recursion so that for each term constructor @{text "C"} with
+ arguments @{text "z"}$_{1..n}$ we have that
%
\begin{equation}\label{ceqvt}
@{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
\end{equation}
- \noindent
- where the variables @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$.
-
The first non-trivial step we have to perform is the generation of
- free-variable functions from the specifications. Given a raw term, these
- functions return sets of atoms. Assuming a nominal datatype
- specification as in \eqref{scheme} and its \emph{raw} types @{text "ty"}$_{1..n}$,
+ free-variable functions from the specifications. For the
+ \emph{raw} types @{text "ty"}$_{1..n}$ of a specification,
we define the free-variable functions
%
\begin{equation}\label{fvars}
@@ -1206,120 +1203,113 @@
While the idea behind these free-variable functions is clear (they just
collect all atoms that are not bound), because of our rather complicated
- binding mechanisms their definitions are somewhat involved. Given a
- term-constructor @{text "C"} of type @{text ty} and some associated binding
- clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
- the union @{text "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} of free variables calculated for
- each binding clause. Given a binding clause @{text bc} is of the form
+ binding mechanisms their definitions are somewhat involved. The functions
+ are defined by recursion defining a clause for each term-constructor. Given
+ the 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
+ "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
+ "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"}. Given the binding clause @{text
+ bc\<^isub>i} is of the form
%
\begin{equation}
- \mbox{\isacommand{bind} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+ \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
- where the body labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$; the binders
- @{text b}$_{1..p}$
+ 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 the
- free variables of the bodies is the set @{text "D"}, the bound variables of the binders
- is the set @{text B} and the free variables of the non-recursive deep binders is @{text "B'"}
- then the free variables of the binding clause @{text bc} is
+ set @{text "D"} stands for the free atoms in the bodies, @{text B} for the
+ binding atoms in the binders and @{text "B'"} for the free atoms in
+ non-recursive deep binders,
+ then the free atoms of the binding clause @{text bc\<^isub>i} are given by
%
\begin{center}
- @{text "fv(bc) = (D - B) \<union> B'"}
+ @{text "fv(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
\end{center}
\noindent
- Formally the set @{text D} is the union of the free variables for the bodies
+ The set @{text D} is defined as
%
\begin{center}
- @{text "D = fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
+ @{text "D \<equiv> fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
\end{center}
\noindent
- whereby the free variable functions @{text "fv_ty\<^isub>i"} are the ones in \eqref{fvars}
- provided the @{text "d\<^isub>i"} refers to one of the types @{text "ty"}$_{1..n}$;
- otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
-
-
-if @{text "d\<^isub>i"} is a label
- for an atomic type we use the following auxiliary free variable functions
-
+ whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion
+ (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the types
+ @{text "ty"}$_{1..n}$; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+ In order to define the set @{text B} we use the following auxiliary bn-functions
+ for atom types to which shallow binders have to refer
+ %
\begin{center}
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{text "fv_atom a"} & @{text "="} & @{text "{atom a}"}\\
- @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\
- @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
+ @{text "bn_atom a"} & @{text "="} & @{text "{atom a}"}\\
+ @{text "bn_atom_set as"} & @{text "="} & @{text "atoms as"}\\
+ @{text "bn_atom_list as"} & @{text "="} & @{text "atoms (set as)"}
\end{tabular}
\end{center}
\noindent
In these functions, @{text "atoms"}, like @{text "atom"}, coerces
- the set of atoms to a set of the generic atom type.
- It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}. Otherwise
-
+ the set of atoms to a set of the generic atom type. It is defined as
+ @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
+ The set @{text B} is then 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}
-
-the values, @{text v}, calculated by the rules for each bining clause:
+ \noindent
+ The set @{text "B'"} collects all free atoms in non-recursive deep
+ binders. Lets assume these binders in @{text "bc\<^isub>i"} are
%
- \begin{equation}\label{deepbinderA}
- \mbox{%
- \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
- \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
- $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
- %
- \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\
- & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\
- & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the
- binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\
- \end{tabular}}
- \end{equation}
- \begin{equation}\label{deepbinderB}
- \mbox{%
- \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
- \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x) \<union> (fv_bn x)"}\\
- $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\
- & provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first
- clause applies for @{text x} being a non-recursive deep binder (that is
- @{text "x \<noteq> y"}$_{1..m}$), the second for a recursive deep binder
- \end{tabular}}
- \end{equation}
+ \begin{center}
+ @{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
+ \end{center}
+
+ \noindent
+ with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
+ "d"}$_{1..q}$. The set @{text "B'"} is then defined as
+ %
+ \begin{center}
+ @{text "B' \<equiv> fv_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fv_bn\<^isub>r a\<^isub>r"}
+ \end{center}
\noindent
- Similarly for the other binding modes. Note that in a non-recursive deep
- binder, we have to add all atoms that are left unbound by the binding
- function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume
- for the constructor @{text "C"} the binding function is of the form @{text
- "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}. We again define a value
- @{text v} which is exactly as in \eqref{deepbinderA}/\eqref{deepbinderB} for shallow and deep
- binding clauses, except for empty binding clauses are defined as follows:
+ Similarly for the other binding modes.
+
+ Note that for non-recursive deep binders, we have to add all atoms that are left
+ unbound by the binding function @{text "bn"}. This is the purpose of the functions
+ @{text "fv_bn"}, also defined by recursion. Assume the user has specified
+ a @{text bn}-clause of the form
%
- \begin{equation}\label{bnemptybinder}
- \mbox{%
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
- $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"}
- and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\
- $\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in @{text "rhs"}
- with a recursive call @{text "bn y"}\\
- $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"},
- but without a recursive call\\
- \end{tabular}}
- \end{equation}
+ \begin{center}
+ @{text "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}
+ \end{center}
\noindent
- The reason why we only have to treat the empty binding clauses specially in
- the definition of @{text "fv_bn"} is that binding functions can only use arguments
- that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot
- be lifted to $\alpha$-equated terms.
+ where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
+ the arguments we calculate the free atoms as follows
+ %
+ \begin{center}
+ \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\
+ $\bullet$ & @{term "fv_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"}\\
+ $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"},
+ but without a recursive call
+ \end{tabular}
+ \end{center}
-
+ \noindent
+ For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"}, we just union up all these values.
+
To see how these definitions work in practice, let us reconsider the term-constructors
@{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}.
- For this specification we need to define three free-variable functions, namely
- @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:
+ For them we consider three free-variable functions, namely
+ @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}:
%
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -1363,6 +1353,8 @@
\noindent
holds for any @{text "bn"}-function defined for the type @{text "ty"}.
+ TBD below.
+
Next we define $\alpha$-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions,
we also need to define auxiliary $\alpha$-equivalence relations for the binding functions.
@@ -1382,7 +1374,8 @@
conclusions of the form
%
\begin{center}
- @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
+ \mbox{\infer{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}}
+ {@{text "prems(bc\<^isub>1)"} & @{text "\<dots>"} & @{text "prems(bc\<^isub>p)"}}}
\end{center}
\noindent
@@ -2060,24 +2053,6 @@
\end{tabular}
\end{center}
- To see this, consider the following equations
-
- \begin{center}
- \begin{tabular}{c}
- @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (b, a)"}\\
- @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (a, b)"}\\
- \end{tabular}
- \end{center}
-
- \noindent
- The interesting point is that they do not imply
-
- \begin{center}
- \begin{tabular}{c}
- @{term "Abs_print [a,b] ((a, b), (a, b)) = Abs_print [a,b] ((a, b), (b, a))"}\\
- \end{tabular}
- \end{center}
-
Because of how we set up our definitions, we had to impose 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
--- a/Paper/document/root.bib Thu Jul 01 14:18:36 2010 +0100
+++ b/Paper/document/root.bib Fri Jul 02 01:54:19 2010 +0100
@@ -67,7 +67,7 @@
@InProceedings{CoreHaskell,
author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly},
title = {{S}ystem {F} with {T}ype {E}quality {C}oercions},
- booktitle = {Proc of the TLDI Workshop},
+ booktitle = {Proc.~of the TLDI Workshop},
pages = {53-66},
year = {2007}
}
@@ -173,7 +173,7 @@
@article{MckinnaPollack99,
author = {J.~McKinna and R.~Pollack},
title = {{S}ome {T}ype {T}heory and {L}ambda {C}alculus {F}ormalised},
- journal = {Journal of Automated Reasoning},
+ journal = {J.~of Automated Reasoning},
volume = 23,
number = {1-4},
year = 1999