(*<*)+
−
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 {*+
−
+
−
  It has not yet fared so well in the POPLmark challenge+
−
  as the second part contain a formalisation of records +
−
  where ...+
−
+
−
  The difficulty can be appreciated by considering that the+
−
  definition given by Leroy in \cite{Leroy92} is incorrect (it omits a+
−
  side-condition).+
−
+
−
  Examples: type-schemes, Spi-calculus+
−
+
−
  Contributions:  We provide definitions for when terms+
−
  involving general bindings are alpha-equivelent.+
−
+
−
  %\begin{center}+
−
  %\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}+
−
+
−
  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}. 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 +
−
  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 *}+
−
+
−
section {* Examples *}+
−
+
−
section {* Adequacy *}+
−
+
−
section {* Related Work *}+
−
+
−
section {* Conclusion *}+
−
+
−
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 for explaining some of the finer points of the OTT-tool.+
−
+
−
+
−
*}+
−
+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−