18 

    18   So far, Nominal Isabelle provided a mechanism to construct

    19   It has not yet fared so well in the POPLmark challenge

    19   automatically alpha-equated lambda terms sich as

    20   as the second part contain a formalisation of records 

    20 

    21   where ...

    21   \begin{center}

    22 

    22   $t ::= x \mid t\;t \mid \lambda x. t$

    23   The difficulty can be appreciated by considering that the

    23   \end{center}

    24   definition given by Leroy in \cite{Leroy92} is incorrect (it omits a

    24 

    25   side-condition).

    25   \noindent

    26 

    26   For such calculi, it derived automatically a convenient reasoning

    27   Examples: type-schemes, Spi-calculus

    27   infrastructure. With this it has been used to formalise an equivalence

    28 

    28   checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

    29   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency

    30   \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result

    31   for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been

    32   used by Pollack for formalisations in the locally-nameless approach to

    33   binding \cite{SatoPollack10}.

    34 

    35   However, Nominal Isabelle has fared less well in a formalisation of

    36   the algorithm W \cite{UrbanNipkow09} where types and type-schemes

    37   are represented by

    38 

    39   \begin{center}

    40   \begin{tabular}{l}

    41   $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$

    42   \end{tabular}

    43   \end{center}

    44 

    45   \noindent

    46   While it is possible to formalise the finite set of variables that are

    47   abstracted in a type-scheme by iterating single abstractions, it leads to a very

    48   clumsy formalisation. This need of iterating single binders for representing

    49   multiple binders is also the reason why Nominal Isabelle and other theorem

    50   provers have so far not fared very well with the more advanced tasks in the POPLmark

    51   challenge, because also there one would like to abstract several variables 

    52   at once.

    53 

    54   There are interesting points to note with binders that abstract multiple 

    55   variables. First in the case of type-schemes we do not like to make a distinction

    56   about the order of the binders. So we would like to regard the following two

    57   type-schemes as alpha-equivalent:

    58 

    59   \begin{center}

    60   $\forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ 

    61   \end{center}

    62 

    63   \noindent

    64   but assuming $x$, $y$ and $z$ are distinct, the following two should be \emph{not} 

    65   alpha-equivalent:

    66 

    67   \begin{center}

    68   $\forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ 

    69   \end{center}

    70 

    71   \noindent

    72   However we do like to regard type-schemes as alpha-equivalent, if they

    73   differ only on \emph{vacuous} binders, such as

    74 

    75   \begin{center}

    76   $\forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ 

    77   \end{center}

    78 

    79   \noindent

    80   In this paper we will give a general abstraction mechanism and assciated notion of alpha-equivalence 

    81   which can be used to represent type-schemes.  The difficulty in finding the notion of alpha-equivalence 

    82   can be appreciated by considering that the definition given by Leroy in \cite{Leroy92} is incorrect 

    83   (it omits a side-condition).

    84 

    85   However, the notion of alpha-equivalence that is preserved by vacuous binders is not

    86   alway wanted. For example in constructs like

    87 

    88   \begin{center}

    89   $\LET x = 3 \AND y = 2 \IN x \backslash y \END$

    90   \end{center}

    91 

    92   \noindent

    93   we might not care in which order the associations $x = 3$ and $y = 2$ are

    94   given, but it would be unusual to regard this term as alpha-equivalent with

    95 

    96   \begin{center}

    97   $\LET x = 3 \AND y = 2 \AND z = loop \IN x \backslash y \END$

    98   \end{center}

    99 

   100   \noindent

   101   We will provide a separate abstraction mechanism for this case where the

   102   order of binders does not matter, but the ``cardinality'' of the binders

   103   has to be the same.

   104 

   105   However, this is still not sufficient for covering language constructs frequently 

   106   occuring in programming language research. For example in patters like

   107 

   108   \begin{center}

   109   $\LET (x, y) = (3, 2) \IN x \backslash y \END$

   110   \end{center}

   111 

   112   \noindent

   113   we want to bind all variables from the pattern (there might be an arbitrary

   114   number of them) inside the body of the let, but we also care about the order

   115   of these variables, since we do not want to identify this term with

   116 

   117   \begin{center}

   118   $\LET (y, x) = (3, 2) \IN x \backslash y \END$

   119   \end{center}

   120 

   121   \noindent

   122   Therefore we have identified three abstraction mechanisms for multiple binders

   123   and allow the user to chose which one is intended. 

   124 

   125   By providing general abstraction mechanisms that allow the binding of multiple

   126   variables, we have to work around aproblem that has been first pointed out

   127   by Pottier in \cite{Pottier}: in let-constructs such as

   128 

   129   \begin{center}

   130   $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$

   131   \end{center}

   132 

   133   \noindent

   134   where the $x_i$ are bound in $s$. In this term we might not care about the order in 

   135   which the $x_i = t_i$ are given, but we do care about the information that there are 

   136   as many $x_i$ as there are $t_i$. We lose this information if we represent the $\mathtt{let}$

   137   as something 

   138 

   139   

   140 

   141   

   142