# HG changeset patch # User Christian Urban # Date 1273088361 -3600 # Node ID c5d28ebf9dab3bd5a955056e933029f64d483b26 # Parent 2725853f43b9338df771cba94769a827e58b56ff a bit mor on the pearl journal paper diff -r 2725853f43b9 -r c5d28ebf9dab Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Wed May 05 10:24:54 2010 +0100 +++ b/Pearl-jv/Paper.thy Wed May 05 20:39:21 2010 +0100 @@ -44,30 +44,23 @@ section {* Introduction *} text {* - The purpose of Nominal Isabelle is to provide a proving infratructure - for conveninet reasoning about programming languages. At its core - Nominal Isabelle is based on nominal logic by Pitts at al - \cite{GabbayPitts02,Pitts03}. - - Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem - prover providing a proving infrastructure for convenient reasoning about - programming languages. At its core Nominal Isabelle is based on the nominal - logic work of Pitts et 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 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. - + 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 + 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. 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. - Therefore it was decided in earlier versions of Nominal Isabelle to use a - separate type for each sort of atoms and let the type system enforce the - sort-respecting property of permutations. Inspired by the work on nominal - unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also - implement permutations concretely as lists of pairs of atoms. Thus Nominal + 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 @{text [display,indent=10] "_ \ _ :: (\ \ \) list \ \ \ \"} @@ -225,6 +218,13 @@ \cite{PittsHOL4} where variables and variable binding depend on type annotations. + Therefore it was decided in earlier versions of Nominal Isabelle to use a + separate type for each sort of atoms and let the type system enforce the + sort-respecting property of permutations. Inspired by the work on nominal + unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also + implement permutations concretely as lists of pairs of atoms. + + *} section {* Sorted Atoms and Sort-Respecting Permutations *} diff -r 2725853f43b9 -r c5d28ebf9dab Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Wed May 05 10:24:54 2010 +0100 +++ b/Pearl-jv/document/root.tex Wed May 05 20:39:21 2010 +0100 @@ -31,14 +31,13 @@ \begin{abstract} Pitts et al introduced a beautiful theory about names and binding based on the -notions of atoms, permutations and support. The engineering challenge -is to smoothly adapt this theory to a theorem prover environment, in our case +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. We present a formalisation of this work that is based on a -unified atom type (that includes all sorts of atoms) 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 can extend the nominal logic with names that carry -additional information. +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. \end{abstract} % generated text of all theories