# HG changeset patch # User Christian Urban # Date 1269361339 -3600 # Node ID 99cee15cb5ffccf4497511d95dc90d08d05f4f61 # Parent b7e19f16bcd04fa7b6771630f606868e387340c7 more tuning in the paper diff -r b7e19f16bcd0 -r 99cee15cb5ff Paper/Paper.thy --- a/Paper/Paper.thy Tue Mar 23 13:07:11 2010 +0100 +++ b/Paper/Paper.thy Tue Mar 23 17:22:19 2010 +0100 @@ -130,7 +130,8 @@ programming language calculus. By providing these general binding mechanisms, however, we have to work around - a problem that has been pointed out by Pottier in \cite{Pottier06}: in + a problem that has been pointed out by Pottier in \cite{Pottier06} and Cheney in + \cite{Cheney05}: in $\mathtt{let}$-constructs of the form % \begin{center} @@ -150,7 +151,7 @@ \noindent where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$} - would be a perfectly legal instance. To exclude such terms an additional + would be a perfectly legal instance. To exclude such terms, an additional predicate about well-formed terms is needed in order to ensure that the two lists are of equal length. This can result into very messy reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications @@ -182,17 +183,18 @@ heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. However, we will not be able to deal with all specifications that are - allowed by Ott. One reason is that Ott allows ``empty'' specifications - like + allowed by Ott. One reason is that Ott lets the user to specify ``empty'' + types like \begin{center} $t ::= t\;t \mid \lambda x. t$ \end{center} \noindent - where no clause for variables is given. 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. + 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. Another reason is that we establish the reasoning infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a reasoning @@ -200,14 +202,14 @@ \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 that the - two type-schemes with $x$, $y$ and $z$ being distinct + two type-schemes (with $x$, $y$ and $z$ being distinct) \begin{center} $\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$ \end{center} \noindent - are not just alpha-equal, but actually equal. As a + 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 @@ -264,7 +266,7 @@ 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 in the representation of terms using the locally + 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. @@ -273,10 +275,10 @@ 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}. This package + \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 lambda terms + to definitions and theorems involving alpha-equated terms. For example + if we define the free-variable function over raw lambda-terms \begin{center} $\fv(x) = \{x\}$\hspace{10mm} @@ -286,7 +288,8 @@ \noindent then with not too great effort we obtain a function $\fv_\alpha$ - operating on quotients, or alpha-equivalence classes of terms, as follows + operating on quotients, or alpha-equivalence classes of lambda-terms. This + function is characterised by the equations \begin{center} $\fv_\alpha(x) = \{x\}$\hspace{10mm} @@ -297,8 +300,8 @@ \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 an equivalence relation, and the - definitions and theorems are respectful w.r.t.~alpha-equivalence. Hence we + only works if alpha-equivalence is an equivalence relation, and the lifted + definitions and theorems are respectful w.r.t.~alpha-equivalence. Accordingly, we will not be able to lift a bound-variable function to alpha-equated terms (since it does not respect alpha-equivalence). To sum up, every lifting of theorems to the quotient level needs proofs of some respectfulness @@ -329,23 +332,27 @@ represent different kinds of variables, such as term- and type-variables in Core-Haskell, and it is assumed that there is an infinite supply of atoms for each sort. However, in order to simplify the description, we shall - assume in what follows that there is only a single sort of atoms. - + assume in what follows that there is 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 - - @{text[display,indent=5] "_ \ _ :: (\ \ \) list \ \ \ \"} + % + @{text[display,indent=5] "_ \ _ :: perm \ \ \ \"} \noindent - with a generic type in which @{text "\"} stands for the type of atoms - and @{text "\"} for the type of the object on which the permutation - acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"}, + with a generic type in which @{text "\"} stands for the type of the object + on 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 for products, lists, sets, functions, booleans etc - (see \cite{HuffmanUrban10}). + (see \cite{HuffmanUrban10}). In the nominal logic work, concrete + permutations are usually build up from swappings, written as @{text "(a b)"}, + which are permutations that behave as follows: + % + @{text[display,indent=5] "(a b) = \c. if a = c then b else if b = c then a else c"} + 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 @@ -354,13 +361,13 @@ 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: - + % @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]} \noindent There is also the derived notion for when an atom @{text a} is \emph{fresh} for an @{text x}, defined as - + % @{thm[display,indent=5] fresh_def[no_vars]} \noindent @@ -391,34 +398,34 @@ 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 specifcation (remember that Nominal Isabelle is a definitional + 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 manageable, we will wherever possible state definitions and perform proofs inside Isabelle, as opposed to write custom - ML-code that generates them for each instance of a term-calculus. To that + ML-code that generates them anew for each specification. To that end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. - These pairs are intended to represent the abstraction, or binding, of the set $as$ - in the body $x$. + These pairs are intended to represent the abstraction, or binding, of the set @{text "as"} + in the body @{text "x"}. The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are alpha-equivalent? (At the moment we are interested in the notion of alpha-equivalence that is \emph{not} preserved by adding vacuous binders.) To answer this, we identify four conditions: {\it i)} given - a free-variable function $\fv$ of type \mbox{@{text "\ \ atom set"}}, then $x$ and $y$ - need to have the same set of free variables; moreover there must be a permutation, - $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged, - but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation, - say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes - the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can + a free-variable function $\fv$ of type \mbox{@{text "\ \ atom set"}}, then @{text x} and @{text y} + need to have the same set of free variables; moreover there must be a permutation + @{text p} such that {\it ii)} it leaves the free variables of @{text x} and @{text y} unchanged, + but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, + say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that @{text p} makes + the abstracted sets @{text as} and @{text bs} equal. The requirements {\it i)} to {\it iv)} can be stated formally as follows: % \begin{equation}\label{alphaset} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] & @{text "fv(x) - as = fv(y) - bs"}\\ - \wedge & @{text "fv(x) - as #* p"}\\ + \wedge & @{text "(fv(x) - as) #* p"}\\ \wedge & @{text "(p \ x) R y"}\\ \wedge & @{text "(p \ as) = bs"}\\ \end{array} @@ -431,8 +438,7 @@ $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support - of $x$ and $y$. To have these parameters means, however, we can derive properties about - them generically. + of $x$ and $y$. The definition in \eqref{alphaset} does not make any distinction between the order of abstracted variables. If we want this, then we can define alpha-equivalence @@ -443,14 +449,14 @@ \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\ - \wedge & @{text "fv(x) - (set as) #* p"}\\ + \wedge & @{text "(fv(x) - set as) #* p"}\\ \wedge & @{text "(p \ x) R y"}\\ \wedge & @{text "(p \ as) = bs"}\\ \end{array} \end{equation} \noindent - where $set$ is just the function that coerces a list of atoms into a set of atoms. + where $set$ is the function that coerces a list of atoms into a set of atoms. If we do not want to make any difference between the order of binders and also allow vacuous binders, then we keep sets of binders, but drop the fourth @@ -460,7 +466,7 @@ \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] & @{text "fv(x) - as = fv(y) - bs"}\\ - \wedge & @{text "fv(x) - as #* p"}\\ + \wedge & @{text "(fv(x) - as) #* p"}\\ \wedge & @{text "(p \ x) R y"}\\ \end{array} \end{equation} @@ -478,12 +484,13 @@ Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \ y)"} and @{text "({y, x}, y \ x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to - be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"} then + be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that - makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the - type \mbox{@{text "x \ y"}} unchanged. Again if @{text "x \ y"}, we have that - $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation. - However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes + makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also leaves the + type \mbox{@{text "x \ y"}} unchanged. Another examples is + $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ which holds by taking $p$ to be the identity permutation. + However, if @{text "x \ y"}, then + $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$). \end{exmple} @@ -522,17 +529,17 @@ section {* Alpha-Equivalence and Free Variables *} text {* - The syntax of a specification for a term-calculus in Nominal Isabelle is - heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a - collection of (possibly mutual recursive) type declarations, say - $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a - collection of associated binding function declarations, say - $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically - written as follows: + Our specifications for term-calculi are heavily + inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is + a collection of (possibly mutual recursive) type declarations, say + $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and an + associated collection of binding function declarations, say + $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically written as + follows: \begin{center} \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l} - types \mbox{declaration part} & + type \mbox{declaration part} & $\begin{cases} \mbox{\begin{tabular}{l} \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\ @@ -541,7 +548,7 @@ \isacommand{and} $ty_{\alpha{}n} = \ldots$\\ \end{tabular}} \end{cases}$\\ - binding \mbox{functions part} & + binding \mbox{function part} & $\begin{cases} \mbox{\begin{tabular}{l} \isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$ @@ -554,31 +561,36 @@ \end{center} \noindent - Each type declaration $ty_{\alpha{}i}$ consists of a collection of + Every type declaration $ty_{\alpha{}i}$ consists of a collection of term-constructors, each of which comes with a list of labelled - types that indicate the types of the arguments of the term-constructor, - like + types that indicate the types of the arguments of the term-constructor. + For example for a term-constructor $C_{\alpha}$ we might have \begin{center} $C_\alpha\;label_1\!::\!ty'_1\;\ldots label_j\!::\!ty'_j\;\;\textit{binding\_clauses}$ \end{center} \noindent - The labels are optional and can be used in the (possibly empty) list of binding clauses. - These clauses indicate the binders and the scope of the binders in a term-constructor. They - are of the form + The labels are optional and can be used in the (possibly empty) list of \emph{binding clauses}. + These clauses indicate the binders and the scope of the binders in a term-constructor. + They come in three forms \begin{center} - \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label} + \begin{tabular}{l} + \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\ + \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\ + \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\ + \end{tabular} \end{center} \noindent - whereby we distinguish between \emph{shallow} binders and \emph{deep} binders. - Shallow binders are just of the form \isacommand{bind}\; {\it label}\; - \isacommand{in}\; {\it another\_label}. The only restriction on shallow binders - is that the {\it label} must refer to either a type which is single atom or - to a type which is a finite set of atoms. For example the specification of - lambda-terms and type-schemes use them: + whereby we also distinguish between \emph{shallow} binders and \emph{deep} binders. + Shallow binders are of the form \isacommand{bind}\; {\it label}\; + \isacommand{in}\; {\it another\_label} (similar the other forms). The restriction + we impose on shallow binders + is that the {\it label} must either refer to a type that is an atom type or + to a type that is a finite set or list of an atom type. For example the specifications of + lambda-terms and type-schemes use shallow binders (where \emph{name} is an atom type): \begin{center} \begin{tabular}{@ {}cc@ {}} @@ -587,20 +599,36 @@ \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\ \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\ \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\ - \hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\ + \hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\ \end{tabular} & \begin{tabular}{@ {}l@ {}} \isacommand{nominal\_datatype} {\it ty} =\\ \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\ \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\ - \isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\ - \hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\ + \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\ + \hspace{22mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\ \end{tabular} \end{tabular} \end{center} \noindent - A specification of a term-calculus in Nominal Isabell is very similar to + A \emph{deep} binder uses an auxiliary binding function that picks out the atoms + that are bound in one or more arguments. This binding function returns either + a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a + list of atoms (for \isacommand{bind}). Such binding functions can be defined + by primitive recursion over the corresponding type. They are defined by equations + included in the binding function part of the scheme given above. + + For the moment we + adopt the restriction of the Ott-tool that binding functions can only return + the empty set, a singleton set of atoms or unions of atom sets. For example + + over the type for which they specify the bound atoms. + + + + \noindent + A specification of a term-calculus in Nominal Isabelle is very similar to the usual datatype definition of Isabelle/HOL: diff -r b7e19f16bcd0 -r 99cee15cb5ff Paper/document/root.bib --- a/Paper/document/root.bib Tue Mar 23 13:07:11 2010 +0100 +++ b/Paper/document/root.bib Tue Mar 23 17:22:19 2010 +0100 @@ -1,3 +1,11 @@ + +@inproceedings{cheney05, + author = {J.~Cheney}, + title = {{T}oward a {G}eneral {T}heory of {N}ames: {B}inding and {S}cope}, + booktitle = {Proc.~of the 3rd MERLIN workshop}, + year = {2005}, + pages = {33-40} +} @Unpublished{Pitts04, author = {Andrew Pitts}, diff -r b7e19f16bcd0 -r 99cee15cb5ff Paper/document/root.tex --- a/Paper/document/root.tex Tue Mar 23 13:07:11 2010 +0100 +++ b/Paper/document/root.tex Tue Mar 23 17:22:19 2010 +0100 @@ -12,6 +12,8 @@ \urlstyle{rm} \isabellestyle{it} +\renewcommand{\isastyleminor}{\it}% +\renewcommand{\isastyle}{\normalsize\it}% \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}} \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}