# HG changeset patch # User Cezary Kaliszyk # Date 1269263255 -3600 # Node ID 69c9d53fb8173a8ad5ba7d7c809eaa87bbc8f0ac # Parent b39108f42638a3a3245784a2b7416e534a08c5c0# Parent 0368aef38e6a710c74c242ba0f3544402b669465 merge diff -r b39108f42638 -r 69c9d53fb817 Nominal/Nominal2_Atoms.thy --- a/Nominal/Nominal2_Atoms.thy Mon Mar 22 14:07:07 2010 +0100 +++ b/Nominal/Nominal2_Atoms.thy Mon Mar 22 14:07:35 2010 +0100 @@ -23,8 +23,6 @@ class at = at_base + assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" -instance at < at_base .. - lemma supp_at_base: fixes a::"'a::at_base" shows "supp a = {atom a}" @@ -146,13 +144,12 @@ subsection {* Syntax for coercing at-elements to the atom-type *} -(* syntax "_atom_constrain" :: "logic \ type \ logic" ("_:::_" [4, 0] 3) translations - "_atom_constrain a t" => "atom (_constrain a t)" -*) + "_atom_constrain a t" => "CONST atom (_constrain a t)" + subsection {* A lemma for proving instances of class @{text at}. *} diff -r b39108f42638 -r 69c9d53fb817 Paper/Paper.thy --- a/Paper/Paper.thy Mon Mar 22 14:07:07 2010 +0100 +++ b/Paper/Paper.thy Mon Mar 22 14:07:35 2010 +0100 @@ -36,12 +36,12 @@ However, Nominal Isabelle has fared less well in a formalisation of the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are of the form - - \begin{center} - \begin{tabular}{l} - $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$ - \end{tabular} - \end{center} + % + \begin{equation}\label{tysch} + \begin{array}{l} + T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T + \end{array} + \end{equation} \noindent and the quantification $\forall$ binds a finite (possibly empty) set of @@ -57,25 +57,25 @@ by iterating single binders. For example in the case of type-schemes we do not like 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{center} - $\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ - \end{center} + % + \begin{equation}\label{ex1} + \forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x + \end{equation} \noindent but the following two should \emph{not} be alpha-equivalent - - \begin{center} - $\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ - \end{center} + % + \begin{equation}\label{ex2} + \forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z + \end{equation} \noindent assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as alpha-equivalent, if they differ only on \emph{vacuous} binders, such as - - \begin{center} - $\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ - \end{center} + % + \begin{equation}\label{ex3} + \forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y + \end{equation} \noindent where $z$ does not occur freely in the type. @@ -157,9 +157,9 @@ \begin{center} \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} - $trm$ & $=$ & \ldots\\ + $trm$ & $::=$ & \ldots\\ & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm] - $assn$ & $=$ & $\mathtt{anil}$\\ + $assn$ & $::=$ & $\mathtt{anil}$\\ & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$ \end{tabular} \end{center} @@ -181,9 +181,21 @@ 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 we establish the reasoning infrastructure - for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of - its specifications a reasoning infrastructure in Isabelle/HOL for + allowed by Ott. One reason is that Ott allows ``empty'' specifications + like + + \begin{center} + $t ::= t\;t \mid \lambda x. t$ + \end{center} + + \noindent + where no clause for variables is given. Such specifications make sense in + the context of Coq's type theory (which Ott supports), but not in a HOL-based + theorem prover 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 + 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 that the @@ -247,7 +259,7 @@ 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 fact that our relation for alpha is an - equivalence relation).\marginpar{\footnotesize Does Ott allow definitions of ``strange'' types?} + equivalence relation). The fact that we obtain an isomorphism between between the new type and the non-empty subset shows that the new type is a faithful representation of alpha-equated terms. @@ -255,11 +267,11 @@ nameless representation of binders: there are non-well-formed terms that need to be excluded by reasoning about a well-formedness predicate. - The problem with introducing a new type is that in order to be useful - a resoning infrastructure needs to be ``lifted'' from the underlying type - and subset to the new type. This is usually a tricky task. To ease this task + 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 reimplemented in Isabelle/HOL the quotient package described by Homeier - \cite{Homeier05}. Gieven that alpha is an equivalence relation, this package + \cite{Homeier05}. Given that alpha is an equivalence relation, this package allows us to automatically lift definitions and theorems involving raw terms to definitions and theorems involving alpha-equated terms. This of course only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence. @@ -267,7 +279,7 @@ variables of raw terms to alpha-equated terms (since this function respects alpha-equivalence), but we will not be able to do this with a bound-variable function (since it does not respect alpha-equivalence). As a result, each - lifting needs some respectulness proofs which we automated.\medskip + lifting needs some respectfulness proofs which we automated.\medskip \noindent {\bf Contributions:} We provide new definitions for when terms @@ -287,11 +299,11 @@ Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in \cite{HuffmanUrban10}, which we review here briefly to aid the description of what follows. Two central notions in the nominal logic work are sorted - atoms and permutations of atoms. The sorted atoms 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. + atoms and sort-respecting permutations of atoms. The sorts can be used to + 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. Permutations are bijective functions from atoms to atoms that are @@ -302,19 +314,20 @@ \noindent with a generic type in which @{text "\"} stands for the type of atoms - and @{text "\"} for the type of the objects on which the permutation + 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"}, the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}} - and the inverse permutation @{term p} as @{text "- p"}. The permutation + 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}). - The most original aspect of the nominal logic work of Pitts et al is a general - definition for ``the set of free variables of an object @{text "x"}''. This - definition is general in the sense that it applies not only to lambda-terms, - 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: + 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: @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]} @@ -350,54 +363,97 @@ section {* General Binders *} text {* - In order to keep our work managable we like to state general definitions - and perform proofs inside Isabelle as much as possible, as opposed to write - custom ML-code that generates appropriate definitions and proofs for each - instance of a term-calculus. For this, we like to consider pairs + In order to keep our work manageable we give need to give definitions + and perform proofs inside Isabelle wherever possible, as opposed to write + custom ML-code that generates them for each + instance of a term-calculus. To this end we will first consider pairs \begin{equation}\label{three} - \mbox{@{text "(as, x) :: atom set \ \"}} + \mbox{@{text "(as, x) :: (atom set) \ \"}} \end{equation} \noindent - consisting of a set of atoms and an object of generic type. The pairs - are intended to be used for representing binding such as found in - type-schemes + consisting of a set of atoms and an object of generic type. These pairs + are intended to represent the abstraction or binding of the set $as$ + in the body $x$ (similarly to type-schemes given in \eqref{tysch}). - \begin{center} - $\forall \{x_1,\ldots,x_n\}. T$ - \end{center} - - \noindent - where the atoms $x_1,\ldots,x_n$ is intended to be in \eqref{three} the - set @{text as} of atoms we want to bind, and $T$, an object-level type, is - one instance for the generic $x$. - - The first question we have to answer is when we should consider the pairs - in \eqref{three} as alpha-equivelent? (At the moment we are interested in + The first question we have to answer is when we should consider pairs such as + $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in the notion of alpha-equivalence that is \emph{not} preserved by adding - vacuous binders.) Assuming we are given a free-variable function, say - \mbox{@{text "fv :: \ \ atom set"}}, then we expect for two alpha-equivelent - pairs that their sets of free variables aggree. That is + vacuous binders.) To answer this we identify four conditions: {\it i)} given + a free-variable function of type \mbox{@{text "fv :: \ \ atom set"}}, then $x$ and $y$ + need to have the same set of free variables; moreover there must be a permutation, + $p$ that {\it ii)} leaves the free variables $x$ and $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 $p$ makes + the abstracted sets $as$ and $bs$ equal (since at the moment we do not want + that the sets $as$ and $bs$ differ on vacuous binders). These requirements can + be stated formally as follows % - \begin{equation}\label{four} - \mbox{@{text "(as, x) \ (bs, y)"} \hspace{2mm}implies\hspace{2mm} @{text "fv(x) - as = fv(y) - bs"}} + \begin{equation}\label{alphaset} + \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} + \multicolumn{2}{l}{(as, x) \approx_{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 "(p \ x) R y"}\\ + \wedge & @{text "(p \ as) = bs"}\\ + \end{array} \end{equation} \noindent - Next we expect that there is a permutation, say $p$, that leaves the - free variables unchanged, but ``moves'' the bound names in $x$ so that - we obtain $y$ modulo a relation, say @{text "_ R _"}, that characterises when two - elments of type $\beta$ are equivalent. We also expect that $p$ - makes the binders equal. We can formulate these requirements as: there - exists a $p$ such that $i)$ @{term "(fv(x) - as) \* p"}, $ii)$ @{text "(p \ x) R y"} and - $iii)$ @{text "(p \ as) = bs"}. + Alpha equivalence between such pairs is then the relation with the additional + existential quantification over $p$. Note that this relation is additionally + dependent on the free-variable function $\fv$ and the relation $R$. The reason + for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms + and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and + we are going to prove that $\fv$ will be equal to the support of $x$ and $y$. + + The definition in \eqref{alphaset} does not make any distinction between the + order of abstracted variables. If we do want this then we can define alpha-equivalence + for pairs of the form \mbox{@{text "(as, x) :: (atom list) \ \"}} by + % + \begin{equation}\label{alphalist} + \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} + \multicolumn{2}{l}{(as, x) \approx_{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 "(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. - We take now \eqref{four} and the three - + If we do not want to make any difference between the order of binders and + allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset} + and define + % + \begin{equation}\label{alphaset} + \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} + \multicolumn{2}{l}{(as, x) \approx_{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 "(p \ x) R y"}\\ + \end{array} + \end{equation} - General notion of alpha-equivalence (depends on a free-variable - function and a relation). + To get a feeling how these definitions pan out in practise consider the case of + abstracting names over types (like in type-schemes). For this we set $R$ to be + the equality and for $\fv(T)$ we define + + \begin{center} + $\fv(x) = \{x\} \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$ + \end{center} + + \noindent + Now reacall the examples 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_{ref}$ by taking $p$ to + be the swapping @{text "(x \ y)"}; but assuming @{text "x \ y"} then for instance + $([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, but leaves the type \mbox{@{text "x \ y"}} + unchanged. *} section {* Alpha-Equivalence and Free Variables *} @@ -406,7 +462,7 @@ Restrictions \begin{itemize} - \item non-emptyness + \item non-emptiness \item positive datatype definitions \item finitely supported abstractions \item respectfulness of the bn-functions\bigskip @@ -420,6 +476,14 @@ section {* Related Work *} +text {* + Ott is better with list dot specifications; subgrammars + + untyped; + +*} + + section {* Conclusion *} text {* diff -r b39108f42638 -r 69c9d53fb817 Paper/document/root.tex --- a/Paper/document/root.tex Mon Mar 22 14:07:07 2010 +0100 +++ b/Paper/document/root.tex Mon Mar 22 14:07:35 2010 +0100 @@ -23,7 +23,7 @@ \newcommand{\IN}{\;\mathtt{in}\;} \newcommand{\END}{\;\mathtt{end}\;} \newcommand{\AND}{\;\mathtt{and}\;} - +\newcommand{\fv}{\mathit{fv}} %----------------- theorem definitions ----------