# HG changeset patch # User Cezary Kaliszyk # Date 1268955358 -3600 # Node ID 48d08d99b94899a7c09ef8ceae68f081fe4f5100 # Parent 770a66131bd3569caffa3b6d9addb3ffdec176f0# Parent 24dbe785f2e5ca97c164895d5340235bdf7aff13 merge 1 diff -r 24dbe785f2e5 -r 48d08d99b948 Nominal/Test.thy --- a/Nominal/Test.thy Fri Mar 19 00:35:20 2010 +0100 +++ b/Nominal/Test.thy Fri Mar 19 00:35:58 2010 +0100 @@ -62,7 +62,7 @@ fixes c::"'a::fs" assumes a1: "\name c. P c (Vr name)" and a2: "\lm1 lm2 c. \\d. P d lm1; \d. P d lm2\ \ P c (Ap lm1 lm2)" - and a3: "\name lm c. \\d. P d lm\ \ P c (Lm name lm)" + and a3: "\name lm c. \atom name \ c; \d. P d lm\ \ P c (Lm name lm)" shows "P c lm" proof - have "\p. P c (p \ lm)" @@ -87,6 +87,7 @@ apply(simp add: fresh_Pair) apply(simp) apply(rule a3) + apply(simp add: fresh_Pair) apply(drule_tac x="((p \ name) \ new) + p" in meta_spec) apply(simp) apply(simp add: fresh_def) @@ -99,6 +100,38 @@ qed +lemma + fixes c::"'a::fs" + assumes a1: "\name c. P c (Vr name)" + and a2: "\lm1 lm2 c. \\d. P d lm1; \d. P d lm2\ \ P c (Ap lm1 lm2)" + and a3: "\name lm c. \atom name \ c; \d. P d lm\ \ P c (Lm name lm)" + shows "P c lm" +proof - + have "\p. P c (p \ lm)" + apply(induct lm arbitrary: c rule: lm.induct) + apply(simp only: lm.perm) + apply(rule a1) + apply(simp only: lm.perm) + apply(rule a2) + apply(blast)[1] + apply(assumption) + thm at_set_avoiding + apply(subgoal_tac "\q. (q \ {p \ atom name}) \* c \ supp (p \ Lm name lm) \* q") + apply(erule exE) + apply(rule_tac t="p \ Lm name lm" and + s="q \ p \ Lm name lm" in subst) + defer + apply(simp add: lm.perm) + apply(rule a3) + apply(simp add: eqvts fresh_star_def) + apply(drule_tac x="q + p" in meta_spec) + apply(simp) + sorry + then have "P c (0 \ lm)" by blast + then show "P c lm" by simp +qed + + nominal_datatype lam = VAR "name" | APP "lam" "lam" @@ -418,14 +451,6 @@ ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} -lemma supports_subset: - fixes S1 S2 :: "atom set" - assumes a: "S1 supports x" - and b: "S1 \ S2" - shows "S2 supports x" - using a b - by (auto simp add: supports_def) - lemma finite_fv_t_tyS: fixes T::"t" and S::"tyS" @@ -473,6 +498,10 @@ (* example 1 from Terms.thy *) + + + + nominal_datatype trm1 = Vr1 "name" | Ap1 "trm1" "trm1" @@ -622,6 +651,28 @@ thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct +lemma +"fv_mexp j = supp j \ fv_body k = supp k \ +(fv_defn c = supp c \ fv_cbinders c = {a. infinite {b. \alpha_cbinders ((a \ b) \ c) c}}) \ +fv_sexp d = supp d \ fv_sbody e = supp e \ +(fv_spec l = supp l \ fv_Cbinders l = {a. infinite {b. \alpha_Cbinders ((a \ b) \ l) l}}) \ +fv_tyty g = supp g \ fv_path h = supp h \ fv_trmtrm i = supp i" +apply(induct rule: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct) +apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv) +apply(simp_all only: supp_Abs[symmetric]) +apply(simp_all (no_asm) only: supp_def) +apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm) +apply(simp_all only: permute_ABS) +apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff Abs_eq_iff) +apply(simp_all only: alpha_gen) +apply(simp_all only: eqvts[symmetric] supp_Pair) +apply(simp_all only: eqvts Pair_eq) +apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) +apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) +apply(simp_all only: de_Morgan_conj[symmetric]) +apply simp_all +done + (* example 3 from Peter Sewell's bestiary *) nominal_datatype exp = diff -r 24dbe785f2e5 -r 48d08d99b948 Paper/Paper.thy --- a/Paper/Paper.thy Fri Mar 19 00:35:20 2010 +0100 +++ b/Paper/Paper.thy Fri Mar 19 00:35:58 2010 +0100 @@ -15,17 +15,148 @@ section {* Introduction *} text {* + So far, Nominal Isabelle provides a mechanism for constructing + automatically alpha-equated terms such as - It has not yet fared so well in the POPLmark challenge - as the second part contain a formalisation of records - where ... + \begin{center} + $t ::= x \mid t\;t \mid \lambda x. t$ + \end{center} + + \noindent + For such terms it derives automatically a reasoning + infrastructure, which has been used in formalisations of an equivalence + checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed + Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency + \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result + for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been + used by Pollack for formalisations in the locally-nameless approach to + binding \cite{SatoPollack10}. + + However, Nominal Isabelle fared less well in a formalisation of + the algorithm W \cite{UrbanNipkow09}, where types and type-schemes + are of the form + + \begin{center} + \begin{tabular}{l} + $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$ + \end{tabular} + \end{center} + + \noindent + and the quantification abstracts over a finite (possibly empty) set of type variables. + While it is possible to formalise such abstractions by iterating single bindings, + it leads to a very clumsy formalisation of W. This need of iterating single binders + for representing multiple binders is also the reason why Nominal Isabelle and other + theorem provers have not fared extremely well with the more advanced tasks + in the POPLmark challenge \cite{challenge05}, because also there one would be able + to aviod clumsy reasoning if there were a mechanisms for abstracting several variables + at once. + + To see this, let us point out some interesting properties of binders abstracting multiple + variables. First, in the case of type-schemes, we do not like to make a distinction + about the order of the bound variables. Therefore we would like to regard the following two + type-schemes as alpha-equivalent + + \begin{center} + $\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ + \end{center} + + \noindent + but the following two should \emph{not} be alpha-equivalent + + \begin{center} + $\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ + \end{center} + + \noindent + assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as + alpha-equivalent, if they differ only on \emph{vacuous} binders, such as + + \begin{center} + $\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ + \end{center} + + \noindent + In this paper we will give a general abstraction mechanism and associated + notion of alpha-equivalence that can be used to faithfully represent + type-schemes in Nominal Isabelle. The difficulty of finding the right notion + for alpha-equivalence in this case can be appreciated by considering that the + definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). + + - The difficulty can be appreciated by considering that the - definition given by Leroy in \cite{Leroy92} is incorrect (it omits a - side-condition). + However, the notion of alpha-equivalence that is preserved by vacuous binders is not + alway wanted. For example in terms like + + \begin{center} + $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$ + \end{center} + + \noindent + we might not care in which order the assignments $x = 3$ and $y = 2$ are + given, but it would be unusual to regard the above term as alpha-equivalent + with + + \begin{center} + $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,\backslash\,y \END$ + \end{center} + + \noindent + Therefore we will also provide a separate abstraction mechanism for cases + in which the order of binders does not matter, but the ``cardinality'' of the + binders has to be the same. + + However, we found that this is still not sufficient for covering language + constructs frequently occuring in programming language research. For example + in $\mathtt{let}$s involving patterns + + \begin{center} + $\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$ + \end{center} + + \noindent + we want to bind all variables from the pattern (there might be an arbitrary + number of them) inside the body of the $\mathtt{let}$, but we also care about + the order of these variables, since we do not want to identify the above term + with - Examples: type-schemes, Spi-calculus + \begin{center} + $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$ + \end{center} + + \noindent + As a result, we provide three general abstraction mechanisms for multiple binders + and allow the user to chose which one is intended when formalising a + programming language calculus. + + By providing these general abstraction mechanisms, however, we have to work around + a problem that has been pointed out by Pottier in \cite{Pottier06}: in + $\mathtt{let}$-constructs of the form + + \begin{center} + $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$ + \end{center} + \noindent + which bind all the $x_i$ in $s$, we might not care about the order in + which the $x_i = t_i$ are given, but we do care about the information that there are + as many $x_i$ as there are $t_i$. We lose this information if we represent the + $\mathtt{let}$-constructor as something like + + \begin{center} + $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ + \end{center} + + \noindent + where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes bound + in $s$. In this representation we need additional predicates to ensure + that the two lists are of equal length. This can result into very + unintelligible reasoning (see for example~\cite{BengtsonParow09}). + + + + + Contributions: We provide definitions for when terms involving general bindings are alpha-equivelent. @@ -51,19 +182,21 @@ %\end{pspicture} %\end{center} - + quotient package \cite{Homeier05} *} section {* A Short Review of the Nominal Logic Work *} text {* At its core, Nominal Isabelle is based on the nominal logic work by Pitts - \cite{Pitts03}. Two central notions in this work are sorted atoms and - permutations of atoms. The sorted atoms represent different - kinds of variables, such as term- and type-variables in Core-Haskell, and it - is assumed that there is an infinite supply of atoms for each sort. - However, in order to simplify the description of our work, we shall - assume in this paper that there is only a single sort of atoms. + \cite{Pitts03}. The implementation of this work are described in + \cite{HuffmanUrban10}, which we review here briefly to aid the description + of what follows in the next sections. Two central notions in the nominal + logic work are sorted atoms and permutations of atoms. The sorted atoms + represent different kinds of variables, such as term- and type-variables in + Core-Haskell, and it is assumed that there is an infinite supply of atoms + for each sort. However, in order to simplify the description of our work, we + shall assume in this paper that there is only a single sort of atoms. Permutations are bijective functions from atoms to atoms that are the identity everywhere except on a finite number of atoms. There is a @@ -96,38 +229,72 @@ @{thm[display,indent=5] fresh_def[no_vars]} \noindent - We also use for sets of atoms the abbreviation @{thm fresh_star_def[no_vars]}. + We also use for sets of atoms the abbreviation + @{thm (lhs) fresh_star_def[no_vars]} defined as + @{thm (rhs) fresh_star_def[no_vars]}. A striking consequence of these definitions is that we can prove without knowing anything about the structure of @{term x} that swapping two fresh atoms, say @{text a} and @{text b}, leave @{text x} unchanged. - \begin{Property} + \begin{property} @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} - \end{Property} + \end{property} - \begin{Property} + \noindent + For a proof see \cite{HuffmanUrban10}. + + \begin{property} @{thm[mode=IfThen] at_set_avoiding[no_vars]} - \end{Property} + \end{property} *} section {* Abstractions *} +text {* + General notion of alpha-equivalence (depends on a free-variable + function and a relation). +*} + section {* Alpha-Equivalence and Free Variables *} +text {* + Restrictions + + \begin{itemize} + \item non-emptyness + \item positive datatype definitions + \item finitely supported abstractions + \item respectfulness of the bn-functions\bigskip + \item binders can only have a ``single scope'' + \end{itemize} +*} + section {* Examples *} +section {* Adequacy *} + +section {* Related Work *} + section {* Conclusion *} text {* + Complication when the single scopedness restriction is lifted (two + overlapping permutations) +*} + +text {* + + TODO: function definitions: + \medskip \noindent {\bf Acknowledgements:} We are very grateful to Andrew Pitts for the many discussions about Nominal Isabelle. We thank Peter Sewell for making the informal notes \cite{SewellBestiary} available to us and - also explaining some of the finer points of the OTT-tool. + also for explaining some of the finer points of the OTT-tool. *} diff -r 24dbe785f2e5 -r 48d08d99b948 Paper/document/root.bib --- a/Paper/document/root.bib Fri Mar 19 00:35:20 2010 +0100 +++ b/Paper/document/root.bib Fri Mar 19 00:35:58 2010 +0100 @@ -1,7 +1,30 @@ +@InProceedings{Homeier05, + author = {P.~Homeier}, + title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients}, + booktitle = {Proc.~of the 18th International Conference on Theorem + Proving in Higher Order Logics (TPHOLs)}, + pages = {130--146}, + year = {2005}, + volume = {3603}, + series = {LNCS} +} + +@INPROCEEDINGS{Pottier06, + author = {F.~Pottier}, + title = {{A}n {O}verview of {C$\alpha$ml}}, + year = {2006}, + booktitle = {ACM Workshop on ML}, + pages = {27--52}, + volume = {148}, + number = {2}, + series = {ENTCS} +} + @Unpublished{HuffmanUrban10, author = {B.~Huffman and C.~Urban}, title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, - note = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf}, + note = {To appear at ITP 2010}, + annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf}, year = {2010} } @@ -19,6 +42,21 @@ note = {Personal communication.} } +@InProceedings{challenge05, + author = {B.~E.~Aydemir and A.~Bohannon and M.~Fairbairn and + J.~N.~Foster and B.~C.~Pierce and P.~Sewell and + D.~Vytiniotis and G.~Washburn and S.~Weirich and + S.~Zdancewic}, + title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark + {C}hallenge}, + booktitle = {Proc.~of the 18th International Conference on Theorem Proving in Higher-Order + Logics (TPHOLs)}, + pages = {50--65}, + year = {2005}, + volume = {3603}, + series = {LNCS} +} + @Unpublished{SatoPollack10, author = {M.~Sato and R.~Pollack}, title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, diff -r 24dbe785f2e5 -r 48d08d99b948 Paper/document/root.tex --- a/Paper/document/root.tex Fri Mar 19 00:35:20 2010 +0100 +++ b/Paper/document/root.tex Fri Mar 19 00:35:58 2010 +0100 @@ -6,21 +6,28 @@ \usepackage{tikz} \usepackage{pgf} \usepackage{pdfsetup} +\usepackage{ot1patch} \urlstyle{rm} \isabellestyle{it} +\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}} +\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}} \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} \renewcommand{\isasymequiv}{$\dn$} \renewcommand{\isasymiota}{} \renewcommand{\isasymemptyset}{$\varnothing$} +\newcommand{\LET}{\;\mathtt{let}\;} +\newcommand{\IN}{\;\mathtt{in}\;} +\newcommand{\END}{\;\mathtt{end}\;} +\newcommand{\AND}{\;\mathtt{and}\;} %----------------- theorem definitions ---------- -\newtheorem{Property}{Theorem}[section] +\newtheorem{property}{Property}[section] \newtheorem{Theorem}{Theorem}[section] \newtheorem{Definition}[Theorem]{Definition} \newtheorem{Example}{\it Example}[section] @@ -38,16 +45,16 @@ \maketitle \begin{abstract} -Nominal Isabelle is a definitional extension of the Isabelle/HOL -theorem prover. It provides a proving infrastructure for -conveninet reasoning about programming language calculi. In this paper -we present an extension of Nominal Isabelle for dealing with general binding -structures. Such structures are ubiquitous in programming language research -and only very poorly handled by the well-known single abstraction in the -lambda-calculus. We give definitions for alpha-equivalence and establish -the reasoning structure for alpha-equated terms. For example we provide -a strong induction principle that has the variable convention already -built in. +Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem +prover. It provides a proving infrastructure for convenient reasoning about +programming language calculi. In this paper we present an extension of Nominal +Isabelle in order to deal with general binding structures. Such binding structures +are ubiquitous in programming language research and only very poorly supported +with single binders, as for example found in the lambda-calculus. For our +extension we introduce novel definitions of alpha-equivalence and establish +automatically the reasoning infrastructure for alpha-equated terms. This +includes a strong induction principle which has the variable convention +already built in. \end{abstract}