Paper/Paper.thy
changeset 1572 0368aef38e6a
parent 1570 014ddf0d7271
child 1577 8466fe2216da
equal deleted inserted replaced
1571:1d70813ae674 1572:0368aef38e6a
    55 
    55 
    56   Binding multiple variables has interesting properties that are not captured
    56   Binding multiple variables has interesting properties that are not captured
    57   by iterating single binders. For example in the case of type-schemes we do not
    57   by iterating single binders. For example in the case of type-schemes we do not
    58   like to make a distinction about the order of the bound variables. Therefore
    58   like to make a distinction about the order of the bound variables. Therefore
    59   we would like to regard the following two type-schemes as alpha-equivalent
    59   we would like to regard the following two type-schemes as alpha-equivalent
    60 
    60   %
    61   \begin{center}
    61   \begin{equation}\label{ex1}
    62   $\forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ 
    62   \forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x 
    63   \end{center}
    63   \end{equation}
    64 
    64 
    65   \noindent
    65   \noindent
    66   but  the following two should \emph{not} be alpha-equivalent
    66   but  the following two should \emph{not} be alpha-equivalent
    67 
    67   %
    68   \begin{center}
    68   \begin{equation}\label{ex2}
    69   $\forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ 
    69   \forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z 
    70   \end{center}
    70   \end{equation}
    71 
    71 
    72   \noindent
    72   \noindent
    73   assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as 
    73   assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as 
    74   alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
    74   alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
    75 
    75   %
    76   \begin{center}
    76   \begin{equation}\label{ex3}
    77   $\forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ 
    77   \forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y
    78   \end{center}
    78   \end{equation}
    79 
    79 
    80   \noindent
    80   \noindent
    81   where $z$ does not occur freely in the type.
    81   where $z$ does not occur freely in the type.
    82   In this paper we will give a general binding mechanism and associated
    82   In this paper we will give a general binding mechanism and associated
    83   notion of alpha-equivalence that can be used to faithfully represent
    83   notion of alpha-equivalence that can be used to faithfully represent
   266   That is different for example in the representation of terms using the locally 
   266   That is different for example in the representation of terms using the locally 
   267   nameless representation of binders: there are non-well-formed terms that need to
   267   nameless representation of binders: there are non-well-formed terms that need to
   268   be excluded by reasoning about a well-formedness predicate.
   268   be excluded by reasoning about a well-formedness predicate.
   269 
   269 
   270   The problem with introducing a new type in Isabelle/HOL is that in order to be useful 
   270   The problem with introducing a new type in Isabelle/HOL is that in order to be useful 
   271   a resoning infrastructure needs to be ``lifted'' from the underlying subset to 
   271   a reasoning infrastructure needs to be ``lifted'' from the underlying subset to 
   272   the new type. This is usually a tricky and arduous task. To ease it
   272   the new type. This is usually a tricky and arduous task. To ease it
   273   we reimplemented in Isabelle/HOL the quotient package described by Homeier 
   273   we reimplemented in Isabelle/HOL the quotient package described by Homeier 
   274   \cite{Homeier05}. Given that alpha is an equivalence relation, this package 
   274   \cite{Homeier05}. Given that alpha is an equivalence relation, this package 
   275   allows us to automatically lift definitions and theorems involving raw terms
   275   allows us to automatically lift definitions and theorems involving raw terms
   276   to definitions and theorems involving alpha-equated terms. This of course
   276   to definitions and theorems involving alpha-equated terms. This of course
   277   only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence.
   277   only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence.
   278   Hence we will be able to lift, for instance, the function for free
   278   Hence we will be able to lift, for instance, the function for free
   279   variables of raw terms to alpha-equated terms (since this function respects 
   279   variables of raw terms to alpha-equated terms (since this function respects 
   280   alpha-equivalence), but we will not be able to do this with a bound-variable
   280   alpha-equivalence), but we will not be able to do this with a bound-variable
   281   function (since it does not respect alpha-equivalence). As a result, each
   281   function (since it does not respect alpha-equivalence). As a result, each
   282   lifting needs some respectulness proofs which we automated.\medskip
   282   lifting needs some respectfulness proofs which we automated.\medskip
   283 
   283 
   284   \noindent
   284   \noindent
   285   {\bf Contributions:}  We provide new definitions for when terms
   285   {\bf Contributions:}  We provide new definitions for when terms
   286   involving multiple binders are alpha-equivalent. These definitions are
   286   involving multiple binders are alpha-equivalent. These definitions are
   287   inspired by earlier work of Pitts \cite{}. By means of automatic
   287   inspired by earlier work of Pitts \cite{}. By means of automatic
   361 
   361 
   362 
   362 
   363 section {* General Binders *}
   363 section {* General Binders *}
   364 
   364 
   365 text {*
   365 text {*
   366   In order to keep our work managable we give need to give definitions  
   366   In order to keep our work manageable we give need to give definitions  
   367   and perform proofs inside Isabelle whereever possible, as opposed to write
   367   and perform proofs inside Isabelle wherever possible, as opposed to write
   368   custom ML-code that generates them  for each 
   368   custom ML-code that generates them  for each 
   369   instance of a term-calculus. To this end we will first consider pairs
   369   instance of a term-calculus. To this end we will first consider pairs
   370 
   370 
   371   \begin{equation}\label{three}
   371   \begin{equation}\label{three}
   372   \mbox{@{text "(as, x) :: (atom set) \<times> \<beta>"}}
   372   \mbox{@{text "(as, x) :: (atom set) \<times> \<beta>"}}
   376   consisting of a set of atoms and an object of generic type. These pairs
   376   consisting of a set of atoms and an object of generic type. These pairs
   377   are intended to represent the abstraction or binding of the set $as$ 
   377   are intended to represent the abstraction or binding of the set $as$ 
   378   in the body $x$ (similarly to type-schemes given in \eqref{tysch}). 
   378   in the body $x$ (similarly to type-schemes given in \eqref{tysch}). 
   379 
   379 
   380   The first question we have to answer is when we should consider pairs such as
   380   The first question we have to answer is when we should consider pairs such as
   381   $(as, x)$ and $(bs, y)$ as alpha-equivelent? (At the moment we are interested in
   381   $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in
   382   the notion of alpha-equivalence that is \emph{not} preserved by adding 
   382   the notion of alpha-equivalence that is \emph{not} preserved by adding 
   383   vacuous binders.) For this we identify four conditions: i) given a free-variable function
   383   vacuous binders.) To answer this we identify four conditions: {\it i)} given 
   384   of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$ 
   384   a free-variable function of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$ 
   385   need to have the same set of free variables; ii) there must be a permutation,
   385   need to have the same set of free variables; moreover there must be a permutation,
   386   say $p$, that leaves the free variables $x$ and $y$ unchanged, but ``moves'' their bound names 
   386   $p$ that {\it ii)} leaves the free variables $x$ and $y$ unchanged, 
   387   so that we obtain modulo a relation, say @{text "_ R _"}, 
   387   but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, 
   388   two equal terms. We also require that $p$ makes the abstracted sets equal. These 
   388   say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes 
   389   requirements can be stated formally as
   389   the abstracted sets $as$ and $bs$ equal (since at the moment we do not want 
   390 
   390   that the sets $as$ and $bs$ differ on vacuous binders). These requirements can 
   391   \begin{center}
   391   be stated formally as follows
   392   \begin{tabular}{rcl}
   392   %
   393   a
   393   \begin{equation}\label{alphaset}
   394   \end{tabular}
   394   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
   395   \end{center}
   395   \multicolumn{2}{l}{(as, x) \approx_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
   396 
   396              & @{text "fv(x) - as = fv(y) - bs"}\\
   397 
   397   \wedge     & @{text "fv(x) - as #* p"}\\
   398   Assuming we are given a free-variable function, say 
   398   \wedge     & @{text "(p \<bullet> x) R y"}\\
   399   \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then we expect for two alpha-equivelent
   399   \wedge     & @{text "(p \<bullet> as) = bs"}\\ 
   400   pairs that their sets of free variables aggree. That is
   400   \end{array}
   401   %
   401   \end{equation}
   402   \begin{equation}\label{four}
   402 
   403   \mbox{@{text "(as, x) \<approx> (bs, y)"} \hspace{2mm}implies\hspace{2mm} @{text "fv(x) - as = fv(y) - bs"}} 
   403   \noindent
   404   \end{equation}
   404   Alpha equivalence between such pairs is then the relation with the additional 
   405 
   405   existential quantification over $p$. Note that this relation is additionally 
   406   \noindent
   406   dependent on the free-variable function $\fv$ and the relation $R$. The reason 
   407   Next we expect that there is a permutation, say $p$, that leaves the 
   407   for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms
   408   free variables unchanged, but ``moves'' the bound names in $x$ so that
   408   and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and
   409   we obtain $y$ modulo a relation, say @{text "_ R _"}, that characterises when two
   409   we are going to prove that $\fv$ will be equal to the support of $x$ and $y$.
   410   elments of type $\beta$ are equivalent. We also expect that $p$ 
   410 
   411   makes the binders equal. We can formulate these requirements as: there
   411   The definition in \eqref{alphaset} does not make any distinction between the
   412   exists a $p$ such that $i)$  @{term "(fv(x) - as) \<sharp>* p"}, $ii)$ @{text "(p \<bullet> x) R y"} and
   412   order of abstracted variables. If we do want this then we can define alpha-equivalence 
   413   $iii)$ @{text "(p \<bullet> as) = bs"}. 
   413   for pairs of the form \mbox{@{text "(as, x) :: (atom list) \<times> \<beta>"}} by
   414 
   414   %
   415   We take now \eqref{four} and the three 
   415   \begin{equation}\label{alphalist}
   416  
   416   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
   417 
   417   \multicolumn{2}{l}{(as, x) \approx_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
   418   General notion of alpha-equivalence (depends on a free-variable
   418              & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
   419   function and a relation).
   419   \wedge     & @{text "fv(x) - (set as) #* p"}\\
       
   420   \wedge     & @{text "(p \<bullet> x) R y"}\\
       
   421   \wedge     & @{text "(p \<bullet> as) = bs"}\\ 
       
   422   \end{array}
       
   423   \end{equation}
       
   424   
       
   425   \noindent
       
   426   where $set$ is just the function that coerces a list of atoms into a set of atoms.
       
   427 
       
   428   If we do not want to make any difference between the order of binders and
       
   429   allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset}
       
   430   and define
       
   431   %
       
   432   \begin{equation}\label{alphaset}
       
   433   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
       
   434   \multicolumn{2}{l}{(as, x) \approx_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
       
   435              & @{text "fv(x) - as = fv(y) - bs"}\\
       
   436   \wedge     & @{text "fv(x) - as #* p"}\\
       
   437   \wedge     & @{text "(p \<bullet> x) R y"}\\
       
   438   \end{array}
       
   439   \end{equation}
       
   440 
       
   441   To get a feeling how these definitions pan out in practise consider the case of 
       
   442   abstracting names over types (like in type-schemes). For this we set $R$ to be 
       
   443   the equality and for $\fv(T)$ we define
       
   444 
       
   445   \begin{center}
       
   446   $\fv(x) = \{x\}  \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$
       
   447   \end{center}
       
   448 
       
   449   \noindent
       
   450   Now reacall the examples in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}: it can be easily 
       
   451   checked that @{text "({x,y}, x \<rightarrow> y)"} and
       
   452   @{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{ref}$ by taking $p$ to
       
   453   be the swapping @{text "(x \<rightleftharpoons> y)"}; but assuming @{text "x \<noteq> y"} then for instance 
       
   454   $([x,y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that 
       
   455   makes the lists @{text "[x,y]"} and @{text "[y,x]"} equal, but leaves the type \mbox{@{text "x \<rightarrow> y"}}
       
   456   unchanged.
   420 *}
   457 *}
   421 
   458 
   422 section {* Alpha-Equivalence and Free Variables *}
   459 section {* Alpha-Equivalence and Free Variables *}
   423 
   460 
   424 text {*
   461 text {*
   425   Restrictions
   462   Restrictions
   426 
   463 
   427   \begin{itemize}
   464   \begin{itemize}
   428   \item non-emptyness
   465   \item non-emptiness
   429   \item positive datatype definitions
   466   \item positive datatype definitions
   430   \item finitely supported abstractions
   467   \item finitely supported abstractions
   431   \item respectfulness of the bn-functions\bigskip
   468   \item respectfulness of the bn-functions\bigskip
   432   \item binders can only have a ``single scope''
   469   \item binders can only have a ``single scope''
   433   \end{itemize}
   470   \end{itemize}