# HG changeset patch # User Christian Urban # Date 1277990316 -3600 # Node ID 36aeb97fabb0cbfe6fcd77cc241499f793bf6ff0 # Parent f296ef291ca9a974f5e646d89a8abbd4194253dd more on the paper diff -r f296ef291ca9 -r 36aeb97fabb0 Paper/Paper.thy --- a/Paper/Paper.thy Thu Jul 01 01:53:00 2010 +0100 +++ b/Paper/Paper.thy Thu Jul 01 14:18:36 2010 +0100 @@ -46,7 +46,7 @@ %%% @{text "(1, (2, 3))"} So far, Nominal Isabelle provides a mechanism for constructing - $\alpha$-equated terms, for example + $\alpha$-equated terms, for example lambda-terms \begin{center} @{text "t ::= x | t t | \x. t"} @@ -365,9 +365,9 @@ 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 concepts behind our specifications of general binders are taken + The method behind our specification of general binders is taken from the Ott-tool, but we introduce restrictions, and also one extension, so - that the specifications make sense for reasoning about $\alpha$-equated terms. + that our specifications make sense for reasoning about $\alpha$-equated terms. \begin{figure} @@ -567,9 +567,9 @@ @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \ x) R (p \ y)"} \end{center} - Finally, the nominal logic work provides us with general means to rename + 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} for renaming single binders, this property + 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. @@ -628,7 +628,7 @@ {\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: + 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} @@ -739,7 +739,7 @@ \end{proof} \noindent - This lemma allows us to use our quotient package and introduce + This lemma allows us to use our quotient package for introducing new types @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} representing $\alpha$-equivalence classes of pairs of type @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} @@ -913,9 +913,9 @@ \begin{center} \begin{tabular}{l} - \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ - \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ - \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ + \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} @@ -923,8 +923,8 @@ The first mode is for binding lists of atoms (the order of binders matters); the second is for sets of binders (the order does not matter, but the cardinality does) and the last is for sets of binders (with vacuous binders - preserving $\alpha$-equivalence). The ``\isacommand{in}-part'' of a binding - clause will be called \emph{bodies} (there can be more than one); the + preserving $\alpha$-equivalence). As indicated, 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: @@ -940,25 +940,28 @@ \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. + 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 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 a bound variable cannot be free at the same time. First, 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 \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: + 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 + \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 + \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@ {}} @@ -994,11 +997,10 @@ \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 primitive recursion over the corresponding type; the equations + 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{% @@ -1042,7 +1044,7 @@ 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@ {}} @@ -1065,10 +1067,10 @@ The difference is that with @{text Let} we only want to bind the atoms @{text "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms inside the assignment. This difference has consequences for the free-variable - function and $\alpha$-equivalence relation, which we are going to define below. + 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 restrictions. First, + same time, we have to impose some further restrictions. First, we cannot have more than one binding function for one binder. So we exclude: \begin{center} @@ -1082,6 +1084,10 @@ \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"}. + + We also need to restrict the form of the binding functions. As will shortly become clear, we cannot return an atom in a binding function that is also bound in the corresponding term-constructor. That means in the example @@ -1089,7 +1095,8 @@ 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). + is \emph{not} used in the definition of the binding function). This restriction + means that we can lift the binding function to $\alpha$-equated terms. In the version of Nominal Isabelle described here, we also adopted the restriction from the @@ -1099,7 +1106,8 @@ (case @{text PTup}). This restriction will simplify some automatic definitions and proofs later on. - In order to simplify our definitions, we shall assume specifications + In order to simplify our definitions of free variables 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 @@ -1132,9 +1140,11 @@ Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just re-arranging the arguments of term-constructors so that binders and their bodies are next to each other will - result in inadequate representations. Therefore we will first + result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\x\<^isub>n=t\<^isub>n in s"}. + Therefore we will first extract datatype definitions from the specification and then define - explicitly an $\alpha$-equivalence relation over them. + explicitly an $\alpha$-equivalence relation over them. We subsequently + quotient the datatypes according to our $\alpha$-equivalence. The datatype definition can be obtained by stripping off the @@ -1158,28 +1168,33 @@ non-empty and the types in the constructors only occur in positive position (see \cite{Berghofer99} for an indepth description of the datatype package in Isabelle/HOL). We then define the user-specified binding - functions, called @{term "bn"}, by primitive recursion over the corresponding + functions, called @{term "bn"}, by recursion over the corresponding raw datatype. We can also easily define permutation operations by - primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \ ty\<^isub>n"} - we have that + recursion so that for each term constructor @{text "C"} with the + argument types @{text "ty"}$_{1..n}$ we have that % \begin{equation}\label{ceqvt} @{text "p \ (C z\<^isub>1 \ z\<^isub>n) = C (p \ z\<^isub>1) \ (p \ 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 the raw types @{text - "ty\<^isub>1 \ ty\<^isub>n"} derived from a specification, we define the - free-variable functions - - \begin{center} + 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}$, + we define the free-variable functions + % + \begin{equation}\label{fvars} @{text "fv_ty\<^isub>1, \, fv_ty\<^isub>n"} - \end{center} + \end{equation} \noindent We define them together with auxiliary free-variable functions for - the binding functions. Given raw binding functions @{text "bn\<^isub>1 \ bn\<^isub>m"} we define - + the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ + we define + % \begin{center} @{text "fv_bn\<^isub>1, \, fv_bn\<^isub>m"} \end{center} @@ -1187,32 +1202,65 @@ \noindent The reason for this setup is that in a deep binder not all atoms have to be bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function - that calculates those unbound atoms. + that calculates those unbound atoms in a deep binder. + + 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\bc\<^isub>k"}, the result of the @{text "fv_ty (C z\<^isub>1 \ z\<^isub>n)"} will be + the union @{text "fv(bc\<^isub>1) \ \ \ fv(bc\<^isub>k)"} of free variables calculated for + each binding clause. Given a binding clause @{text bc} is of the form + % + \begin{equation} + \mbox{\isacommand{bind} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} + \end{equation} - For atomic types we define the auxiliary - free variable functions: + \noindent + where the body labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$; 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 + % + \begin{center} + @{text "fv(bc) = (D - B) \ B'"} + \end{center} + + \noindent + Formally the set @{text D} is the union of the free variables for the bodies + % + \begin{center} + @{text "D = fv_ty\<^isub>1 d\<^isub>1 \ ... \ 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 \begin{center} \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\ + @{text "fv_atom a"} & @{text "="} & @{text "{atom a}"}\\ @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\ @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\ \end{tabular} \end{center} \noindent - Like the coercion function @{text atom}, @{text "atoms"} coerces + 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 \ {atom a | a \ as}"}. + It is defined as @{text "atoms as \ {atom a | a \ as}"}. Otherwise + - While the idea behind these free-variable functions is clear (they just - collect all atoms that are not bound), because of our rather complicated - binding mechanisms their definitions are somewhat involved. Given a - term-constructor @{text "C"} of type @{text ty} and some associated binding - clauses @{text bcs}, the result of the @{text "fv_ty (C z\<^isub>1 \ z\<^isub>n)"} will be - the union of the values, @{text v}, calculated by the rules for empty, shallow and - deep binding clauses: +the values, @{text v}, calculated by the rules for each bining clause: % \begin{equation}\label{deepbinderA} \mbox{% @@ -1965,7 +2013,7 @@ 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, + 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 @@ -2043,7 +2091,7 @@ representing terms with general binders inside OCaml. This language is implemented as a front-end that can be translated to OCaml with a help of a library. He presents a type-system in which the scope of general binders - can be indicated with some special constructs, written @{text "inner"} and + can be indicated with some special markers, written @{text "inner"} and @{text "outer"}. With this, it seems, our and his specifications can be inter-translated, but we have not proved this. However, we believe the binding specifications in the style of Ott are a more natural way for