# HG changeset patch # User Christian Urban # Date 1269815420 -7200 # Node ID 51bc795b81fd9f1cb1f466073c3619a22ed93375 # Parent 7b3dd407f6b3d70a82d0961555fcbaae08b16bc9 more on the paper diff -r 7b3dd407f6b3 -r 51bc795b81fd Nominal/ExCoreHaskell.thy --- a/Nominal/ExCoreHaskell.thy Sun Mar 28 22:54:38 2010 +0200 +++ b/Nominal/ExCoreHaskell.thy Mon Mar 29 00:30:20 2010 +0200 @@ -33,7 +33,8 @@ | CAll tv::"tvar" "ckind" C::"co" bind tv in C | CEq "co" "co" "co" | CSym "co" -| CCir "co" "co" +| CCir "co" "co" +(* At ??? *) | CLeft "co" | CRight "co" | CSim "co" diff -r 7b3dd407f6b3 -r 51bc795b81fd Paper/Paper.thy --- a/Paper/Paper.thy Sun Mar 28 22:54:38 2010 +0200 +++ b/Paper/Paper.thy Mon Mar 29 00:30:20 2010 +0200 @@ -41,7 +41,7 @@ \end{center} \noindent - where free and bound variables have names. For such terms Nominal Isabelle + where free and bound variables have names. For such alpha-equated terms, Nominal Isabelle derives automatically a reasoning infrastructure that has been used successfully in formalisations of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed @@ -52,8 +52,8 @@ binding \cite{SatoPollack10}. However, Nominal Isabelle has fared less well in a formalisation of - the algorithm W \cite{UrbanNipkow09}, where types and type-schemes - are of the form + the algorithm W \cite{UrbanNipkow09}, where types and type-schemes, + respectively, are of the form % \begin{equation}\label{tysch} \begin{array}{l} @@ -171,7 +171,8 @@ where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"} become bound in @{text s}. In this representation the term \mbox{@{text "\ [x].s [t\<^isub>1, t\<^isub>2]"}} would be a perfectly legal - instance. To exclude such terms, additional predicates about well-formed + instance, but the lengths of two lists do not agree. To exclude such terms, + additional predicates about well-formed terms are needed in order to ensure that the two lists are of equal length. This can result into very messy reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will allow type @@ -190,7 +191,7 @@ \noindent where @{text assn} is an auxiliary type representing a list of assignments and @{text bn} an auxiliary function identifying the variables to be bound - by the @{text "\"}. This function is defined by recursion over @{text + by the @{text "\"}. This function can be defined by recursion over @{text assn} as follows \begin{center} @@ -238,7 +239,9 @@ only support specifications that make sense on the level of alpha-equated terms (offending specifications, which for example bind a variable according to a variable bound somewhere else, are not excluded by Ott, but we have - to). Our insistence on reasoning with alpha-equated terms comes from the + to). + + Our insistence on reasoning with alpha-equated terms comes from the wealth of experience we gained with the older version of Nominal Isabelle: for non-trivial properties, reasoning about alpha-equated terms is much easier than reasoning with raw terms. The fundamental reason for this is @@ -311,7 +314,7 @@ \end{center} \noindent - then with not too great effort we obtain a function @{text "fv\<^sup>\"} + then with the help of te quotient package we obtain a function @{text "fv\<^sup>\"} operating on quotients, or alpha-equivalence classes of lambda-terms. This lifted function is characterised by the equations @@ -325,18 +328,20 @@ (Note that this means also the term-constructors for variables, applications and lambda are lifted to the quotient level.) This construction, of course, only works if alpha-equivalence is indeed an equivalence relation, and the lifted - definitions and theorems are respectful w.r.t.~alpha-equivalence. Accordingly, we + definitions and theorems are respectful w.r.t.~alpha-equivalence. For exmple, we will not be able to lift a bound-variable function, which can be defined for - raw terms, to alpha-equated terms - (since it does not respect alpha-equivalence). To sum up, every lifting of + raw terms. The reason is that this function does not respect alpha-equivalence. + To sum up, every lifting of theorems to the quotient level needs proofs of some respectfulness - properties. In the paper we show that we are able to automate these + properties (see \cite{Homeier05}). In the paper we show that we are able to + automate these proofs and therefore can establish a reasoning infrastructure for alpha-equated terms. The examples we have in mind where our reasoning infrastructure will be - immeasurably helpful is what is often referred to as Core-Haskell (see - Figure~\ref{corehas}). There terms include patterns which include a list of + helpful is the term language of System @{text "F\<^isub>C"}, also known as + Core-Haskell (see Figure~\ref{corehas}). This term language has patterns + which include lists of type- and term- variables (the arguments of constructors) all of which are bound in case expressions. One difficulty is that each of these variables come with a kind or type annotation. Representing such binders with single @@ -355,8 +360,45 @@ have the variable convention already built in. \begin{figure} - - \caption{Core Haskell.\label{corehas}} + \begin{boxedminipage}{\linewidth} + \begin{center} + \begin{tabular}{l} + Type Kinds\\ + @{text "\ ::= \ | \\<^isub>1 \ \\<^isub>2"}\\ + Coercion Kinds\\ + @{text "\ ::= \\<^isub>1 \ \\<^isub>2"}\\ + Types\\ + @{text "\ ::= a | T | \\<^isub>1 \\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\"}}$@{text "\<^sup>n"}\\ + @{text "| \a:\. \ "}\\ + ??? Type equality\\ + Coercion Types\\ + @{text "\ ::= a | C | S\<^isub>n"}$\;\overline{@{text "\"}}$@{text "\<^sup>n"}\\ + @{text "| \a:\. \"}\\ + ??? Coercion Type equality\\ + @{text "| sym \ | \\<^isub>1 \ \\<^isub>2 | left \ | right \ | \\<^isub>1 \ \\<^isub>2 "}\\ + @{text "| rightc \ | leftc \ | \\<^isub>1 \ \\<^isub>2"}\\ + Terms\\ + @{text "e ::= x | K | \a:\. e | \a:\. e | e \ | e \"}\\ + @{text "| \x:\.e | e\<^isub>1 e\<^isub>2"}\\ + @{text "| \ x:\ = e\<^isub>1 \ e\<^isub>2"}\\ + @{text "| \ e\<^isub>1 \"}$\;\overline{@{text "p \ e\<^isub>2"}}$\\ + @{text "| e \ \"}\\ + Patterns\\ + @{text "p ::= K"}$\;\overline{@{text "a:\"}}\;\overline{@{text "x:\"}}$\\ + Constants\\ + @{text C} coercion constant\\ + @{text T} value type constructor\\ + @{text "S\<^isub>n"} n-ary type function\\ + @{text K} data constructor\\ + Variables\\ + @{text a} type variable\\ + @{text x} term variable\\ + \end{tabular} + \end{center} + \end{boxedminipage} + \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as Core-Haskell, + according to \cite{CoreHaskell}. We only made an issential modification by + separating the grammars for type kinds and coercion types.\label{corehas}} \end{figure} *} @@ -455,7 +497,7 @@ given a free-variable function @{text "fv"} of type \mbox{@{text "\ \ atom set"}}, then @{text x} and @{text y} need to have the same set of free variables; moreover there must be a permutation @{text p} such that {\it - ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but + ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The @@ -463,7 +505,7 @@ % \begin{equation}\label{alphaset} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{@{term "(as, x) \gen R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\ + \multicolumn{2}{l}{@{term "(as, x) \gen R fv p (bs, y)"}\hspace{2mm}@{text "\"}\hspace{30mm}}\\[1mm] & @{term "fv(x) - as = fv(y) - bs"}\\ @{text "\"} & @{term "(fv(x) - as) \* p"}\\ @{text "\"} & @{text "(p \ x) R y"}\\ @@ -489,7 +531,7 @@ % \begin{equation}\label{alphalist} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{@{term "(as, x) \lst R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\[1mm] + \multicolumn{2}{l}{@{term "(as, x) \lst R fv p (bs, y)"}\hspace{2mm}@{text "\"}\hspace{30mm}}\\[1mm] & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\ \wedge & @{term "(fv(x) - set as) \* p"}\\ \wedge & @{text "(p \ x) R y"}\\ @@ -507,14 +549,13 @@ % \begin{equation}\label{alphares} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{@{term "(as, x) \res R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\[1mm] + \multicolumn{2}{l}{@{term "(as, x) \res R fv p (bs, y)"}\hspace{2mm}@{text "\"}\hspace{30mm}}\\[1mm] & @{term "fv(x) - as = fv(y) - bs"}\\ \wedge & @{term "(fv(x) - as) \* p"}\\ \wedge & @{text "(p \ x) R y"}\\ \end{array} \end{equation} - \begin{exmple}\rm It might be useful to consider some examples for how these definitions of alpha-equivalence pan out in practise. For this consider the case of abstracting a set of variables over types (as in type-schemes). @@ -526,20 +567,21 @@ \noindent Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and - \eqref{ex3}. It can be easily checked that @{text "({x,y}, x \ y)"} and - @{text "({y,x}, y \ x)"} are equal according to $\approx_{\textit{set}}$ and + \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \ y)"} and + @{text "({y, x}, y \ x)"} are equal according to $\approx_{\textit{set}}$ and $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then @{text "([x, y], x \ y)"} - $\not\approx_{\textit{list}}$ @{text "([y,x], x \ y)"} since there is no permutation + $\not\approx_{\textit{list}}$ @{text "([y, x], x \ y)"} since there is no permutation that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \ y"}} unchanged. Another example is - @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x,y}, x)"} which holds by + @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity permutation. However, if @{text "x \ y"}, then @{text "({x}, x)"} - $\not\approx_{\textit{set}}$ @{text "({x,y}, x)"} since there is no permutation + $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation that makes the - sets @{text "{x}"} and @{text "{x,y}"} equal (similarly for $\approx_{\textit{list}}$). - \end{exmple} + sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$). + It can also relatively easily be shown that all tree notions of alpha-equivalence + coincide, if we only abstract a single atom. % looks too ugly %\noindent @@ -569,22 +611,26 @@ %\end{proof} - In the rest of this section we are going to introduce a type- and term-constructor - for abstractions. For this we define (similarly for $\approx_{\textit{abs\_list}}$ - and $\approx_{\textit{abs\_res}}$) + In the rest of this section we are going to introduce a type- and term-constructors + for abstraction. For this we define % \begin{equation} @{term "abs_set (as, x) (bs, x) \ \p. alpha_gen (as, x) equal supp p (bs, x)"} \end{equation} \noindent - We can show that these relations are equivalence relations and equivariant - (we only show the $\approx_{\textit{abs\_set}}$-case). + (similarly for $\approx_{\textit{abs\_list}}$ + and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence + relations and equivariant. - \begin{lemma}\label{alphaeq} - $\approx_{\textit{abs\_set}}$ is an equivalence + \begin{lemma}\label{alphaeq} The relations + $\approx_{\textit{abs\_set}}$, + $\approx_{\textit{abs\_list}}$ + and $\approx_{\textit{abs\_res}}$ + are equivalence relations, and if @{term "abs_set (as, x) (bs, y)"} then also - @{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"}. + @{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"} (similarly for + the other two relations). \end{lemma} \begin{proof} @@ -595,29 +641,10 @@ calculations. \end{proof} - \noindent - We are also define the following two auxiliary functions taking a pair - as argument. - % - \begin{equation}\label{aux} - \begin{array}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "aux (as, x)"} & @{text "\"} & @{text "supp x - as"}\\ - @{text "aux_list (bs, x)"} & @{text "\"} & @{text "supp x - set bs"} - \end{array} - \end{equation} - \noindent - The point of these two functions is that they are preserved under - alpha-equivalence, that means for instance - % - \begin{equation}\label{auxpreserved} - @{term "abs_set (as, x) (bs, y)"} \;\;\text{implies}\;\; - @{term "aux (as, x) = aux (bs, y)"} - \end{equation} - - Lemma \ref{alphaeq} allows us to use our quotient package and introduce + This lemma allows us to use our quotient package and introduce new types @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} - representing the alpha-equivalence classes. Elements in these types + representing alpha-equivalence classes of pairs. The elements in these types we will, respectively, write as: \begin{center} @@ -627,31 +654,71 @@ \end{center} \noindent - By definition we have + indicating that a set or list is abstracted in @{text x}. We will call the types + \emph{abstraction types} and their elements \emph{abstractions}. The important + property we need is a characterisation for the support of abstractions, namely + \begin{thm}[Support of Abstractions]\label{suppabs} + Assuming @{text x} has finite support, then \begin{center} - @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;iff\; - @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} + \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)[no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[no_vars]} + \end{tabular} \end{center} - + \end{thm} \noindent - The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and - $\approx_{\textit{abs\_res}}$) will be crucial below: + We will only show in the rest of the section the first equation, as the others + follow similar arguments. By definition of the abstraction type @{text "abs_set"} + we have + % + \begin{equation}\label{abseqiff} + @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\text{if and only if}\; + @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} + \end{equation} + + \noindent + With this, we can show the following lemma about swapping two atoms (the permutation + operation for abstractions is the one lifted for pairs).\footnote{metion this in the nominal + logic section} \begin{lemma} @{thm[mode=IfThen] abs_swap1(1)[no_vars]} \end{lemma} \begin{proof} - This lemma is straightforward by observing that the assumptions give us + By using \eqref{abseqiff}, this lemma is straightforward when observing that + the assumptions give us @{term "(a \ b) \ (supp x - bs) = (supp x - bs)"} and that @{text supp} - is equivariant. + and set difference are equivariant. \end{proof} + \noindent + This lemma gives us + % + \begin{equation}\label{halfone} + @{thm abs_supports(1)[no_vars]} + \end{equation} + + \noindent + which with \ref{} gives us one half of Thm~\ref{suppabs}. The other half is + a bit more involved. We first define an auxiliary function + % + \begin{center} + @{thm supp_res.simps[THEN eq_reflection, no_vars]} + \end{center} + + \begin{lemma} $supp ([as]set. x) = supp x - as$ \end{lemma} + + \noindent + The point of these general lemmas about pairs is that we can define and prove properties + about them conveninently on the Isabelle level, and in addition can use them in what + follows next when we have to deal with specific instances of term-specification. *} section {* Alpha-Equivalence and Free Variables *} diff -r 7b3dd407f6b3 -r 51bc795b81fd Paper/document/root.bib --- a/Paper/document/root.bib Sun Mar 28 22:54:38 2010 +0200 +++ b/Paper/document/root.bib Mon Mar 29 00:30:20 2010 +0200 @@ -1,3 +1,11 @@ + +@InProceedings{CoreHaskell, + author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly}, + title = {{S}ystem {F} with {T}ype {E}quality {C}oercions}, + booktitle = {Proc of TLDI}, + pages = {??}, + year = {2007} +} @inproceedings{cheney05, author = {J.~Cheney}, diff -r 7b3dd407f6b3 -r 51bc795b81fd Paper/document/root.tex --- a/Paper/document/root.tex Sun Mar 28 22:54:38 2010 +0200 +++ b/Paper/document/root.tex Mon Mar 29 00:30:20 2010 +0200 @@ -9,6 +9,7 @@ \usepackage{pdfsetup} \usepackage{ot1patch} \usepackage{times} +\usepackage{boxedminipage} \urlstyle{rm} \isabellestyle{it} @@ -21,7 +22,7 @@ \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} \renewcommand{\isasymequiv}{$\dn$} -\renewcommand{\isasymiota}{} +%%\renewcommand{\isasymiota}{} \renewcommand{\isasymemptyset}{$\varnothing$} \newcommand{\isasymnotapprox}{$\not\approx$} \newcommand{\isasymLET}{$\mathtt{let}$} @@ -31,6 +32,8 @@ \newcommand{\isasymBIND}{$\mathtt{bind}$} \newcommand{\isasymANIL}{$\mathtt{anil}$} \newcommand{\isasymACONS}{$\mathtt{acons}$} +\newcommand{\isasymCASE}{$\mathtt{case}$} +\newcommand{\isasymOF}{$\mathtt{of}$} \newcommand{\LET}{\;\mathtt{let}\;} \newcommand{\IN}{\;\mathtt{in}\;} \newcommand{\END}{\;\mathtt{end}\;} @@ -69,7 +72,7 @@ poorly supported with single binders, such as lambda-abstractions. Our extension includes novel definitions of alpha-equivalence and establishes automatically the reasoning infrastructure for alpha-equated terms. We -also provide strong induction principles that have the usual variable +also prove strong induction principles that have the usual variable convention already built in. \end{abstract}