# HG changeset patch # User Christian Urban # Date 1269255329 -3600 # Node ID 0368aef38e6a710c74c242ba0f3544402b669465 # Parent 1d70813ae6749b469b71aa78ca24b9abf592c1b3 more on the paper diff -r 1d70813ae674 -r 0368aef38e6a Paper/Paper.thy --- a/Paper/Paper.thy Mon Mar 22 10:21:14 2010 +0100 +++ b/Paper/Paper.thy Mon Mar 22 11:55:29 2010 +0100 @@ -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. @@ -268,7 +268,7 @@ 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 resoning infrastructure needs to be ``lifted'' from the underlying subset to + 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}. Given that alpha is an equivalence relation, this package @@ -279,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 @@ -363,8 +363,8 @@ section {* General Binders *} text {* - In order to keep our work managable we give need to give definitions - and perform proofs inside Isabelle whereever possible, as opposed to write + 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 @@ -378,45 +378,82 @@ in the body $x$ (similarly to type-schemes given in \eqref{tysch}). The first question we have to answer is when we should consider pairs such as - $(as, x)$ and $(bs, y)$ as alpha-equivelent? (At the moment we are interested in + $(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.) For this we identify four conditions: 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; ii) there must be a permutation, - say $p$, that leaves the free variables $x$ and $y$ unchanged, but ``moves'' their bound names - so that we obtain modulo a relation, say @{text "_ R _"}, - two equal terms. We also require that $p$ makes the abstracted sets equal. These - requirements can be stated formally as - - \begin{center} - \begin{tabular}{rcl} - a - \end{tabular} - \end{center} - - - 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 *} @@ -425,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 diff -r 1d70813ae674 -r 0368aef38e6a Paper/document/root.tex --- a/Paper/document/root.tex Mon Mar 22 10:21:14 2010 +0100 +++ b/Paper/document/root.tex Mon Mar 22 11:55:29 2010 +0100 @@ -23,7 +23,7 @@ \newcommand{\IN}{\;\mathtt{in}\;} \newcommand{\END}{\;\mathtt{end}\;} \newcommand{\AND}{\;\mathtt{and}\;} - +\newcommand{\fv}{\mathit{fv}} %----------------- theorem definitions ----------