--- a/Pearl-jv/Paper.thy Wed Mar 02 00:06:28 2011 +0000
+++ b/Pearl-jv/Paper.thy Tue Mar 08 09:07:27 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 "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
+ @{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"}
\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 "_ \<bullet> _"}, 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 "\<Gamma>"} of the form
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^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 \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for
+ all permutations @{text "\<pi>"}. This is \emph{not} the case for arbitrary
+ renaming substitutions, as they might identify some variables in @{text \<Gamma>}.
+ 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 "\<forall>\<pi>. \<pi> \<bullet> 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 "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^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
+ "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^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\<iota> = Atom\<iota> 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 \<notin> 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="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
- @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
+ @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm}
+ @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{5mm}
+ @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{5mm}
@{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
\end{tabular}
\end{isabelle}
@@ -221,16 +270,15 @@
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}
- @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}
- @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}
+ @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{5mm}
+ @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{5mm}
+ @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{5mm}
@{thm group_add_class.left_minus[where a="\<pi>::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 \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} 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 "\<beta>"} 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 "\<pi> \<bullet> _"}~~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="\<pi>",no_vars, THEN eq_reflection]}\\
- 2) & functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
- 3) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
- 4) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- 5) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- 6) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ \begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}}
+ a) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
+ b) & functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
+ c) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
+ d) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ e) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ f) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
& & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- 7) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- 8) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ g) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ h) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
\end{tabular}}
\end{equation}
--- a/Slides/Slides1.thy Wed Mar 02 00:06:28 2011 +0000
+++ b/Slides/Slides1.thy Tue Mar 08 09:07:27 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<presentation>{
\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<presentation>{
\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<presentation>{
+ \begin{frame}<1->[c]
\frametitle{\begin{tabular}{c}Questions?\end{tabular}}
\mbox{}\\[-6mm]
@@ -1070,6 +1087,8 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+
+
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -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}}