998 

   998   %

   999   \begin{center}

   999   \begin{equation}\label{letpat}

  1000   \mbox{%

  1016   \end{tabular}

  1017   \end{tabular}}

  1017   \end{center}

  1018   \end{equation}

  1085   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} 

  1086   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}\\ 

  1086      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t},

  1087   \hspace{20mm}\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t},

  1633   For each binding function @{text "bn\<^isub>j :: ty\<^isub>i \<Rightarrow> \<dots>"} we define a permutation operation

  1636 *}

  1634   @{text "\<bullet>bn\<^isub>j\<^isub> :: perm \<Rightarrow> ty\<^isub>i \<Rightarrow> ty\<^isub>i"}. This operation permutes only the arguments

  1637 

  1635   that are bound by the binding function while also descending in the recursive subcalls.

  1638 section {* Strong Induction Principles *}

  1636   For each term constructor @{text "C x\<^isub>1 \<dots> x\<^isub>n"} the @{text "\<bullet>bn\<^isub>j"} operation applied

  1639 

  1637   to a permutation @{text "\<pi>"} and to this constructor equals the constructor applied

  1640 text {*

  1638   to the values for each argument. Provided @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, the value

  1641   In the previous section we were able to provide induction principles that 

  1639   for an argument @{text "x\<^isub>j"} is:

  1642   allow us to perform structural inductions over alpha-equated terms. 

  1643   We call such induction principles \emph{weak}, because in case of a term-contructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},

  1644   the induction hypothesis requires us to establish the implication

  1645   %

  1646   \begin{equation}\label{weakprem}

  1647   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 

  1648   \end{equation}

  1649 

  1650   \noindent

  1651   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 

  1652   The problem with this implication is that in general it is not easy to establish.

  1653   The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"} 

  1654   (for example we cannot assume the variable convention).

  1655 

  1656   In \cite{UrbanTasson05} we introduced a method for automatically

  1657   strengthening weak induction principles for terms containing single

  1658   binders. These stronger induction principles allow us to make additional

  1659   assumptions about binders. These additional assumptions amount to a formal

  1660   version of the usual variable convention for binders. A natural question is

  1661   whether we can also strengthen the weak induction principles in the presence

  1662   general binders. We will indeed be able to so, but for this we need an 

  1663   additional notion of permuting deep binders. 

  1664 

  1665   Given a binding function @{text "bn"} we need to define an auxiliary permutation 

  1666   operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.

  1667   Given a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then

  1668   %

  1669   \begin{center}

  1670   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"}

  1671   \end{center}

  1672 

  1673   \noindent

  1674   with @{text "y\<^isub>i"} determined as follows:

  1675   %

  1642   $\bullet$ & @{text "x\<^isub>i"} provided @{text "x\<^isub>i"} is not in @{text "rhs"}\\

  1678   $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\

  1643   $\bullet$ & @{text "\<pi> \<bullet> x\<^isub>i"} provided @{text "x\<^isub>i"} is in @{text "rhs"} without a binding function\\

  1679   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\

  1644   $\bullet$ & @{text "\<pi> \<bullet>bn\<^isub>k x\<^isub>i"} provided @{text "bn\<^isub>k x\<^isub>i"} is @{text "rhs"}\\

  1680   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise

  1645   \end{tabular}

  1681   \end{tabular}

  1646   \end{center}

  1682   \end{center}

  1647 

  1683   

  1648   The definition of @{text "\<bullet>bn"} is respectful (simple induction) so we can lift it

  1684   \noindent

  1649   and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this definition is correct is:

  1685   Using the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to alpha

  1650 

  1686   equated terms. We can then prove

  1651 %% We could get this from ExLet/perm_bn lemma.

  1687 

  1652   \begin{lemma} For every bn function  @{text "bn\<^isup>\<alpha>\<^isub>i"},

  1688   \begin{lemma} Given a binding function @{text "bn\<^sup>\<alpha>"}. Then 

  1653   \begin{eqnarray}

  1689   {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"} and {\it ii)}

  1654   @{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i x"} & = & @{text "bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}\\

  1690   for all permutations @{text p},  @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.

  1655   @{text "fv_bn\<^isup>\<alpha>\<^isub>i x"} & = & @{text "fv_bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}

  1656   \end{eqnarray}

  1658   \begin{proof} By induction on the lifted type it follows from the definitions of

  1692 

  1659     permutations on the lifted type and the lifted defining equations of @{text "\<bullet>bn"}

  1693   \begin{proof} 

  1660     and @{text "fv_bn"}.

  1694   By induction on @{text x}. The equation follow by simple unfolding 

  1695   of the definitions. 

  1663 *}

  1698   This allows is to strengthen the induction principles. We will explain

  1664 

  1699   the details with the @{text "Let"} term-constructor from \eqref{letpat}.

  1665 section {* Strong Induction Principles *}

  1700   Instead of establishing the implication 

  1666 

  1701 

  1667 text {*

  1702   \begin{center}

  1703   a

  1704   \end{center}

  1705 

  1706   \noindent

  1707   from the weak induction principle. 

  1708 

  1709 

  1802   To our knowledge the earliest usage of general binders in a theorem prover

  1846   To our knowledge, the earliest usage of general binders in a theorem prover

  1805   de-Bruijn indices representation. Since type schemes contain only a single

  1849   de-Bruijn indices representation. Since type schemes of W contain only a single

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

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

  1812   kinds of de-Bruijn indices comes for free in any modern theorem prover as

  1856   representations of bindings comes for free in the theorem provers Isabelle/HOL and

  1813   the corresponding term-calculi can be implemented as ``normal'' datatypes.

  1857   Coq, for example, as the corresponding term-calculi can be implemented as ``normal''

  1814   However, in both approaches, it seems difficult to achieve our fine-grained

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

  1815   control over the ``semantics'' of bindings (i.e.~whether the order of

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

  1816   binders should matter, or vacuous binders should be taken into account). To

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

  1817   do so, requires additional predicates that filter out some unwanted

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

  1818   terms. Our guess is that they results in rather intricate formal reasoning.

  1862   unwanted terms. Our guess is that such predicates results in rather

  1819   Also one motivation of our work is that the user does not need to know

  1863   intricate formal reasoning.

  1820   anything at all about de-Bruijn indices, which are of course visible in the

  1821   usual de-Bruijn indices representations, but also in locally nameless

  1822   representations.

  1825   (HOAS), for example implemented in the Twelf system. This representation

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

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

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

  1829   are represented in this work. Judging from the submitted Twelf-solution for the

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

  1830   POPLmark challenge, HOAS cannot easily deal with binding

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

  1831   constructs where the number of bound variables is not fixed. For example in

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

  1832   the second part of this challenge, @{text "Let"}s involve patterns that bind

  1873   example in the second part of this challenge, @{text "Let"}s involve

  1833   multiple variables at once. In such situations, HOAS representations have to 

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

  1834   resort, essentially, to the iterated-single-binders-approach with all the unwanted

  1875   representations have to resort to the iterated-single-binders-approach with

  1835   consequences for reasoning about terms. 

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

  1836 

  1877 

  1837   Two formalisations involving general binders have been performed in older

  1878   Two formalisations involving general binders have also been performed in older

  1839   use also the approach based on iterated single binders. Our experience with the

  1880   use the approach based on iterated single binders. Our experience with

  1840   latter formalisation has been disappointing. The major pain arises

  1881   the latter formalisation has been disappointing. The major pain arose from

  1841   from the need to ``unbind'' variables. This can be done in one step with our

  1882   the need to ``unbind'' variables. This can be done in one step with our

  1843   iteration with single binders. The resulting formal reasoning is rather

  1884   iteration with single binders. The resulting formal reasoning turned out to

  1844   unpleasant. The hope is that the extension presented in this paper is a

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

  1845   substantial improvement.  

  1886   is a substantial improvement.

  1847   The most closely related work is the description of the Ott-tool

  1888   The most closely related work to the one presented here is the Ott-tool \cite{ott-jfp}. This tool is a

  1848   \cite{ott-jfp}. This tool is a nifty front-end for creating \LaTeX{}

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

  1849   documents from term-calculi specifications. For a subset of the

  1890   term-calculi involving general binders. For a subset of the specifications, Ott can also generate

  1850   specifications, Ott can also generate theorem prover code using a raw

  1891   theorem prover code using a raw representation of terms, and in Coq also a

  1851   representation and in Coq also a locally nameless representation for

  1892   locally nameless representation. The developers of this tool have also put

  1852   terms. The developers of this tool have also put forward (on paper) a

  1893   forward (on paper) a definition for alpha-equivalence of terms that can be

  1853   definition for the notion of alpha-equivalence of the term-calculi that can

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

  1854   be specified in Ott.  This definition is rather different from ours, not

  1895   any nominal techniques. Although we were heavily inspired by their syntax,

  1855   using any nominal techniques; it also aims for maximum expressivity,

  1896   their definition of alpha-equivalence is unsuitable for our extension of

  1856   covering as many binding structures from programming language research as

  1857   possible.  Although we were heavily inspired by their syntax, their

  1858   definition of alpha-equivalence was no use at all for our extension of

  1862   sense for our alpha-equated terms. It also allows empty types that have

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

  1863   no meaning in a HOL-based theorem prover. 

  1901   meaning in a HOL-based theorem prover.

  1864 

  1902 

  1865   Because of how we set up our definitions, we had to impose some

  1903   Because of how we set up our definitions, we had to impose restrictions,

  1866   restrictions, like excluding overlapping deep binders, which are not present

  1904   like excluding overlapping deep binders, that are not present in Ott. Our

  1867   in Ott. Our expectation is that we can still cover many interesting term-calculi

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

  1868   from programming language research, like Core-Haskell. For features of Ott,

  1906   programming language research, for example Core-Haskell. For prviding support

  1869   like subgrammars, the datatype infrastructure in Isabelle/HOL is

  1907   of neat features in Ott, such as subgrammars, the existing datatype

  1870   unfortunately not yet powerful enough to implement them. On the other hand 

  1908   infrastructure in Isabelle/HOL is unfortunately not powerful enough. On the

  1871   we are not aware that Ott can make any distinction between our three 

  1909   other hand, we are not aware that Ott can make the distinction between our

  1872   different binding modes. Also, definitions for notions like free-variables 

  1910   three different binding modes. Also, definitions for notions like the free

  1873   are work in progress in Ott. Since Ott produces either raw representations

  1911   variables of a term are work in progress in Ott.

  1874   or locally nameless representations it can largely rely on the reasoning

  1875   infrastructure derived automatically by the theorem provers. In contrast,

  1876   have to make considerable effort to establish a reasoning infrastructure 

  1877   for alpha-equated terms. 

  1883   We have presented an extension for Nominal Isabelle in order to derive a

  1917   We have presented an extension of Nominal Isabelle for deriving

  1884   convenient reasoning infrastructure for term-constructors binding multiple

  1918   automatically a convenient reasoning infrastructure that can deal with

  1885   variables at once. This extension can deal with term-calculi such as

  1919   general binders, that is term-constructors binding multiple variables at

  1886   Core-Haskell. For such calculi, we can also derive strong induction

  1920   once. This extension has been tried out with the Core-Haskell

  1887   principles that have the usual variable already built in. At the moment we

  1921   term-calculus. For such general binders, we can also extend

  1888   can do so only with manual help, but future work will automate them

  1922   earlier work that derives strong induction principles which have the usual

  1889   completely.  The code underlying this extension will become part of the

  1923   variable convention already built in. At the moment we can do so only with manual help,

  1890   Isabelle distribution, but for the moment it can be downloaded from the

  1924   but future work will automate them completely.  The code underlying the presented

  1891   Mercurial repository linked at

  1925   extension will become part of the Isabelle distribution, but for the moment

  1926   it can be downloaded from the Mercurial repository linked at

  1895   We have left out a discussion about how functions can be defined

  1930   We have left out a discussion about how functions can be defined over

  1896   over alpha-equated terms with general binders. In earlier work \cite{UrbanBerghofer06}

  1931   alpha-equated terms that involve general binders. In earlier versions of Nominal

  1897   this turned out to be a thorny issue for  Nominal Isabelle.

  1932   Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue.  We

  1898   We hope to do better this time by using the function package that

  1933   hope to do better this time by using the function package that has recently

  1899   has recently been implemented in Isabelle/HOL and also by restricting

  1934   been implemented in Isabelle/HOL and also by restricting function

  1900   function definitions to equivariant functions (for such functions

  1935   definitions to equivariant functions (for such functions it is possible to

  1901   it is possible to provide more automation).

  1936   provide more automation).

  1902 

  1937 

  1903   There are some restrictions we imposed, like the absence of nested type

  1938   There are some restrictions we imposed in this paper, we like to lift in

  1904   definitions that allow one to specify the function kinds as 

  1939   future work. One is the exclusion of nested datatype definitions. Nested

  1905   @{text "TFun string (ty list)"} instead of the unfolded version

  1940   datatype definitions allow one to specify, for instance, the function kinds

  1906   @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}; such

  1941   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded

  1907   restrictions can be easily lifted. They essentially amount to a more

  1942   version @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}. For

  1908   clever implementation than we have at the moment. More interesting is 

  1943   them we need a more clever implementation than we have at the moment. 

  1909   lifting our restriction about overlapping deep binders. Given our

  1944 

  1910   current setup, we cannot deal with specifications such as

  1945   More

  1946   interesting is lifting our restriction about overlapping deep binders. Given

  1947   our current setup, we cannot deal with specifications such as

  1948 

  1921   where the deep binders @{text "bn(r)"} and @{text "bn(s)"} overlap.. 

  1959   where the deep binders @{text "bn(r)"} and @{text "bn(s)"} overlap. 

  1922   We would need to implement such bindings with alpha-equivalences like

  1960   The difficulty is that we would need to implement such overlapping bindings 

  1961   with alpha-equivalences like

  1937   first version cannot not work since it leaves unbound atoms that should be 

  1976   first version cannot work since it leaves some atoms unbound that should be 

  1941   On the other hand, such bindings can be made sense of \cite{SewellBestiary}.

  1980   On the other hand, such bindings can be made sense of informally \cite{SewellBestiary}.

  1942   This clearly needs more investigation.

  1981   This suggest there should be an approriate notion of alpha-equivalence.

  1982 

  1983   Another interesting line of investigation is whether we can go beyond the 

  1984   simple-minded form of binding function we adopted from Ott. At the moment, binding

  1985   functions can only return the empty set, a singleton atom set or unions

  1986   of atom sets (similarly for lists). It remains to be seen whether 

  1987   properties like \eqref{bnprop} provide us with means to support more interesting

  1988   binding functions. 

  1989 

  1945   imagine that the here is a mode \isacommand{bind\_\#list} with the associated

  1992   imagine that there is need for a binding mode \isacommand{bind\_\#list} with an associated

  1946   alpha-equivalence definition

  1993   alpha-equivalence definition as follows:

  1960   In this definition we added the requirement that all bound variables 

  2007   In this definition we added the requirement that all bound variables in a

  1961   in a list are distinct. We can imagine applications for such a notion

  2008   list are distinct. Once we feel confident about such binding modes, our implementation 

  1962   of binding, but have not explored them yet. Our implementation can 

  2009   can be easily extended to accommodate them.

  1963   easily extended to accommodate further binding modes.

  1970   also for patiently explaining some of the finer points about the abstract 

  2016   also for patiently explaining some of the finer points of the work on the Ott-tool. We

  1971   definitions and about the implementation of the Ott-tool. We