# HG changeset patch # User Christian Urban # Date 1299575269 0 # Node ID 651355113eeec3339315396f7667ee19c889f4e2 # Parent a9e63abf3febc9f8eda8d120111a36a997a5c285# Parent b5ffcb30b6d0252ff7548688319f1f5998b4140d merged diff -r b5ffcb30b6d0 -r 651355113eee Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Wed Mar 02 16:07:56 2011 +0900 +++ b/Pearl-jv/Paper.thy Tue Mar 08 09:07:49 2011 +0000 @@ -44,11 +44,10 @@ text {* Nominal Isabelle provides a proving infratructure for convenient reasoning - about programming language calculi involving binders, such as lambda abstractions or - quantifications in type schemes: + about syntax involving binders, such as lambda terms or type schemes: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\x. t \{x\<^isub>1,\,x\<^isub>n}. \"} + @{text "\x. t \{x\<^isub>1,\, x\<^isub>n}. \"} \hfill\numbered{atomperm} \end{isabelle} @@ -56,12 +55,59 @@ At its core Nominal Isabelle is based on the nominal logic work by Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a sort-respecting permutation operation defined over a countably infinite - collection of sorted atoms. The nominal logic work has been starting - point for a number of formalisations, most notable Norrish \cite{norrish04} - in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own - work in Isabelle/HOL. + collection of sorted atoms. The atoms are used for representing variable names + that might be bound or free. Multiple sorts are necessary for being able to + represent different kinds of variables. For example, in the language Mini-ML + there are bound term variables in lambda abstractions and bound type variables in + type schemes. In order to be able to separate them, each kind of variables needs to be + represented by a different sort of atoms. + + The nominal logic work has been the starting point for a number of proving + infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by + Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and teh work by Urban + and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very + general notion, called \emph{support}, for the `set of free variables, or + atoms' of an object that applies not just to lambda terms and type schemes, + but also to sets, products, lists and even functions. The notion of support + is derived from the permutation operation defined over atoms. This + permutation operation, written @{text "_ \ _"}, has proved to be very + convenient for reasoning about syntax, in comparison to, say, arbitrary + renaming substitutions of atoms. The reason is that permutations are + bijective renamings of atoms and thus they can be easily `undone'---namely + by applying the inverse permutation. A corresponding inverse substitution + might not exist in general, since renaming substitutions are only injective. + Permutations also preserve many constructions when reasoning about syntax. + For example validity of a typing context is preserved under permutations. + Suppose a typing context @{text "\"} of the form + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "x\<^isub>1:\\<^isub>1, \, x\<^isub>n:\\<^isub>n"} + \end{isabelle} + + \noindent + is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"} + occur twice. Then validity is preserved under + permutations in the sense that if @{text \} is valid then so is @{text "\ \ \"} for + all permutations @{text "\"}. This is \emph{not} the case for arbitrary + renaming substitutions, as they might identify some variables in @{text \}. + Permutations fit well with HOL's definitions. For example + + Because + of the good properties of permutations, we will be able to automate reasoning + steps determining when a construction in HOL is + \emph{equivariant}. By equivariance we mean the property that every + permutation leaves an object unchanged, that is @{term "\\. \ \ x = x"}. + This will often simplify arguments involving the notion of support. + + + There are a number of subtle differences between the nominal logic work by Pitts + and the one we will present in this paper. Nominal + + In the nominal logic work, the `new quantifier' plays a prominent role. + + + Using a single atom type to represent atoms of different sorts and representing permutations as functions are not new ideas; see \cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution @@ -74,34 +120,30 @@ depend on type annotations. The paper is organised as follows\ldots + + + Two binders *} section {* Sorted Atoms and Sort-Respecting Permutations *} text {* - The most basic notion in this work is a + The two most basic notions in the nominal logic work are sort-respecting permutation operation defined over a countably infinite - collection of sorted atoms. The atoms are used for representing variable names - that might be bound or free. Multiple sorts are necessary for being able to - represent different kinds of variables. For example, in the language Mini-ML - there are bound term variables in lambda abstractions and bound type variables in - type schemes. In order to be able to separate them, each kind of variables needs to be - represented by a different sort of atoms. - - + collection of sorted atoms. The existing nominal logic work usually leaves implicit the sorting information for atoms and as far as we know leaves out a description of how sorts are represented. In our formalisation, we therefore have to make a design decision about how to implement sorted atoms and sort-respecting - permutations. One possibility, which we described in \cite{Urban08}, is to - have separate types for the different - kinds of atoms, say types @{text "\\<^isub>1,\,\\<^isub>n"}. + permutations. One possibility, which we described in \cite{Urban08}, is to + have separate types for the different kinds of atoms, say types @{text + "\\<^isub>1,\,\\<^isub>n"}. However, this does not blend well with the + resoning infrastructure of type-classes in Isabelle/HOL (see Section ??? + about related work). Therefore we use here a single unified atom type to + represent atoms of different sorts. A basic requirement is that there must + be a countably infinite number of atoms of each sort. This can be + implemented as the datatype - In the nominal logic work of Pitts, binders and bound variables are - represented by \emph{atoms}. As stated above, we need to have different - \emph{sorts} of atoms to be able to bind different kinds of variables. A - basic requirement is that there must be a countably infinite number of atoms - of each sort. We implement these atoms as *} datatype atom\ = Atom\ string nat @@ -110,13 +152,19 @@ \noindent whereby the string argument specifies the sort of the atom.\footnote{A similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} - for their variables.} (The use of type \emph{string} is merely for - convenience; any countably infinite type would work as well.) We have an - auxiliary function @{text sort} that is defined as @{thm - sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} + for their variables.} The use of type \emph{string} for sorts is merely for + convenience; any countably infinite type would work as well. We have an + auxiliary function @{text sort} that is defined as + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{thm sort_of.simps[no_vars, THEN eq_reflection]} + \end{isabelle} + + \noindent + and we clearly have for every finite set @{text S} of atoms and every sort @{text s} the property: - \begin{proposition}\label{choosefresh} + \begin{proposition}\label{choosefresh}\mbox{}\\ @{text "For a finite set of atoms S, there exists an atom a such that sort a = s and a \ S"}. \end{proposition} @@ -174,8 +222,8 @@ the value of @{text "(a b)"} is unspecified. However, this looked like a cumbersome solution, since sort-related side conditions would be required everywhere, even to unfold the definition. It turned out to be more - convenient to actually allow the user to state ``ill-sorted'' swappings but - limit their ``damage'' by defaulting to the identity permutation in the + convenient to actually allow the user to state `ill-sorted' swappings but + limit their `damage' by defaulting to the identity permutation in the ill-sorted case: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -191,7 +239,7 @@ @{text a} and @{text b}, and sort respecting. Therefore it is a function in @{typ perm}. - One advantage of using functions instead of lists as a representation for + One advantage of using functions as a representation for permutations is that for example the swappings \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -202,16 +250,17 @@ \end{isabelle} \noindent - are \emph{equal}. We do not have to use the equivalence relation shown - in~\eqref{permequ} to identify them, as we would if they had been represented - as lists of pairs. Another advantage of the function representation is that - they form a (non-commutative) group provided we define + are \emph{equal}. Therfore we can use for permutations HOL's built-in + principle of `replacing equals by equals in any context'. Another advantage + of the function representation is that they form a (non-commutative) group + provided we define + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} - @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{4mm} - @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{4mm} + @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm} + @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{5mm} + @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{5mm} @{thm minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} \end{tabular} \end{isabelle} @@ -221,16 +270,15 @@ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm add_assoc[where a="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]} \hspace{3mm} - @{thm monoid_add_class.add_0_left[where a="\::perm"]} \hspace{3mm} - @{thm monoid_add_class.add_0_right[where a="\::perm"]} \hspace{3mm} + @{thm add_assoc[where a="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]} \hspace{5mm} + @{thm monoid_add_class.add_0_left[where a="\::perm"]} \hspace{5mm} + @{thm monoid_add_class.add_0_right[where a="\::perm"]} \hspace{5mm} @{thm group_add_class.left_minus[where a="\::perm"]} \end{tabular} \end{isabelle} \noindent - Again this is in contrast to the list-of-pairs representation which does not - form a group. The technical importance of this fact is that we can rely on + The technical importance of this fact is that we can rely on Isabelle/HOL's existing simplification infrastructure for groups, which will come in handy when we have to do calculations with permutations. Note that Isabelle/HOL defies standard conventions of mathematical notation @@ -240,9 +288,8 @@ nominal theory as smoothly as possible in Isabelle/HOL, we tolerate the non-standard notation in order to reuse the existing libraries. - By formalising permutations abstractly as functions, and using a single type - for all atoms, we can now restate the \emph{permutation properties} from - \eqref{permprops} as just the two equations + In order to reason abstractly about permutations, we state the following two + \emph{permutation properties} \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} @@ -252,14 +299,11 @@ \end{isabelle} \noindent - in which the permutation operations are of type @{text "perm \ \ \ \"} and so - have only a single type parameter. Consequently, these properties are - compatible with the one-parameter restriction of Isabelle/HOL's type classes. - There is no need to introduce a separate type class instantiated for each - sort, like in the old approach. - - The next notion allows us to establish generic lemmas involving the - permutation operation. + We state these properties in terms of Isabelle/HOL's type class + mechanism \cite{}. + This allows us to delegate much of the resoning involved in + determining whether these properties are satisfied to the type system. + For this we define \begin{definition} A type @{text "\"} is a \emph{permutation type} if the permutation @@ -268,7 +312,8 @@ \end{definition} \noindent - First, it follows from the laws governing + The type class also allows us to establish generic lemmas involving the + permutation operation. First, it follows from the laws governing groups that a permutation and its inverse cancel each other. That is, for any @{text "x"} of a permutation type: @@ -281,6 +326,7 @@ \end{isabelle} \noindent + ??? Proof Consequently, in a permutation type the permutation operation @{text "\ \ _"}~~is bijective, which in turn implies the property @@ -316,16 +362,16 @@ \begin{equation}\label{permdefs} \mbox{ - \begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}} - 1) & atoms: & @{thm permute_atom_def[where p="\",no_vars, THEN eq_reflection]}\\ - 2) & functions: & @{text "\ \ f \ \x. \ \ (f ((-\) \ x))"}\\ - 3) & permutations: & @{thm permute_perm_def[where p="\" and q="\'", THEN eq_reflection]}\\ - 4) & sets: & @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ - 5) & booleans: & @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]}\\ - 6) & lists: & @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ + \begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}} + a) & atoms: & @{thm permute_atom_def[where p="\",no_vars, THEN eq_reflection]}\\ + b) & functions: & @{text "\ \ f \ \x. \ \ (f ((-\) \ x))"}\\ + c) & permutations: & @{thm permute_perm_def[where p="\" and q="\'", THEN eq_reflection]}\\ + d) & sets: & @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ + e) & booleans: & @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]}\\ + f) & lists: & @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ & & @{thm permute_list.simps(2)[where p="\", no_vars, THEN eq_reflection]}\\ - 7) & products: & @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\ - 8) & nats: & @{thm permute_nat_def[where p="\", no_vars, THEN eq_reflection]}\\ + g) & products: & @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\ + h) & nats: & @{thm permute_nat_def[where p="\", no_vars, THEN eq_reflection]}\\ \end{tabular}} \end{equation} diff -r b5ffcb30b6d0 -r 651355113eee Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Wed Mar 02 16:07:56 2011 +0900 +++ b/Pearl-jv/document/root.tex Tue Mar 08 09:07:49 2011 +0000 @@ -37,12 +37,12 @@ notions of atoms, permutations and support. The engineering challenge is to smoothly adapt this theory to a theorem prover environment, in our case Isabelle/HOL. For this we have to formulate the theory so that it is -compatible with choice principles, which the work by Pitts is not. We -present a formalisation of this work that is based on a unified atom type +compatible with HOL, which the original formulation by Pitts is not. We +present a formalisation that is based on a unified atom type and that represents permutations by bijective functions from atoms to atoms. Interestingly, we allow swappings, which are permutations build from two -atoms, to be ill-sorted. We also describe a formalisation of an -abstraction operator that binds sets of names. +atoms, to be ill-sorted. We also describe a formalisation of two +abstraction operators that bind sets of names. \end{abstract} % generated text of all theories diff -r b5ffcb30b6d0 -r 651355113eee Slides/Slides1.thy --- a/Slides/Slides1.thy Wed Mar 02 16:07:56 2011 +0900 +++ b/Slides/Slides1.thy Tue Mar 08 09:07:49 2011 +0000 @@ -11,7 +11,8 @@ text_raw {* - \renewcommand{\slidecaption}{Cambridge, 8.~June 2010} + %%\renewcommand{\slidecaption}{Cambridge, 8.~June 2010} + \renewcommand{\slidecaption}{Uppsala, 3.~March 2011} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<1>[t] @@ -187,8 +188,8 @@ \onslide<2->{ \begin{center} - \isacommand{bind\_res}\hspace{6mm} - \isacommand{bind\_set}\hspace{6mm} + \isacommand{bind (set+)}\hspace{6mm} + \isacommand{bind (set)}\hspace{6mm} \isacommand{bind} \end{center}} @@ -268,19 +269,19 @@ \begin{center} \begin{tabular}{l} \isacommand{bind} a b c \ldots \isacommand{in} x y z \ldots\\ - \isacommand{bind\_set} a b c \ldots \isacommand{in} x y z \ldots\\ - \isacommand{bind\_res} a b c \ldots \isacommand{in} x y z \ldots + \isacommand{bind (set)} a b c \ldots \isacommand{in} x y z \ldots\\ + \isacommand{bind (set+)} a b c \ldots \isacommand{in} x y z \ldots \end{tabular} \end{center}\bigskip\medskip the reason is that with our definition of $\alpha$-equivalence\medskip \begin{center} \begin{tabular}{l} - \isacommand{bind\_res} as \isacommand{in} x y $\not\Leftrightarrow$\\ - \hspace{8mm}\isacommand{bind\_res} as \isacommand{in} x, \isacommand{bind\_res} as \isacommand{in} y + \isacommand{bind (set+)} as \isacommand{in} x y $\not\Leftrightarrow$\\ + \hspace{8mm}\isacommand{bind (set+)} as \isacommand{in} x, \isacommand{bind (set+)} as \isacommand{in} y \end{tabular} \end{center}\medskip - same with \isacommand{bind\_set} + same with \isacommand{bind (set)} \end{itemize}} \end{itemize} @@ -374,7 +375,7 @@ \begin{tabular}{@ {\hspace{1cm}}l} $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-6>{${}_{\text{set}}$}% \only<7>{${}_{\text{\alert{list}}}$}% - \only<8>{${}_{\text{\alert{res}}}$}}% + \only<8>{${}_{\text{\alert{set+}}}$}}% \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$ \end{tabular}\bigskip \end{itemize} @@ -438,7 +439,7 @@ {\tiny\color{darkgray} \begin{minipage}{3.4cm}\raggedright \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{res:}\\ + \multicolumn{2}{@ {}l}{set+:}\\ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ $\wedge$ & $\pi \cdot x = y$\\ @@ -497,7 +498,7 @@ \end{center} \begin{itemize} - \item $\approx_{\text{res}}$, $\approx_{\text{set}}$% + \item $\approx_{\text{set+}}$, $\approx_{\text{set}}$% \only<2>{, \alert{$\not\approx_{\text{list}}$}} \end{itemize} @@ -509,7 +510,7 @@ {\tiny\color{darkgray} \begin{minipage}{3.4cm}\raggedright \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{res:}\\ + \multicolumn{2}{@ {}l}{set+:}\\ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ $\wedge$ & $\pi \cdot x = y$\\ @@ -567,7 +568,7 @@ \end{center} \begin{itemize} - \item $\approx_{\text{res}}$, $\not\approx_{\text{set}}$, + \item $\approx_{\text{set+}}$, $\not\approx_{\text{set}}$, $\not\approx_{\text{list}}$ \end{itemize} @@ -579,7 +580,7 @@ {\tiny\color{darkgray} \begin{minipage}{3.4cm}\raggedright \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{res:}\\ + \multicolumn{2}{@ {}l}{set+:}\\ $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ $\wedge$ & $\pi \cdot x = y$\\ @@ -668,7 +669,7 @@ \only<1->{ \begin{textblock}{8}(12,3.8) - \footnotesize $^*$ set, res, list + \footnotesize $^*$ set, set+, list \end{textblock}} \end{frame}} @@ -883,7 +884,7 @@ \infer[\text{LetRec-}\!\approx_\alpha] {\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'} {(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} - ^{R,fv} (\text{bn}(as'), (t', as'))} + ^{R,\text{fv}} (\text{bn}(as'), (t', as'))} \]\bigskip \onslide<1->{\alert{deep recursive binders}} @@ -933,7 +934,7 @@ \item the properties for support are implied by the properties of $[\_].\_$ - \item we can derive strong induction principles (almost automatic---matter of time) + \item we can derive strong induction principles \end{itemize} @@ -981,7 +982,7 @@ \begin{itemize} \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions \begin{center} - $\sim$ 1 min + $\sim$ 2 mins \end{center} \end{itemize} @@ -1059,6 +1060,22 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<1->[c] + \frametitle{\begin{tabular}{c}Future Work\end{tabular}} + \mbox{}\\[-6mm] + + \begin{itemize} + \item Function definitions + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1->[c] \frametitle{\begin{tabular}{c}Questions?\end{tabular}} \mbox{}\\[-6mm] @@ -1070,6 +1087,8 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} + + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -1088,10 +1107,10 @@ \end{center} \onslide<2-> - {1.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$, - \isacommand{bind\_set} as \isacommand{in} $\tau_2$\medskip + {1.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$, + \isacommand{bind (set)} as \isacommand{in} $\tau_2$\medskip - 2.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$ $\tau_2$ + 2.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$ $\tau_2$ } \end{frame}}