# HG changeset patch # User Christian Urban # Date 1271684253 -7200 # Node ID 23e3dc4f2c597a2641f68c5e54dc4ff22e8072cf # Parent edf10db61708c6088d994ddf1addd8800775430f small updates to the paper; remaining points in PAPER-TODO diff -r edf10db61708 -r 23e3dc4f2c59 PAPER-TODO --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/PAPER-TODO Mon Apr 19 15:37:33 2010 +0200 @@ -0,0 +1,20 @@ +_{res} -> _{\textrm{res}} etc.; same for =^{def}? + +Nominal Isabelle view, rather than functional programming view +(e.g. first sentence of Abstract and Intro) + + +:: for cons might need some explanations, esp. that it's also used later +next to labels in nominal types (e.g. x::name t::lam). + + +Ott-tool -> Ott tool (throughout) + +I didn't quite get top of second column, p. 6 + +"the problem Pottier and Cheney pointed out": I had forgotten it in the +meantime + +the equation in the first actuall bullet on p. 8 lacks it =? + +missing v. spaces, top of 2nd col p. 8 \ No newline at end of file diff -r edf10db61708 -r 23e3dc4f2c59 Paper/Paper.thy --- a/Paper/Paper.thy Mon Apr 19 12:28:48 2010 +0200 +++ b/Paper/Paper.thy Mon Apr 19 15:37:33 2010 +0200 @@ -441,7 +441,7 @@ acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, and the inverse permutation of @{term p} as @{text "- p"}. The permutation - operation is defined by induction over the type-hierarchy (see \cite{HuffmanUrban10}); + operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10}; for example permutations acting on products, lists, sets, functions and booleans is given by: % @@ -614,7 +614,7 @@ "as"} in the body @{text "x"}. The first question we have to answer is when two pairs @{text "(as, x)"} and - @{text "(bs, y)"} are alpha-equivalent? (At the moment we are interested in + @{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in the notion of alpha-equivalence that is \emph{not} preserved by adding vacuous binders.) To answer this, we identify four conditions: {\it i)} given a free-variable function @{text "fv"} of type \mbox{@{text "\ \ atom @@ -680,7 +680,7 @@ \end{equation} It might be useful to consider some examples for how these definitions of alpha-equivalence - pan out in practise. + pan out in practice. For this consider the case of abstracting a set of variables over types (as in type-schemes). We set @{text R} to be the equality and for @{text "fv(T)"} we define @@ -784,8 +784,8 @@ \begin{center} \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\ - @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\ - @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]} + @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}\\ + @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]} \end{tabular} \end{center} \end{thm} @@ -809,7 +809,7 @@ \noindent The second fact derives from the definition of permutations acting on pairs - (see \eqref{permute}) and alpha-equivalence being equivariant + \eqref{permute} and alpha-equivalence being equivariant (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show the following lemma about swapping two atoms. @@ -1258,7 +1258,7 @@ \end{center} \noindent - To see how these definitions work in practise, let us reconsider the term-constructors + To see how these definitions work in practice, let us reconsider the term-constructors @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. For this specification we need to define three free-variable functions, namely @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows: @@ -1737,7 +1737,7 @@ $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\ \end{tabular} \end{boxedminipage} - \caption{The nominal datatype declaration for Core-Haskell. At the moment we + \caption{The nominal datatype declaration for Core-Haskell. For the moment we do not support nested types; therefore we explicitly have to unfold the lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved in a future version of Nominal Isabelle. Apart from that, the @@ -1917,7 +1917,7 @@ Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps}, we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}. This completes the proof showing that the strong induction principle derives from - the weak induction principle. At the moment we can derive the difficult cases of + the weak induction principle. For the moment we can derive the difficult cases of the strong induction principles only by hand, but they are very schematically so that with little effort we can even derive them for Core-Haskell given in Figure~\ref{nominalcorehas}. @@ -2004,7 +2004,7 @@ once. This extension has been tried out with the Core-Haskell term-calculus. For such general binders, we can also extend earlier work that derives strong induction principles which have the usual - variable convention already built in. At the moment we can do so only with manual help, + variable convention already built in. For the moment we can do so only with manual help, but future work will automate them completely. The code underlying the presented extension will become part of the Isabelle distribution, but for the moment it can be downloaded from the Mercurial repository linked at