1141 

  1141   %

  1142   \begin{center}

  1142   \begin{equation}\label{ceqvt}

  1144   \end{center}

  1144   \end{equation}

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

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

  1467   the reasoning infrastructure for the types the user specified. For this we first

  1467   introducing the reasoning infrastructure for the alpha-equated types the

  1468   have to show that the alpha-equivalence relations defined in the previous

  1468   user specified. We sketch in this section the facts we need for establishing

  1469   section are indeed equivalence relations. 

  1469   this reasoning infrastructure. We first have to show that the

  1470 

  1470   alpha-equivalence relations defined in the previous section are indeed

  1471   \begin{lemma} 

  1471   equivalence relations.

  1472 

  1473   \begin{lemma}\label{equiv} 

  1526   analysing the definition of @{text "\<approx>ty"}. For this to succed we have to establish an

  1528   analysing the definition of @{text "\<approx>ty"}. For this to succeed we have to establish an

  1537   Having established respectfullness for every raw term-constructor, the 

  1539   Having established respectfulness for every raw term-constructor, the 

  1538   quotient package will automaticaly deduce \eqref{distinctalpha} from \eqref{distinctraw}.

  1540   quotient package will automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.

  1560 

  1562   Next we lift the permutation operations defined in \eqref{ceqvt} for

  1561 

  1563   the raw term-constructors @{text "C"}. These facts contain, in addition 

  1562 To lift

  1564   to the term-constructors, also permutations operations. Therefore

  1563   the raw definitions to the quotient type, we need to prove that they

  1565   we have to know that permutation operations are respectful 

  1564   \emph{respect} the relation. We follow the definition of respectfullness given

  1566   w.r.t.~alpha-equivalence, which amounts to knowing that the 

  1565   by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition

  1567   alpha-equivalence relations are equivariant, which we established 

  1566   is that when a function (or constructor) is given arguments that are

  1568   in Lemma~\ref{equiv}. As a result we can add the equations

  1567   alpha-equivalent the results are also alpha equivalent. For arguments that are

  1569   

  1568   not of any of the relations taken into account, equivalence is replaced by

  1570   \begin{equation}\label{ceqvt}

  1569   equality. In particular the respectfullness condition for a @{text "bn"}

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

  1570   function means that for alpha equivalent raw terms it returns the same bound

  1572   \end{equation}

  1571   names. Thanks to the restrictions on the binding functions introduced in

  1573 

  1572   Section~\ref{sec:alpha} we can show that are respectful.

  1574   \noindent

  1573 

  1575   to our infrastructure. In a similar fashion we can lift the equations

  1574   \begin{lemma} The functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"}, @{text "fv_ty\<^isub>1 \<dots> fv_ty\<^isub>n"},

  1576   characterising our free-variable functions and the binding functions. 

  1575   the raw constructors, the raw permutations and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are

  1577   The necessary respectfulness lemmas are

  1576   respectful w.r.t. the relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>n"}.

  1578   %

  1579   \begin{equation}\label{fnresp}

  1580   \mbox{%

  1581   \begin{tabular}{l}

  1582   @{text "x \<approx>ty y"} implies @{text "fv_ty x = fv_ty y"}\\

  1583   @{text "x \<approx>ty y"} implies @{text "bn x = bn y"}

  1584   \end{tabular}}

  1585   \end{equation}

  1586 

  1587   \noindent

  1588   which can be established by induction on @{text "\<approx>ty"}. While the first

  1589   kind of lemma is always ensured by way of how we defined the free variable

  1590   functions, the second does not hold in general. It only if the @{text bn}-functions 

  1591   do not return any atom that is also bound. Hence our restriction imposed

  1592   on the binding functions that excludes this possibility. 

  1593 

  1594   Having the facts \eqref{fnresp} at our disposal, we can finally lift the

  1595   definitions that characterise when two terms of the form

  1596 

  1597   \begin{center}

  1598   @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}

  1599   \end{center}

  1600 

  1601   \noindent

  1602   are alpha-equivalent. This gives us conditions when the corresponding

  1603   alpha-equated terms are equal, namely

  1604 

  1605   \begin{center}

  1606   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}

  1607   \end{center}

  1608 

  1609   \noindent

  1610   We call these conditions as \emph{quasi-injectivity}. Except for one definition we have

  1611   to lift in the next section, this completes

  1612   the lifting part of establishing the reasoning infrastructure. From

  1613   now on we can ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only

  1614   reason with @{text "ty\<AL>\<^bsub>1..n\<^esub>"}

  1615 

  1616   We can first show that the free-variable function and binding functions

  1617   are equivariant, namely

  1618 

  1619   \begin{center}

  1620   \begin{tabular}{rcl}

  1621   @{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\

  1622   @{text "p \<bullet> (bn\<^sup>\<alpha> x)"}    & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}

  1623   \end{tabular}

  1624   \end{center}

  1625 

  1626   \noindent

  1627   These facts can be established by structural induction over the @{text x}.

  1628 

  1629   Until now we have not yet derived any fact about the support of the 

  1630   alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can

  1631   show for every term-constructor @{text "C\<^sup>\<alpha>"} that 

  1632 

  1633   \begin{center}

  1634   @{text "supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}

  1635   \end{center}

  1636  

  1637   \noindent

  1638   holds. This together with Property~\ref{supportsprobs} allows us to show

  1639  

  1640 

  1641   \begin{center}

  1642   @{text "finite (supp x\<^isub>i)"}

  1643   \end{center}

  1644 

  1645   \noindent

  1646   by mutual structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types 

  1647   @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in 

  1648   @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\<AL>\<^bsub>1..n\<^esub>"}.

  1649 

  1650   \begin{lemma} For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that 

  1651   @{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds.

  1578   \begin{proof} Respectfullness of permutations is a direct consequence of

  1653 

  1579   equivariance.  All other properties by induction on the alpha-equivalence

  1580   relation.  For @{text "bn"} the thesis follows by simple calculations thanks

  1581   to the restrictions on the binding functions. For @{text "fv"} functions it

  1582   follows using respectfullness of @{text "bn"}. For type constructors it is a

  1583   simple calculation thanks to the way alpha-equivalence was defined. For @{text

  1584   "alpha_bn"} after a second induction on the second relation by simple

  1585   calculations.  \end{proof}

  1586 

  1587   With these respectfullness properties we can use the quotient package

  1588   to define the above constants on the quotient level. We can then automatically

  1589   lift the theorems that talk about the raw constants to theorems on the quotient

  1590   level. The following lifted properties are proved:

  1591 

  1592   \begin{center}

  1593   \begin{tabular}{cp{7cm}}

  1594 %skipped permute_zero and permute_add, since we do not have a permutation

  1595 %definition

  1596   $\bullet$ & permutation defining equations \\

  1597   $\bullet$ & @{term "bn"} defining equations \\

  1598   $\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\

  1599   $\bullet$ & induction. The induction principle that we obtain by lifting

  1600     is the weak induction principle, just on the term structure \\

  1601   $\bullet$ & quasi-injectivity. This means the equations that specify

  1602     when two constructors are equal and comes from lifting the alpha

  1603     equivalence defining relations\\

  1604   $\bullet$ & distinctness\\

  1605 %may be skipped

  1606   $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\

  1607   \end{tabular}

  1608   \end{center}

  1609 

  1610   Until now we have not said anything about the support of the

  1611   defined type. This is because we could not use the general definition of

  1612   support in lifted theorems, since it does not preserve the relation.

  1613   Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"},

  1614   since the @{term "x"} is bound. On the raw level, before the binding is

  1615   introduced the term has the support equal to @{text "{x}"}. 

  1616 

  1617   To show the support equations for the lifted types we want to use the

  1618   Theorem \ref{suppabs}, so we start with showing that they have a finite

  1619   support.

  1620 

  1621   \begin{lemma} The types @{text "ty\<^isup>\<alpha>\<^isub>1 \<dots> ty\<^isup>\<alpha>\<^isub>n"} have finite support.

  1622   \end{lemma}

  1624   By induction on the lifted types. For each constructor its support is

  1655   The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case

  1625   supported by the union of the supports of all arguments. By induction

  1656   we unfold the definition of @{text "supp"}, move the swapping inside the 

  1626   hypothesis we know that each of the recursive arguments has finite

  1657   term-constructors and the use the quasi-injectivity lemmas in order to complete the

  1627   support. We also know that atoms and finite atom sets and lists that

  1658   proof.

  1628   occur in the constructors have finite support. A union of finite

  1629   sets is finite thus the support of the constructor is finite.

  1632 % Very vague...

  1661   \noindent

  1633   \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"}

  1662   To sum up this section, we established a reasoning infrastructure

  1634    of this type:

  1663   for the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"} 

  1635   \begin{equation}

  1664   by first lifting definitions from the raw level to the quotient level and

  1636   @{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}.

  1665   then establish facts about these lifted definitions. All necessary proofs

  1637   \end{equation}

  1666   are generated automatically by custom ML-code. This code can deal with 

  1638   \end{lemma}

  1667   specifications as shown in Figure~\ref{nominalcorehas} for Core-Haskell.  

  1639   \begin{proof}

  1640   We will show this by induction together with equations that characterize

  1641   @{term "fv_bn\<^isup>\<alpha>\<^isub>"} in terms of @{term "alpha_bn\<^isup>\<alpha>"}. For each of @{text "fv_bn\<^isup>\<alpha>"}

  1642   functions this equation is:

  1643   \begin{center}

  1644   @{term "{a. infinite {b. \<not> alpha_bn\<^isup>\<alpha> ((a \<rightleftharpoons> b) \<bullet> x) x}} = fv_bn\<^isup>\<alpha> x"}

  1645   \end{center}

  1646 

  1647   In the induction we need to show these equations together with the goal

  1648   for the appropriate constructors. We first transform the right hand sides.

  1649   The free variable functions are applied to theirs respective constructors

  1650   so we can apply the lifted free variable defining equations to obtain

  1651   free variable functions applied to subterms minus binders. Using the

  1652   induction hypothesis we can replace free variable functions applied to

  1653   subterms by support. Using Theorem \ref{suppabs} we replace the differences

  1654   by supports of appropriate abstractions.

  1655 

  1656   Unfolding the definition of supports on both sides of the equations we

  1657   obtain by simple calculations the equalities.

  1658   \end{proof}

  1659 

  1660   With the above equations we can substitute free variables for support in

  1661   the lifted free variable equations, which gives us the support equations

  1662   for the term constructors. With this we can show that for each binding in

  1663   a constructors the bindings can be renamed. To rename a shallow binder

  1664   or a deep recursive binder a permutation is sufficient. This is not the

  1665   case for a deep non-recursive bindings. Take the term

  1666   @{text "Let (ACons x (Vr x) ANil) (Vr x)"}, representing the language construct

  1667   @{text "let x = x in x"}. To rename the binder the permutation cannot

  1668   be applied to the whole assignment since it would rename the free @{term "x"}

  1669   as well. To avoid this we introduce a new construction operation

  1670   that applies a permutation under a binding function.

  1671 

  1672 *}

  1673 

  1674 section {* Strong Induction Principles *}

  1675 

  1676 text {*

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

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

  1679   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"},

  1680   the induction hypothesis requires us to establish the implication

  1681   %

  1682   \begin{equation}\label{weakprem}

  1683   @{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)"} 

  1684   \end{equation}

  1685 

  1686   \noindent

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

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

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

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

  1691 

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

  1693   strengthening weak induction principles for terms containing single

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

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

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

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

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

  1699   additional notion of permuting deep binders. 

  1700 

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

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

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

  1704   %

  1705   \begin{center}

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

  1707   \end{center}

  1708 

  1709   \noindent

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

  1711   %

  1712   \begin{center}

  1713   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}

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

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

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

  1717   \end{tabular}

  1718   \end{center}

  1719   

  1720   \noindent

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

  1722   equated terms. We can then prove

  1723 

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

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

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

  1727   \end{lemma}

  1728 

  1729   \begin{proof} 

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

  1731   of the definitions. 

  1732   \end{proof}

  1733 

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

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

  1736   Instead of establishing the implication 

  1737 

  1738   \begin{center}

  1739   @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}

  1740   \end{center}

  1741 

  1742   \noindent

  1743   from the weak induction principle, we will show that it is sufficient

  1744   to establish

  1745   

  1746   \begin{center}

  1747   \begin{tabular}{l}

  1748   @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\

  1749   \hspace{5mm}@{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c \<and>"}\\

  1750   \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\

  1751   \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}

  1752   \end{tabular}

  1753   \end{center}

  1754 

  1755 

  1756   With the help of @{text "\<bullet>bn"} functions defined in the previous section

  1757   we can show that binders can be substituted in term constructors. We show

  1758   this only for the specification from Figure~\ref{nominalcorehas}. The only

  1759   constructor with a complicated binding structure is @{text "ACons"}. For this

  1760   constructor we prove:

  1761   \begin{eqnarray}

  1762   \lefteqn{@{text "supp (Abs_lst (bv pat) trm) \<sharp>* \<pi> \<Longrightarrow>"}} \nonumber \\

  1763   & & @{text "ACons pat trm al = ACons (\<pi> \<bullet>bv pat) (\<pi> \<bullet> trm) al"} \nonumber

  1764   \end{eqnarray}

  1765 

  1766   \noindent With the Property~\ref{avoiding} we can prove a strong induction principle

  1767   which we show again only for the interesting constructors in the Core Haskell

  1768   example. We first show the weak induction principle for comparison:

  1769 

  1770 \begin{equation}\nonumber

  1771 \infer

  1772 {

  1773   \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}

  1774 }{

  1775   \begin{tabular}{cp{7cm}}

  1776 %%  @{text "P1 KStar"}\\

  1777 %%  @{text "\<forall>tk1 tk2. \<^raw:\big(>P1 tk1 \<and> P1 tk2\<^raw:\big)> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\

  1778 %%  @{text "\<dots>"}\\

  1779   @{text "\<forall>v ty t1 t2. \<^raw:\big(>P3 ty \<and> P7 t1 \<and> P7 t2\<^raw:\big)> \<Longrightarrow> P7 (Let v ty t1 t2)"}\\

  1780   @{text "\<forall>p t al. \<^raw:\big(>P9 p \<and> P7 t \<and> P8 al\<^raw:\big)> \<Longrightarrow> P8 (ACons p t al)"}\\

  1781   @{text "\<dots>"}

  1782   \end{tabular}

  1783 }

  1784 \end{equation}

  1785 

  1786 

  1787   \noindent In comparison, the cases for the same constructors in the derived strong

  1788   induction principle are:

  1789 

  1790 \begin{equation}\nonumber

  1791 \infer

  1792 {

  1793   \begin{tabular}{cp{7cm}}

  1794   \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}\\

  1795   \textrm{ avoiding any atoms in a given }@{text "y"}

  1796   \end{tabular}

  1797 }{

  1798   \begin{tabular}{cp{7cm}}

  1799 %%  @{text "\<forall>b. P1 b KStar"}\\

  1800 %%  @{text "\<forall>tk1 tk2 b. \<^raw:\big(>\<forall>c. P1 c tk1 \<and> \<forall>c. P1 c tk2\<^raw:\big)> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\

  1801 %%  @{text "\<dots>"}\\

  1802   @{text "\<forall>v ty t1 t2 b. \<^raw:\big(>\<forall>c. P3 c ty \<and> \<forall>c. P7 c t1 \<and> \<forall>c. P7 c t2 \<and>"}\\

  1803   @{text "\<^raw:\hfill>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\

  1804   @{text "\<forall>p t al b. \<^raw:\big(>\<forall>c. P9 c p \<and> \<forall>c. P7 c t \<and> \<forall>c. P8 c al \<and>"}\\

  1805   @{text "\<^raw:\hfill>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\

  1806   @{text "\<dots>"}

  1807   \end{tabular}

  1808 }

  1809 \end{equation}

  1810 

  1811   

  1812 

  1813 *}

  1814 

  1815 text {*