667   requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:

   667   requirements {\it (i)} to {\it (iv)} can be stated formally as:

  1025   \isacommand{binds} the labels must refer to atom types or lists of atom

  1038   \isacommand{binds} the labels must refer to atom types or to lists of atom

  1031   \begin{tabular}{@ {}c@ {\hspace{5mm}}c@ {}}

  1044   \begin{tabular}{@ {}c@ {\hspace{8mm}}c@ {}}

  1041   \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\

  1055   \hspace{2mm}\phantom{$\mid$}~@{text "TVar name"}\\

  1042   \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\

  1056   \hspace{2mm}$\mid$~@{text "TFun ty ty"}\\

  1043   \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\hspace{3mm}%

  1057   \isacommand{and}~@{text "tsc ="}\\

  1058   \hspace{2mm}\phantom{$\mid$}~@{text "TAll xs::(name fset) T::ty"}\hspace{3mm}%

  1179   In this example the term constructor @{text "ACons'"} contains a binding 

  1194   In this example the term constructor @{text "ACons'"} has four arguments and

  1180   clause, and also is used in the definition of the binding function. The

  1195   contains a binding clause. This constructor is also used in the definition

  1181   restriction we have to impose is that the binding function can only return

  1196   of the binding function. The restriction we have to impose is that the

  1182   free atoms, that is the ones that are not mentioned in a binding clause.

  1197   binding function can only return free atoms, that is the ones that are not

  1183   Therefore @{text "y"} cannot be used in the binding function @{text "bn"}

  1198   mentioned in a binding clause.  Therefore @{text "y"} cannot be used in the

  1184   (since it is bound in @{text "ACons'"} by the binding clause), but @{text x}

  1199   binding function @{text "bn"} (since it is bound in @{text "ACons'"} by the

  1185   can (since it is a free atom). This restriction is sufficient for lifting 

  1200   binding clause), but @{text x} can (since it is a free atom). This

  1186   the binding function to alpha-equated terms. If we would permit that @{text "bn"}

  1201   restriction is sufficient for lifting the binding function to alpha-equated

  1187   can also return @{text "y"}, then it would not be respectful and therefore

  1202   terms. If we would permit that @{text "bn"} can also return @{text "y"},

  1188   cannot be lifted.

  1203   then it would not be respectful and therefore cannot be lifted.

  1502   clause are. To understand better whet the general pattern is, let us first 

  1517   clause are. To understand better what the general pattern is, let us first 

  1511   In this binding clause no atom is bound and we only have to `alpha-relate' the bodies. For this

  1526   In this binding clause no atom is bound and we only have to `alpha-relate'

  1512   we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}  

  1527   the bodies. For this we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>,

  1513   whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and

  1528   d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}

  1514   respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate

  1529   whereby the labels @{text "d"}$_{1..q}$ refer to the arguments @{text

  1515   two such tuples we define the compound alpha-equivalence relation @{text "R"} as follows

  1530   "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text

  1516   

  1531   "z\<PRIME>"}$_{1..n}$ of the term-constructor. In order to relate two such

  1532   tuples we define the compound alpha-equivalence relation @{text "R"} as

  1533   follows

  1534 

  1519   \end{equation}

  1537   \end{equation}\smallskip

  1520 

  1538 

  1521   \noindent

  1539   \noindent

  1522   with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and 

  1540   with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding

  1523   @{text "d\<PRIME>\<^isub>i"} refer

  1541   labels @{text "d\<^isub>i"} and @{text "d\<PRIME>\<^isub>i"} refer to a

  1524   to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise

  1542   recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise

  1525   we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define

  1543   we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the

  1526   the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"},

  1544   latter is because @{text "ty\<^isub>i"} is not part of the specified types

  1527   which can be unfolded to the series of premises

  1545   and alpha-equivalence of any previously defined type is supposed to coincide

  1528   

  1546   with equality.  This lets us now define the premise for an empty binding

  1529   \begin{center}

  1547   clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"}, which can be

  1548   unfolded to the series of premises

  1549   

  1550   \[

  1531   \end{center}

  1552   \]\smallskip

  1540   \end{equation}

  1561   \end{equation}\smallskip

  1553   \begin{center}

  1574   \[

  1555   \end{center}

  1576   \]\smallskip

  1562   \begin{center}

  1583   \[

  1564   \end{center}

  1585   \]\smallskip

  1570   \begin{center}

  1591   \[

  1572   \end{center}

  1593   \]\smallskip

  1576   clause. 

  1597   clause. However, in case the binders have non-recursive deep binders, this

  1577   However, in case the binders have non-recursive deep binders, this premise

  1598   premise is not enough: we also have to ``propagate'' alpha-equivalence

  1578   is not enough:

  1599   inside the structure of these binders. An example is @{text "Let"} where we

  1579   we also have to ``propagate'' alpha-equivalence inside the structure of

  1600   have to make sure the right-hand sides of assignments are

  1580   these binders. An example is @{text "Let"} where we have to make sure the

  1601   alpha-equivalent. For this we use relations @{text "\<approx>bn"}$_{1..m}$ (which we

  1581   right-hand sides of assignments are alpha-equivalent. For this we use 

  1602   will formally define shortly).  Let us assume the non-recursive deep binders

  1582   relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).

  1603   in @{text "bc\<^isub>i"} are

  1583   Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are

  1604   

  1584   

  1605   \[

  1585   \begin{center}

  1587   \end{center}

  1607   \]\smallskip

  1588   

  1608   

  1589   \noindent

  1609   \noindent

  1590   The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})

  1610   The tuple @{text L} consists then of all these binders @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} 

  1591   and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}. 

  1611   (similarly @{text "L'"}) and the compound equivalence relation @{text "R'"} 

  1592   All premises for @{text "bc\<^isub>i"} are then given by

  1612   is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}.  All premises for @{text "bc\<^isub>i"} are then given by

  1593   

  1613   

  1594   \begin{center}

  1614   \[

  1596   \end{center} 

  1616   \]\smallskip

  1602   \begin{center}

  1622   \[

  1604   \end{center}

  1624   \]\smallskip

  1610   \begin{center}

  1630   \[

  1613   \end{center}

  1633   \]\smallskip

  1618   \begin{center}

  1638   \[\mbox{

  1621   is a recursive argument of @{text C},\\

  1641   is a recursive argument of @{text C},\smallskip\\

  1623   and is a non-recursive argument of @{text C},\\

  1643   and is a non-recursive argument of @{text C},\smallskip\\

  1625   with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\

  1645   with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\smallskip\\

  1628   \end{tabular}

  1648   \end{tabular}}

  1629   \end{center}

  1649   \]\smallskip

  1641   \begin{center}

  1661   \[\mbox{

  1644   {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\

  1664   {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & 

  1665   \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\\

  1666   \\

  1646   {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}

  1668   {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}\\

  1647   \end{tabular}

  1669   \\

  1648   \end{center}

  1670 

  1649 

  1650   \begin{center}

  1654   {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}

  1674   {@{text "a = a'"} & \hspace{5mm}@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>assn\<^esub> as'"}}

  1655   \end{tabular}

  1675   \end{tabular}\\

  1656   \end{center}

  1676   \\

  1657 

  1677 

  1658   \begin{center}

  1662   {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}

  1681   {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}

  1664   \end{center}

  1683   \end{tabular}}

  1684   \]\smallskip

  1680   Having made all necessary definitions for raw terms, we can start

  1700   Having made all necessary definitions for raw terms, we can start with

  1681   with establishing the reasoning infrastructure for the alpha-equated types

  1701   establishing the reasoning infrastructure for the alpha-equated types @{text

  1682   @{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch

  1702   "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We

  1683   in this section the proofs we need for establishing this infrastructure. One

  1703   give in this section and the next the proofs we need for establishing this

  1684   main point of our work is that we have completely automated these proofs in Isabelle/HOL.

  1704   infrastructure. One main point of our work is that we have completely

  1685 

  1705   automated these proofs in Isabelle/HOL.

  1686   First we establish that the

  1706 

  1687   alpha-equivalence relations defined in the previous section are 

  1707   First we establish that the free-variable functions, the binding functions and the

  1708   alpha-equivalences are equivariant.

  1709 

  1710   \begin{lem}\mbox{}\\

  1711   @{text "(i)"} The functions @{text "fa_ty"}$_{1..n}$, @{text "fa_bn"}$_{1..m}$ and

  1712   @{text "bn"}$_{1..m}$ are equivariant.\\

  1713   @{text "(ii)"} The relations @{text "\<approx>ty"}$_{1..n}$ and

  1714   @{text "\<approx>bn"}$_{1..m}$ are equivariant.

  1715   \end{lem}

  1716 

  1717   \begin{proof}

  1718   The function package of Isabelle/HOL allows us to prove the first part is by mutual 

  1719   induction over the definitions of the functions. The second is by a straightforward

  1720   induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using 

  1721   the first part.

  1722   \end{proof}

  1723 

  1724   \noindent

  1725   Next we establish that the alpha-equivalence relations defined in the

  1726   previous section are equivalence relations.

  1727 

  1728   \begin{lem}\label{equiv} 

  1729   The relations @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ are

  1700   can be dealt with as in Lemma~\ref{alphaeq}.

  1737   can be dealt with as in Lemma~\ref{alphaeq}. However, the transitivity

  1738   case needs in addition the fact that the relations are equivariant. 

  1707   "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text

  1746   "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text "C"}$_{1..k}$,

  1708   "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text

  1747   and similar definitions for the free-atom functions @{text

  1709   "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text

  1748   "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the

  1710   "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the 

  1749   binding functions @{text "bn"}$^\alpha_{1..m}$. For this we have to show

  1750   by induction over the definitions of alpha-equivalences that the ``raw'' 

  1751   functions are respectful. This means we need to establish that

  1752 

  1753   \[\mbox{

  1754   \begin{tabular}{lll}

  1755   @{text "x \<approx>ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\

  1756   @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\

  1757   @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\

  1758   \end{tabular}

  1759   }\]\smallskip

  1760   

  1761   \noindent

  1762   holds whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"} is defined. A 

  1763   similar property is needed for the constructors @{text "C"}$_{1..k}$. In order 

  1764   to establish it we need to prove that

  1765 

  1766   \[\mbox{

  1767   \begin{tabular}{lll}

  1768   @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "x \<approx>bn\<^isub>j x'"}\\

  1769   \end{tabular}

  1770   }\]\smallskip

  1771 

  1772   \noindent

  1773   The respectfulness properties are crucial, ... ???

  1774   However, these definitions are not really useful to the 

  1719   \begin{equation}\label{distinctalpha}

  1783   \[\label{distinctalpha}

  1722   \end{equation}

  1786   \]\smallskip

  1729   \begin{equation}\label{distinctraw}

  1793   \[\label{distinctraw}

  1731   \end{equation}

  1795   \]\smallskip

  1777   \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can 

  1841   \eqref{distinctraw}. ??? Having the facts \eqref{fnresp} at our disposal, we can 

  1779   %

  1843   

  1780   \begin{center}

  1844   \[

  1781   @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}

  1845   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}

  1782   \end{center}

  1846   \]\smallskip

  1788   \begin{center}

  1852   \[

  1790   \end{center}

  1854   \]\smallskip

  1806   @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}

  1870   @{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}

  1807   \end{equation}

  1871   \end{equation}\smallskip

  1824   \end{equation} 

  1888   \end{equation} \smallskip

  1833   \end{equation}

  1897   \end{equation}\smallskip

  1843   \begin{center}

  1907   \[\mbox{

  1844   \begin{tabular}{rcl@ {\hspace{10mm}}rcl}

  1908   \begin{tabular}{rcl}

  1845   @{text "p \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"} &

  1909   @{text "\<pi> \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (\<pi> \<bullet> x)"}\\

  1846   @{text "p \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}\\

  1910   @{text "\<pi> \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\

  1847   @{text "p \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\

  1911   @{text "\<pi> \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\

  1848   \end{tabular}

  1912   \end{tabular}}

  1849   \end{center}

  1913   \]

  1850   

  1914 

  1851   \noindent

  1915   

  1852   These properties can be established using the induction principle for the types @{text "ty\<AL>"}$_{1..n}$.

  1916   \noindent

  1853   in \eqref{weakinduct}.

  1917   These properties can be established using the induction principle for the

  1854   Having these equivariant properties established, we can

  1918   types @{text "ty\<AL>"}$_{1..n}$.  in \eqref{weakinduct}.  Having these

  1855   show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in

  1919   equivariant properties established, we can show that the support of

  1856   the support of its arguments, that means 

  1920   term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its

  1857 

  1921   arguments, that means

  1858   \begin{center}

  1922 

  1923   \[

  1860   \end{center}

  1925   \]\smallskip

  2247   is described in \cite{NaraschewskiNipkow99} about a formalisation of the

  2312   is described by Nara\-schew\-ski and Nipkow \cite{NaraschewskiNipkow99} with a

  2248   algorithm W. This formalisation implements binding in type-schemes using a

  2313   formalisation of the algorithm W. This formalisation implements binding in

  2249   de-Bruijn indices representation. Since type-schemes in W contain only a single

  2314   type-schemes using a de-Bruijn indices representation. Since type-schemes in

  2250   place where variables are bound, different indices do not refer to different binders (as in the usual

  2315   W contain only a single place where variables are bound, different indices

  2251   de-Bruijn representation), but to different bound variables. A similar idea

  2316   do not refer to different binders (as in the usual de-Bruijn

  2252   has been recently explored for general binders in the locally nameless

  2317   representation), but to different bound variables. A similar idea has been

  2253   approach to binding \cite{chargueraud09}.  There, de-Bruijn indices consist

  2318   recently explored for general binders by Chargu\'eraud in the locally nameless 

  2254   of two numbers, one referring to the place where a variable is bound, and the

  2319   approach to

  2255   other to which variable is bound. The reasoning infrastructure for both

  2320   binding \cite{chargueraud09}.  There, de-Bruijn indices consist of two

  2256   representations of bindings comes for free in theorem provers like Isabelle/HOL or

  2321   numbers, one referring to the place where a variable is bound, and the other

  2257   Coq, since the corresponding term-calculi can be implemented as ``normal''

  2322   to which variable is bound. The reasoning infrastructure for both

  2258   datatypes.  However, in both approaches it seems difficult to achieve our

  2323   representations of bindings comes for free in theorem provers like

  2259   fine-grained control over the ``semantics'' of bindings (i.e.~whether the

  2324   Isabelle/HOL or Coq, since the corresponding term-calculi can be implemented

  2260   order of binders should matter, or vacuous binders should be taken into

  2325   as ``normal'' datatypes.  However, in both approaches it seems difficult to

  2261   account). To do so, one would require additional predicates that filter out

  2326   achieve our fine-grained control over the ``semantics'' of bindings

  2262   unwanted terms. Our guess is that such predicates result in rather

  2327   (i.e.~whether the order of binders should matter, or vacuous binders should

  2263   intricate formal reasoning.

  2328   be taken into account). To do so, one would require additional predicates

  2329   that filter out unwanted terms. Our guess is that such predicates result in

  2330   rather intricate formal reasoning. We are not aware of any non-trivial 

  2331   formalisation that uses Chargu\'eraud's idea.

  2332 

  2266   (HOAS). , which for example is implemented in the Twelf system. 

  2335   (HOAS), which for example is implemented in the Twelf system. This

  2267   This representation

  2336   representation technique supports very elegantly many aspects of

  2268   technique supports very elegantly many aspects of \emph{single} binding, and

  2337   \emph{single} binding, and impressive work by Lee et al has been done that

  2269   impressive work has been done that uses HOAS for mechanising the metatheory

  2338   uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We

  2270   of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple

  2339   are, however, not aware how multiple binders of SML are represented in this

  2271   binders of SML are represented in this work. Judging from the submitted

  2340   work. Judging from the submitted Twelf-solution for the POPLmark challenge,

  2272   Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with

  2341   HOAS cannot easily deal with binding constructs where the number of bound

  2273   binding constructs where the number of bound variables is not fixed. For example 

  2342   variables is not fixed. For example In the second part of this challenge,

  2274   In the second part of this challenge, @{text "Let"}s involve

  2343   @{text "Let"}s involve patterns that bind multiple variables at once. In

  2275   patterns that bind multiple variables at once. In such situations, HOAS

  2344   such situations, HOAS seems to have to resort to the

  2276   seems to have to resort to the iterated-single-binders-approach with

  2345   iterated-single-binders-approach with all the unwanted consequences when

  2277   all the unwanted consequences when reasoning about the resulting terms.

  2346   reasoning about the resulting terms.

  2347 

  2288   be rather unpleasant. The hope is that the extension presented in this paper

  2358   be rather unpleasant. 

  2289   is a substantial improvement.

  2291   The most closely related work to the one presented here is the Ott-tool

  2360   The most closely related work to the one presented here is the Ott-tool by

  2292   \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty

  2361   Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier

  2293   front-end for creating \LaTeX{} documents from specifications of

  2362   \cite{Pottier06}. Ott is a nifty front-end for creating \LaTeX{} documents

  2294   term-calculi involving general binders. For a subset of the specifications

  2363   from specifications of term-calculi involving general binders. For a subset

  2295   Ott can also generate theorem prover code using a raw representation of

  2364   of the specifications Ott can also generate theorem prover code using a raw

  2296   terms, and in Coq also a locally nameless representation. The developers of

  2365   representation of terms, and in Coq also a locally nameless

  2297   this tool have also put forward (on paper) a definition for

  2366   representation. The developers of this tool have also put forward (on paper)

  2298   alpha-equivalence of terms that can be specified in Ott.  This definition is

  2367   a definition for alpha-equivalence and free variables for terms that can be

  2299   rather different from ours, not using any nominal techniques.  To our

  2368   specified in Ott.  This definition is rather different from ours, not using

  2300   knowledge there is no concrete mathematical result concerning this

  2369   any nominal techniques.  To our knowledge there is no concrete mathematical

  2301   notion of alpha-equivalence.  Also the definition for the 

  2370   result concerning this notion of alpha-equivalence and free variables. We

  2302   notion of free variables

  2371   have proved that our definitions lead to alpha-equated terms, whose support

  2303   is work in progress.

  2372   is as expected (that means bound names are removed from the support). We

  2304 

  2373   also showed that our specifications lift from a raw type to a type of

  2305   Although we were heavily inspired by the syntax of Ott,

  2374   alpha-equivalence classes. For this we were able to establish then every

  2306   its definition of alpha-equi\-valence is unsuitable for our extension of

  2375   term-constructor and function is repectful w.r.t.~alpha-equivalence.

  2307   Nominal Isabelle. First, it is far too complicated to be a basis for

  2376 

  2308   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it

  2377   Although we were heavily inspired by the syntax of Ott, its definition of

  2309   covers cases of binders depending on other binders, which just do not make

  2378   alpha-equi\-valence is unsuitable for our extension of Nominal

  2310   sense for our alpha-equated terms. Third, it allows empty types that have no

  2379   Isabelle. First, it is far too complicated to be a basis for automated

  2311   meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 

  2380   proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases

  2312   binding clauses. In Ott you specify binding clauses with a single body; we 

  2381   of binders depending on other binders, which just do not make sense for our

  2313   allow more than one. We have to do this, because this makes a difference 

  2382   alpha-equated terms. Third, it allows empty types that have no meaning in a

  2314   for our notion of alpha-equivalence in case of \isacommand{binds (set)} and 

  2383   HOL-based theorem prover. We also had to generalise slightly Ott's binding

  2315   \isacommand{binds (set+)}. 

  2384   clauses. In Ott one specifies binding clauses with a single body; we allow

  2316   

  2385   more than one. We have to do this, because this makes a difference for our

  2317   Consider the examples

  2386   notion of alpha-equivalence in case of \isacommand{binds (set)} and

  2318   

  2387   \isacommand{binds (set+)}. Consider the examples

  2319   \begin{center}

  2388   

  2389   \[\mbox{

  2326   \end{tabular}

  2396   \end{tabular}}

  2327   \end{center}

  2397   \]\smallskip

  2328   

  2398   

  2329   \noindent

  2399   \noindent

  2330   In the first term-constructor we have a single

  2400   In the first term-constructor we have a single body that happens to be

  2331   body that happens to be ``spread'' over two arguments; in the second term-constructor we have

  2401   ``spread'' over two arguments; in the second term-constructor we have two

  2332   two independent bodies in which the same variables are bound. As a result we 

  2402   independent bodies in which the same variables are bound. As a result we

  2333   have

  2403   have\footnote{Assuming @{term "a \<noteq> b"}, there is no permutation that can

  2404   make @{text "(a, b)"} equal with @{text "(a, b)"} and @{text "(b, a)"}, but

  2405   there are two permutations so that we can make @{text "(a, b)"} and @{text

  2406   "(a, b)"} equal with one permutation, and @{text "(a, b)"} and @{text "(b,

  2407   a)"} with the other.}

  2408 

  2335   \begin{center}

  2410   \[\mbox{

  2338   @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\

  2413   @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}

  2414   \end{tabular}}

  2415   \]\smallskip

  2416  

  2417   \noindent

  2418   but 

  2419 

  2420   \[\mbox{

  2421   \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}

  2341   \end{tabular}

  2424   \end{tabular}}

  2342   \end{center}

  2425   \]\smallskip

  2343   

  2426   

  2344   \noindent

  2427   \noindent

  2345   and therefore need the extra generality to be able to distinguish between 

  2428   and therefore need the extra generality to be able to distinguish between

  2346   both specifications.

  2429   both specifications.  Because of how we set up our definitions, we also had

  2347   Because of how we set up our definitions, we also had to impose some restrictions

  2430   to impose some restrictions (like a single binding function for a deep

  2348   (like a single binding function for a deep binder) that are not present in Ott. 

  2431   binder) that are not present in Ott. Our expectation is that we can still

  2349   Our

  2432   cover many interesting term-calculi from programming language research, for

  2350   expectation is that we can still cover many interesting term-calculi from

  2433   example Core-Haskell. ???

  2351   programming language research, for example Core-Haskell. 

  2434 

  2352 

  2435   Pottier presents a programming language, called C$\alpha$ml, for

  2353   Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for 

  2436   representing terms with general binders inside OCaml \cite{Pottier06}. This

  2354   representing terms with general binders inside OCaml. This language is

  2437   language is implemented as a front-end that can be translated to OCaml with

  2355   implemented as a front-end that can be translated to OCaml with the help of

  2438   the help of a library. He presents a type-system in which the scope of

  2356   a library. He presents a type-system in which the scope of general binders

  2439   general binders can be specified using special markers, written @{text

  2357   can be specified using special markers, written @{text "inner"} and 

  2440   "inner"} and @{text "outer"}. It seems our and his specifications can be

  2358   @{text "outer"}. It seems our and his specifications can be

  2441   inter-translated as long as ours use the binding mode \isacommand{binds}

  2359   inter-translated as long as ours use the binding mode 

  2442   only.  However, we have not proved this. Pottier gives a definition for

  2360   \isacommand{binds} only.

  2361   However, we have not proved this. Pottier gives a definition for 

  2364   it defines an equivalence relation. A complete

  2445   it defines an equivalence relation. A complete reasoning infrastructure is

  2365   reasoning infrastructure is well beyond the purposes of his language. 

  2446   well beyond the purposes of his language. Similar work for Haskell with

  2366   Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.

  2447   similar results was reported by Cheney \cite{Cheney05a} and more recently 

  2367   

  2448   by ???

  2368   In a slightly different domain (programming with dependent types), the 

  2449 

  2369   paper \cite{Altenkirch10} presents a calculus with a notion of 

  2450   In a slightly different domain (programming with dependent types),

  2370   alpha-equivalence related to our binding mode \isacommand{binds (set+)}.

  2451   Altenkirch et al present a calculus with a notion of alpha-equivalence

  2371   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it

  2452   related to our binding mode \isacommand{binds (set+)} \cite{Altenkirch10}.

  2372   has a more operational flavour and calculates a partial (renaming) map. 

  2453   Their definition is similar to the one by Pottier, except that it has a more

  2373   In this way, the definition can deal with vacuous binders. However, to our

  2454   operational flavour and calculates a partial (renaming) map. In this way,

  2374   best knowledge, no concrete mathematical result concerning this

  2455   the definition can deal with vacuous binders. However, to our best

  2375   definition of alpha-equivalence has been proved.  

  2456   knowledge, no concrete mathematical result concerning this definition of

  2457   alpha-equivalence has been proved.

  2381   Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure).

  2463   %%Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure).

  2382 

  2464 

  2383 

  2465 

  2384   We have presented an extension of Nominal Isabelle for dealing with

  2466   We have presented an extension of Nominal Isabelle for dealing with general

  2385   general binders, that is term-constructors having multiple bound 

  2467   binders, that is term-constructors having multiple bound variables. For this

  2386   variables. For this extension we introduced new definitions of 

  2468   extension we introduced new definitions of alpha-equivalence and automated

  2387   alpha-equivalence and automated all necessary proofs in Isabelle/HOL.

  2469   all necessary proofs in Isabelle/HOL.  To specify general binders we used

  2388   To specify general binders we used the specifications from Ott, but extended them 

  2470   the syntax from Ott, but extended it in some places and restricted

  2389   in some places and restricted

  2471   it in others so that they make sense in the context of alpha-equated

  2390   them in others so that they make sense in the context of alpha-equated terms. 

  2472   terms. We also introduced two binding modes (set and set+) that do not exist

  2391   We also introduced two binding modes (set and set+) that do not 

  2473   in Ott. We have tried out the extension with calculi such as Core-Haskell,

  2392   exist in Ott. 

  2474   type-schemes and approximately a dozen of other typical examples from

  2393   We have tried out the extension with calculi such as Core-Haskell, type-schemes 

  2475   programming language research~\cite{SewellBestiary}. The code will

  2394   and approximately a  dozen of other typical examples from programming 

  2476   eventually become part of the next Isabelle distribution.\footnote{It 

  2395   language research~\cite{SewellBestiary}. 

  2477   can be downloaded already from the Mercurial repository linked at

  2396   The code

  2397   will eventually become part of the next Isabelle distribution.\footnote{For the moment

  2398   it can be downloaded from the Mercurial repository linked at

  2415   achieve this, we need a slightly more clever implementation than we have at the moment. 

  2494   achieve this, we need more clever implementation than we have 

  2495   at the moment. However, really lifting this restriction will involve major

  2496   work on the datatype package of Isabelle/HOL.

  2423   \begin{center}

  2504   \[

  2424   @{text "fa_ty x  =  bn x \<union> fa_bn x"}.

  2505   \mbox{@{text "fa_ty x  =  bn x \<union> fa_bn x"}}

  2425   \end{center}

  2506   \]\smallskip

  2431   imagine that there is need for a binding mode where instead of lists, we

  2512   imagine that there is need for a binding mode where instead of usual lists,

  2432   abstract lists of distinct elements.  Once we feel confident about such

  2513   we abstract lists of distinct elements (the corresponding type @{text

  2433   binding modes, our implementation can be easily extended to accommodate

  2514   "dlist"} already exists in the library of Isabelle/HOL). We expect the

  2434   them.\medskip

  2515   presented work can be easily extended to accommodate them.\medskip