(*<*)+
−
theory Paper+
−
imports "../Nominal/Test" "LaTeXsugar"+
−
begin+
−
+
−
notation (latex output)+
−
  swap ("'(_ _')" [1000, 1000] 1000) and+
−
  fresh ("_ # _" [51, 51] 50) and+
−
  fresh_star ("_ #* _" [51, 51] 50) and+
−
  supp ("supp _" [78] 73) and+
−
  uminus ("-_" [78] 73) and+
−
  If  ("if _ then _ else _" 10)+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
  So far, Nominal Isabelle provides a mechanism for constructing+
−
  alpha-equated terms such as+
−
+
−
  \begin{center}+
−
  $t ::= x \mid t\;t \mid \lambda x. t$+
−
  \end{center}+
−
+
−
  \noindent+
−
  where free and bound variables have names.+
−
  For such terms Nominal Isabelle derives automatically a reasoning+
−
  infrastructure, which has been used successfully 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 has 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 binds at once a finite (possibly empty) set of type-variables.+
−
  While it is possible to implement this kind of more general binders by iterating single binders, +
−
  this leads to a rather clumsy formalisation of W. The need of iterating single binders +
−
  is also one reason why Nominal Isabelle and similar +
−
  theorem provers have not fared extremely well with the more advanced tasks +
−
  in the POPLmark challenge \cite{challenge05}, because also there one would like +
−
  to bind multiple variables at once.+
−
+
−
  Binding multiple variables has interesting properties that are not+
−
  captured by iterating single binders. 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+
−
  where $z$ does not occur freely in the type.+
−
  In this paper we will give a general binding mechanism and associated+
−
  notion of alpha-equivalence that can be used to faithfully represent+
−
  this kind of binding 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).+
−
+
−
  However, the notion of alpha-equivalence that is preserved by vacuous binders is not+
−
  alway wanted. For example in terms like+
−
+
−
  \begin{equation}\label{one}+
−
  \LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END+
−
  \end{equation}+
−
+
−
  \noindent+
−
  we might not care in which order the assignments $x = 3$ and $y = 2$ are+
−
  given, but it would be unusual to regard \eqref{one} 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 binding mechanism for cases +
−
  in which the order of binders does not matter, but the ``cardinality'' of the +
−
  binders has to agree.+
−
+
−
  However, we found that this is still not sufficient for dealing with language +
−
  constructs frequently occurring in programming language research. For example +
−
  in $\mathtt{let}$s involving patterns +
−
+
−
  \begin{equation}\label{two}+
−
  \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END+
−
  \end{equation}+
−
+
−
  \noindent+
−
  we want to bind all variables from the pattern inside the body of the+
−
  $\mathtt{let}$, but we also care about the order of these variables, since+
−
  we do not want to identify \eqref{two} with+
−
+
−
  \begin{center}+
−
  $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$+
−
  \end{center}+
−
+
−
  \noindent+
−
  As a result, we provide three general binding mechanisms each of which binds multiple+
−
  variables at once, and we let the user chose which one is intended when formalising a+
−
  programming language calculus.+
−
+
−
  By providing these general binding 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 notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become +
−
  bound in $s$. In this representation we need additional predicates about terms +
−
  to ensure that the two lists are of equal length. This can result into very +
−
  unintelligible reasoning (see for example~\cite{BengtsonParow09}). +
−
  To avoid this, we will allow to specify $\mathtt{let}$s +
−
  as follows+
−
+
−
  \begin{center}+
−
  \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}+
−
  $trm$ & $::=$  & \ldots\\ +
−
        & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm]+
−
  $assn$ & $::=$  & $\mathtt{anil}$\\+
−
         & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  where $assn$ is an auxiliary type representing a list of assignments+
−
  and $bn$ an auxiliary function identifying the variables to be bound by +
−
  the $\mathtt{let}$. This function can be defined as +
−
+
−
  \begin{center}+
−
  $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ +
−
  \end{center}+
−
  +
−
  \noindent+
−
  The scope of the binding is indicated by labels given to the types, for example+
−
  $s\!::\!trm$, and a binding clause $\mathtt{bind}\;bn\,(a) \IN s$.+
−
  This style of specifying terms and bindings is heavily +
−
  inspired by the syntax of the Ott-tool \cite{ott-jfp}.+
−
+
−
  However, we will not be able to deal with all specifications that are+
−
  allowed by Ott. One reason is that we establish the reasoning infrastructure+
−
  for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of+
−
  its specifications a reasoning infrastructure in Isabelle for+
−
  \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms+
−
  and the concrete terms produced by Ott use names for the bound variables,+
−
  there is a key difference: working with alpha-equated terms means that the+
−
  two type-schemes with $x$, $y$ and $z$ being distinct+
−
+
−
  \begin{center}+
−
  $\forall \{x\}. x \rightarrow y  \;=\; \forall \{x, z\}. x \rightarrow y$ +
−
  \end{center}+
