# HG changeset patch # User Christian Urban # Date 1286874468 -3600 # Node ID e7cc033f72c72b423f7f7818814759af29d6c73b # Parent d65a19b070bbccf52d48ccab62025a0f49ae0923 tiny work on the pearl paper diff -r d65a19b070bb -r e7cc033f72c7 Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Fri Oct 08 23:53:51 2010 +0100 +++ b/Pearl-jv/Paper.thy Tue Oct 12 10:07:48 2010 +0100 @@ -39,41 +39,44 @@ (*>*) +(* + TODO: write about supp of finite sets, abstraction over finite sets +*) + section {* Introduction *} text {* - TODO: write about supp of finite sets + Nominal Isabelle provides a proving infratructure for convenient reasoning + about programming languages involving binders such as lambda abstractions or + quantifications in type schemes: - Nominal Isabelle provides a proving infratructure for - convenient reasoning about programming languages. At its core Nominal - Isabelle is based on the nominal logic work by Pitts at al - \cite{GabbayPitts02,Pitts03}. The most basic notion in this work - is a sort-respecting permutation operation defined over a countably infinite - collection of sorted atoms. The atoms are used for representing variables - that might be bound. Multiple sorts are necessary for being able to + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "\x. t \{x\<^isub>1,\,x\<^isub>n}. \"} + \hfill\numbered{atomperm} + \end{isabelle} + + \noindent + At its core Nominal Isabelle is based on the nominal logic work by Pitts at + al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a + sort-respecting permutation operation defined over a countably infinite + collection of sorted atoms. The atoms are used for representing variable names + that might be free or bound. 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 and bound type variables; each kind needs to - be represented by a different sort of atoms. + 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. In our formalisation of the nominal logic work, we have to make a design decision about how to represent sorted atoms and sort-respecting permutations. One possibility - is to - - - -% Unfortunately, the type system of Isabelle/HOL is not a good fit for the way -% atoms and sorts are used in the original formulation of the nominal logic work. -% The reason is that one has to ensure that permutations are sort-respecting. -% This was done implicitly in the original nominal logic work \cite{Pitts03}. - - - Isabelle used the two-place permutation operation with the generic type + is to have separate types for the different kinds of atoms. With this one can represent + permutations as lists of pairs of atoms and the operation of applying + a permutation to an object as the overloaded function @{text [display,indent=10] "_ \ _ :: (\ \ \) list \ \ \ \"} \noindent - where @{text "\"} stands for the type of atoms and @{text "\"} for the type - of the objects on which the permutation acts. For atoms of type @{text "\"} + where @{text "\"} stands for a type of atoms and @{text "\"} for the type + of the objects on which the permutation acts. For atoms the permutation operation is defined over the length of lists as follows \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -91,15 +94,58 @@ @{text "b"}. For atoms of different type, the permutation operation is defined as @{text "\ \ c \ c"}. - With the list representation of permutations it is impossible to state an - ``ill-sorted'' permutation, since the type system excludes lists containing - atoms of different type. Another advantage of the list representation is that - the basic operations on permutations are already defined in the list library: - composition of two permutations (written @{text "_ @ _"}) is just list append, - and inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just - list reversal. A disadvantage is that permutations do not have unique - representations as lists; we had to explicitly identify permutations according - to the relation + +% Unfortunately, the type system of Isabelle/HOL is not a good fit for the way +% atoms and sorts are used in the original formulation of the nominal logic work. +% The reason is that one has to ensure that permutations are sort-respecting. +% This was done implicitly in the original nominal logic work \cite{Pitts03}. + + + With the separate atom types and the list representation of permutations it + is impossible to state an ``ill-sorted'' permutation, since the type system + excludes lists containing atoms of different type. However, whenever we + need to generalise induction hypotheses by quantifying over permutations, we + have to build cumbersome quantifications like + + @{text [display,indent=10] "\\\<^isub>1 \ \\\<^isub>n. \"} + + \noindent + where the @{text "\\<^isub>i"} are of type @{text "(\\<^isub>i \ \\<^isub>i) list"}. + The reason is that the permutation operation behaves differently for + every @{text "\\<^isub>i"}. Similarly, the notion of support + + @{text [display,indent=10] "supp _ :: \ \ \ set"} + + \noindent + which we will define later, cannot be + used to express the support of an object over \emph{all} atoms. The reason + is that support can behave differently for each @{text + "\\<^isub>i"}. This problem is annoying, because if we need to know in + a statement that an object, say @{text "x"}, is finitely supported we end up + with having to state premises of the form + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{text "finite ((supp x) :: \\<^isub>1 set) , \, finite ((supp x) :: \\<^isub>n set)"} + \end{tabular}\hfill\numbered{fssequence} + \end{isabelle} + + + + + + + + + + An advantage of the + list representation is that the basic operations on permutations are already + defined in the list library: composition of two permutations (written @{text + "_ @ _"}) is just list append, and inversion of a permutation (written + @{text "_\<^sup>-\<^sup>1"}) is just list reversal. A disadvantage is that + permutations do not have unique representations as lists; we had to + explicitly identify permutations according to the relation + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} diff -r d65a19b070bb -r e7cc033f72c7 Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Fri Oct 08 23:53:51 2010 +0100 +++ b/Pearl-jv/document/root.tex Tue Oct 12 10:07:48 2010 +0100 @@ -37,7 +37,8 @@ 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. Furthermore we extend the nominal -logic work with names that carry additional information. +logic work with names that carry additional information and with abstractions +that bind finite sets of names. \end{abstract} % generated text of all theories