# HG changeset patch # User Christian Urban # Date 1330491366 0 # Node ID 4bad521e3b9e2e9a265e2a9ce06be0d059ad453a # Parent d13ac9f4e77350b7b642a0588249b62aff26f5d2 more on the lmcs paper diff -r d13ac9f4e773 -r 4bad521e3b9e LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Wed Feb 29 03:13:45 2012 +0000 +++ b/LMCS-Paper/Paper.thy Wed Feb 29 04:56:06 2012 +0000 @@ -128,7 +128,8 @@ definition is to get access to the bound variables and the type-part of a type-scheme @{text S}, though in general we will only get access to some variables and some type @{text T} that are - ``alpha-equivalent'' to @{text S}---it is an unbinding \emph{relation}. Still, with this + ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation, not a function. + Still, with this definition in place we can formally define when a type is an instance of a type-scheme as \[ @@ -139,13 +140,13 @@ meaning there exists a list of variables @{text xs} and a type @{text T'} to which the type-scheme @{text S} unbinds, and there exists a substitution whose domain is @{text xs} (seen as set) such that @{text "\(T') = T"}. - The pain with this definition is that we cannot follow the usual proofs + The problem with this definition is that we cannot follow the usual proofs that are by induction on the type-part of the type-scheme (since it is under - an existential quantifier). The representation of type-schemes by iterating single binders + an existential quantifier). The representation of type-schemes using iterations of single binders prevents us from directly ``unbinding'' the bound variables and the type-part of a type-scheme. The purpose of this paper is to introduce general binders, which - allow us to represent type-schemes following closely informal practice and as - a result solve this problem. + allow us to represent type-schemes so that they can bind multiple variables at once + and as a result solve this problem. The need of iterating single binders is also one reason why Nominal Isabelle and similar theorem provers that only provide mechanisms for binding single variables have not fared extremely well with @@ -160,7 +161,7 @@ the second pair should \emph{not} be alpha-equivalent: \begin{equation}\label{ex1} - @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. y \ x"}\hspace{10mm} + @{text "\{x, y}. x \ y \\<^isub>\ \{x, y}. y \ x"}\hspace{10mm} @{text "\{x, y}. x \ y \\<^isub>\ \{z}. z \ z"} \end{equation}\smallskip @@ -421,7 +422,7 @@ \noindent {\bf Contributions:} We provide three new definitions for when terms involving general binders are alpha-equivalent. These definitions are - inspired by earlier work of Pitts \cite{Pitts04}. By means of automatically-generated + inspired by earlier work of Pitts \cite{Pitts04}. By means of automati\-cally-generated proofs, we establish a reasoning infrastructure for alpha-equated terms, including properties about support, freshness and equality conditions for alpha-equated terms. We are also able to automatically derive strong @@ -519,7 +520,7 @@ \end{tabular} & \begin{tabular}{@ {}l@ {}} @{thm permute_perm_def[where p="\" and q="\'", no_vars, THEN eq_reflection]}\\ - @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ + @{thm permute_set_def[where p="\", no_vars, THEN eq_reflection]}\\ @{text "\ \ f \ \x. \ \ (f (- \ \ x))"}\\ @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]} \end{tabular} @@ -618,34 +619,33 @@ it is required that every permutation leaves @{text f} unchanged, that is \begin{equation}\label{equivariancedef} - @{term "\\. \ \ f = f"} + @{term "\\. \ \ f = f"}\;. \end{equation}\smallskip \noindent If a function is of type @{text "\ \ \"}, this definition is equivalent to the fact that a permutation applied to the application @{text "f x"} can be moved to the argument @{text x}. That means for - functions @{text f} of type @{text "\ \ \"}, we have for all permutations @{text "\"}: + such functions, we have for all permutations @{text "\"}: \begin{equation}\label{equivariance} @{text "\ \ f = f"} \;\;\;\;\textit{if and only if}\;\;\;\; - @{text "\x. \ \ (f x) = f (\ \ x)"} + @{text "\x. \ \ (f x) = f (\ \ x)"}\;. \end{equation}\smallskip \noindent There is also a similar property for relations, which are in HOL functions of type @{text "\ \ \ \ bool"}. - Suppose a relation @{text R}, then - that for all permutations @{text \}: + Suppose a relation @{text R}, then for all permutations @{text \}: \[ @{text "\ \ R = R"} \;\;\;\;\textit{if and only if}\;\;\;\; - @{text "\x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\ \ x) R (\ \ y)"} + @{text "\x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\ \ x) R (\ \ y)"}\;. \]\smallskip \noindent Note that from property \eqref{equivariancedef} and the definition of @{text supp}, we - can easily deduce that equivariant functions have empty support. + can easily deduce that for a function being equivariant is equivalent to having empty support. Using freshness, the nominal logic work provides us with general means for renaming binders. @@ -1043,8 +1043,9 @@ recursive arguments need to satisfy a `positivity' restriction, which ensures that the type has a set-theoretic semantics (see \cite{Berghofer99}). If the types are polymorphic, we require the - type variables are of finitely supported type. - The labels annotated on the types are optional. Their + type variables stand for types that are finitely supported and over which + a permutation operation is defined. + The labels @{text "label"}$_{1..l}$ annotated on the types are optional. Their purpose is to be used in the (possibly empty) list of \emph{binding clauses}, which indicate the binders and their scope in a term-constructor. They come in three \emph{modes}: @@ -1238,7 +1239,9 @@ out different atoms to become bound, respectively be free, in @{text "p"}. (Since the Ott-tool does not derive a reasoning infrastructure for alpha-equated terms with deep binders, it can permit such specifications.) - + For convenience we exlude such specifications even if @{text "bn\<^isub>1"} and + @{text "bn\<^isub>2"} are the same binding functions, which would otherwise be harmless. + We also need to restrict the form of the binding functions in order to ensure the @{text "bn"}-functions can be defined for alpha-equated terms. The main restriction is that we cannot return an atom in a binding