# HG changeset patch # User Christian Urban # Date 1269948192 -7200 # Node ID 40f13b52b107d459e5927c3f2b76e52fe8507260 # Parent 55cb244b020cd985d74d6d8e28f4f255334f614d# Parent 88b33de74e61f273c23ea5b13cb4162bac49f426 merged diff -r 88b33de74e61 -r 40f13b52b107 Paper/Paper.thy --- a/Paper/Paper.thy Tue Mar 30 12:31:28 2010 +0200 +++ b/Paper/Paper.thy Tue Mar 30 13:23:12 2010 +0200 @@ -148,7 +148,7 @@ \noindent As a result, we provide three general binding mechanisms each of which binds multiple variables at once, and let the user chose which one is intended - when formalising a programming language calculus. + when formalising a term-calculus. By providing these general binding mechanisms, however, we have to work around a problem that has been pointed out by Pottier \cite{Pottier06} and @@ -342,7 +342,7 @@ The examples we have in mind where our reasoning infrastructure will be helpful includes the term language of System @{text "F\<^isub>C"}, also known as Core-Haskell (see Figure~\ref{corehas}). This term language - involves patterns that have lists of type-, coercion- and term-variables + involves patterns that have lists of type-, coercion- and term-variables, all of which are bound in @{text "\"}-expressions. One difficulty is that each of these variables come with a kind or type annotation. Representing such binders with single binders and reasoning @@ -395,7 +395,7 @@ \caption{The term-language of System @{text "F\<^isub>C"} \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this version of the term-language we made a modification by separating the - grammars for type and coercion kinds, as well as for types and coercion + grammars for type kinds and coercion kinds, as well as for types and coercion types. For this paper the interesting term-constructor is @{text "\"}, which binds multiple type-, coercion- and term-variables.\label{corehas}} \end{figure} @@ -409,13 +409,14 @@ \cite{HuffmanUrban10} (including proofs). We shall briefly review this work to aid the description of what follows. - Two central notions in the nominal - logic work are sorted atoms and sort-respecting permutations of atoms. The - sorts can be used to represent different kinds of variables, such as the - term-, coercion- 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, we shall assume in what follows that there is only one sort of - atoms. + Two central notions in the nominal logic work are sorted atoms and + sort-respecting permutations of atoms. We will use the variables @{text "a, + b, c, \"} to stand for atoms and @{text "p, q, \"} to stand for + permutations. The sorts of atoms can be used to represent different kinds of + variables, such as the term-, coercion- 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, we shall assume in what + follows that there is only one 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 @@ -486,19 +487,18 @@ swapping two fresh atoms, say @{text a} and @{text b}, leave @{text x} unchanged. - \begin{property} + \begin{property}\label{swapfreshfresh} @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} \end{property} - \noindent - While often the support of an object can be easily described, for - example\\[-6mm] + While often the support of an object can be relatively easily + described, for example\\[-6mm] % \begin{eqnarray} @{term "supp a"} & = & @{term "{a}"}\\ @{term "supp (x, y)"} & = & @{term "supp x \ supp y"}\\ @{term "supp []"} & = & @{term "{}"}\\ - @{term "supp (x#xs)"} & = & @{term "supp (x, xs)"}\\ + @{term "supp (x#xs)"} & = & @{term "supp x \ supp xs"}\\ @{text "supp (f x)"} & @{text "\"} & @{term "supp (f, x)"}\label{suppfun}\\ @{term "supp b"} & = & @{term "{}"}\\ @{term "supp p"} & = & @{term "{a. p \ a \ a}"} @@ -507,7 +507,7 @@ \noindent in some cases it can be difficult to establish the support precisely, and only give an approximation (see the case for function applications - above). Such approximations can be made precise with the notion + above). Such approximations can be calculated with the notion \emph{supports}, defined as follows \begin{defn} @@ -525,21 +525,57 @@ Another important notion in the nominal logic work is \emph{equivariance}. For a function @{text f}, say of type @{text "\ \ \"}, to be equivariant - requires that every permutation leaves @{text f} unchanged, or equivalently that - a permutation applied to the application @{text "f x"} can be moved to its - arguments. That is + requires that every permutation leaves @{text f} unchanged, that is + % + \begin{equation}\label{equivariancedef} + @{term "\p. p \ f = f"} + \end{equation} + + \noindent or equivalently that a permutation applied to the application + @{text "f x"} can be moved to the argument @{text x}. That means we have for + all permutations @{text p} % \begin{equation}\label{equivariance} - @{text "\p. p \ f = f"} \;\;if and only if\;\; - @{text "\p. p \ (f x) = f (p \ x)"} + @{text "p \ f = f"} \;\;\;\textit{if and only if}\;\;\; + @{text "p \ (f x) = f (p \ x)"} \end{equation} \noindent - From the first equation and the definition of support shown in \eqref{suppdef}, - we can be easily deduce that an equivariant function has empty support. + From equation \eqref{equivariancedef} and the definition of support shown in + \eqref{suppdef}, we can be easily deduce that an equivariant function has + empty support. + + Finally, the nominal logic work provides us with elegant means to rename + binders. While in the older version of Nominal Isabelle, we used extensively + Property~\ref{swapfreshfresh} for renaming single binders, this property + proved unwieldy for dealing with multiple binders. For this the following + generalisations turned out to be easier to use. + + \begin{property}\label{supppermeq} + @{thm[mode=IfThen] supp_perm_eq[no_vars]} + \end{property} - In the next section we use @{text "supp"} and permutations for characterising - alpha-equivalence in the presence of multiple binders. + \begin{property} + For a finite set @{text xs} and a finitely supported @{text x} with + @{term "xs \* x"} and also a finitely supported @{text c}, there + exists a permutation @{text p} such that @{term "(p \ xs) \* c"} and + @{term "supp x \* p"}. + \end{property} + + \noindent + The idea behind the second property is that given a finite set @{text xs} + of binders (being bound in @{text x} which is ensured by the + assumption @{term "xs \* x"}), then there exists a permutation @{text p} such that + the renamed binders @{term "p \ xs"} avoid the @{text c} (which can be arbitrarily chosen + as long as it is finitely supported) and also does not affect anything + in the support of @{text x} (that is @{term "supp x \* p"}). The last + fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders + in @{text x}, because @{term "p \ x = x"}. + + All properties given in this section are formalised in Isabelle/HOL and also + most of them are described with proofs in \cite{HuffmanUrban10}. In the next section + we make extensively use of the properties of @{text "supp"} and permutations + for characterising alpha-equivalence in the presence of multiple binders. *}