−
  +
−
  \noindent+
−
  are not just alpha-equal, but actually equal (note the ``=''-sign). 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 concrete+
−
  terms. The fundamental reason is that the HOL-logic underlying+
−
  Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast replacing +
−
  ``alpha-equals-by-alpha-equals'' in a term calculus requires a lot of extra reasoning work.+
−
+
−
  +
−
  Although in informal settings a reasoning infrastructure for alpha-equated +
−
  terms (that have names for bound variables) is nearly always taken for granted, establishing +
−
  it automatically in a theorem prover is a rather non-trivial task. +
−
  For every specification we will need to construct a type containing as +
−
  elements the alpha-equated terms. To do so we use +
−
  the standard HOL-technique of defining a new type by  +
−
  identifying a non-empty subset of an existing type. In our +
−
  case  we take as the starting point the type of sets of concrete+
−
  terms (the latter being defined as a datatype). Then identify the +
−
  alpha-equivalence classes according to our alpha-equivalence relation and +
−
  then identify the new type as these alpha-equivalence classes.  The construction we +
−
  can perform in HOL is illustrated by the following picture:+
−
 +
−
  \begin{center}+
−
  figure+
−
  %\begin{pspicture}(0.5,0.0)(8,2.5)+
−
  %%\showgrid+
−
  %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5)+
−
  %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6}+
−
  %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9)+
−
  +
−
  %\pcline[linewidth=0.4mm]{->}(2.6,1.5)(4.8,1.5)+
−
  +
−
  %\pcline[linewidth=0.2mm](2.2,2.1)(6,2.1)+
−
  %\pcline[linewidth=0.2mm](2.2,0.9)(6,0.9)+
−
+
−
  %\rput(7.3,2.2){$\mathtt{phi}$}+
−
  %\rput(6,1.5){$\lama$}+
−
  %\rput[l](7.6,2.05){\begin{tabular}{l}existing\\[-1.6mm]type\end{tabular}}+
−
  %\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}}+
−
  %\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}}+
−
  %\rput[c](1.7,1.5){$\lama$}+
−
  %\rput(3.7,1.75){isomorphism}+
−
  %\end{pspicture}+
−
  \end{center}+
−
+
−
  \noindent+
−
  To ``lift'' the reasoning from the underlying type to the new type+
−
  is usually a tricky task. To ease this task we reimplemented in Isabelle/HOL+
−
  the quotient package described by Homeier in \cite{Homeier05}. This+
−
  re-implementation will automate the proofs we require for our+
−
  reasoning infrastructure over alpha-equated terms.\medskip+
−
+
−
  \noindent+
−
  {\bf Contributions:}  We provide new definitions for when terms+
−
  involving multiple binders are alpha-equivalent. These definitions are+
−
  inspired by earlier work of Pitts \cite{}. By means of automatic+
−
  proofs, we establish a reasoning infrastructure for alpha-equated+
−
  terms, including properties about support, freshness and equality+
−
  conditions for alpha-equated terms. We will also derive for these+
−
  terms a strong induction principle that has the variable convention+
−
  already built in.+
−
*}+
−
+
−
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}. 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, we+
−
  shall assume in what follows 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 +
−
  two-place permutation operation written+
−
+
−
  @{text[display,indent=5] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+
−
+
−
  \noindent +
−
  with a generic type in which @{text "\<alpha>"} stands for the type of atoms +
−
  and @{text "\<beta>"} for the type of the objects on which the permutation +
−
  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 @{term p} as @{text "- p"}. The permutation+
−
  operation is defined for products, lists, sets, functions, booleans etc +
−
  (see \cite{HuffmanUrban10}).+
−
+
−
  The most original aspect of the nominal logic work of Pitts et al is a general+
−
  definition for ``the set of free variables of an object @{text "x"}''.  This+
−
  definition is general in the sense that it applies not only to lambda-terms,+
−
  but also to lists, products, sets and even functions. The definition depends+
−
  only on the permutation operation and on the notion of equality defined for+
−
  the type of @{text x}, namely:+
−
+
−
  @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}+
−
+
−
  \noindent+
−
  There is also the derived notion for when an atom @{text a} is \emph{fresh}+
−
  for an @{text x}, defined as+
−
  +
−
  @{thm[display,indent=5] fresh_def[no_vars]}+
−
+
−
  \noindent+
−
  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}+
−
  @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}+
−
  \end{property}+
−
+
−
  \noindent+
−
  For a proof see \cite{HuffmanUrban10}.+
−
+
−
  \begin{property}+
−
  @{thm[mode=IfThen] at_set_avoiding[no_vars]}+
−
  \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  +
−
  many discussions about Nominal Isabelle. We thank Peter Sewell for +
−
  making the informal notes \cite{SewellBestiary} available to us and +
−
  also for explaining some of the finer points about the abstract +
−
  definitions and about the implementation of the Ott-tool.+
−
+
−
+
−
*}+
−
+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−