3
$\begingroup$

Does anyone have an idea how to prove in lambda calculus that bool contains two terms? I am quite new to it and I haven't succeeded in doing so. I came up with two terms so far, which would guarantee existence: $\lambda x_{\alpha}.\lambda y_{\alpha}.x$ and $\lambda x_{\alpha}.\lambda y_{\alpha}.y$. These terms are clearly of the type $Bool$.

But how can we prove that there are no other ones? I have tried induction on terms, induction on types, but everything failed so far. Any tips are welcome, thanks.

$\endgroup$
3
$\begingroup$

Your theorem statement has "atomic" carrying a decent load. You may want to consider what (if anything) about "atomic types" make this theorem true. In particular, you can "generalize" the statement.

At any rate, you want to do an induction on normal forms. The statement you want to prove can be formulated as $$\forall t\in \mathcal{N}. t\text{ has type } Bool\iff(t = \lambda x_\alpha.\lambda y_\alpha. x \lor t = \lambda x_\alpha.\lambda y_\alpha. y)$$ where $\mathcal{N}$ is the set of ($\alpha$-equivalence classes of) normal forms and (thus) equality, here, means $\alpha$-equivalence. $\mathcal{N}$ is roughly an inductively defined set and so to prove a statement about all its elements requires induction. However, since the terms include binding forms things get a bit hairier. In particular, and this will be a common move, you need to strengthen the induction hypothesis to hold for open terms. So instead of doing induction over normal forms, you want to do induction over "normal-forms-in-context". (We can simplify significantly for this particular problem [how?], but I will work more generally.) What's happening is that closed terms (and normal forms) do not form an inductively defined set (at least not in a natural way), but terms-in-context do.

Given a list of types called $\Gamma$, we can define $\mathtt{vars}(\Gamma)\equiv\{x^i\mid i < \#\Gamma\}$ to be a corresponding set of variables where $\#\Gamma$ is the length of $\Gamma$. Finally, define $$\alpha^\Gamma \equiv \begin{cases}\alpha, & \Gamma = \cdot\\\beta\to\alpha^\Delta, & \Gamma = \beta,\Delta\end{cases}$$ and $$\mathtt{abstract}(\Gamma,x)\equiv\begin{cases}x, &\Gamma = \cdot\\\lambda x^{\#\Delta}_\beta.\mathtt{abstract}(\Delta,x), & \Gamma = \beta,\Delta\end{cases}$$ The strengthened (but not quite correct) induction hypothesis is now $$\forall \Gamma.\forall t\in \mathcal{N}.\ \cdot\vdash t:\alpha^\Gamma\iff t \in\{\mathtt{abstract}(\Gamma,x)\mid x \in \mathtt{vars}(\Gamma)\land \Gamma\vdash x:\alpha\}$$ where $\Gamma\vdash t : \alpha$ means $t$ has type $\alpha$ in context $\Gamma$. As stated, this is not true, but if we restrict $\Gamma$ to lists of "atomic" types, it is. The original theorem is recovered in the $\alpha,\alpha,\cdot$ case.

$\endgroup$
  • $\begingroup$ The main change is that we only need to consider lists of types containing only $\alpha$ at which point we only need to know the length of the list. Thus all the recursions and the induction of $\Gamma$ can be replaced with recursions/induction of the number of $\alpha$'s to the left of the arrow in the type. This is mostly a notational savings, though we can drop the $\Gamma\vdash x:\alpha$ condition. For example, instead of $\alpha^\Gamma$, we'd have $$\alpha^n\equiv \begin{cases}\alpha, & n= 0 \\ \alpha\to\alpha^m, & n= m+1\end{cases}$$ $\endgroup$ – Derek Elkins Mar 21 '17 at 7:02
  • $\begingroup$ Yes, right nested arrow types, i.e. $\alpha$, $\alpha\to\alpha$, $\alpha\to(\alpha\to\alpha)$, etc. Unrelatedly, I made some significant but small corrections, see the edits. Also, technically I could get rid of $\mathcal{\Gamma}$ and just use $\mathcal{N}$, or I could get rid of $\alpha^\Gamma$ and keep $\mathcal{N}_\Gamma$ and say $\Gamma\vdash t:\alpha$ which would require a lemma $\Gamma\vdash t:\alpha \iff \cdot\vdash t:\alpha^\Gamma$ which is usually true (via $\eta$-conversion) to connect it to the original problem statement $\endgroup$ – Derek Elkins Mar 21 '17 at 7:39
  • $\begingroup$ Bingo. Yes, you do. Your original statement is false if "atomic" doesn't exclude types with normal forms. For example, if $\alpha=\mathbb{N}$ then there is an infinite number of normal forms. If $\alpha=1$ (the unit type) and you have $\eta$-conversion for it, then $\lambda x_1.\lambda y_1.x = \lambda x_1.\lambda y_1.\langle\rangle = \lambda x_1.\lambda y_1.y$ and you only have one $\beta\eta$-normal form. So what we really need from $\alpha$ is for it to not have any normal form terms. $\endgroup$ – Derek Elkins Mar 21 '17 at 8:10
  • $\begingroup$ It's over normal forms because we want to know something about all normal forms (of the appropriate type), namely that they are contained in a particular finite set. If the statement had been about arbitrary terms, then it would have been an induction over terms-in-context. That said, there are an infinite number of (arbitrary) terms for any inhabited type. For any term $t$ of that type, $(\lambda x_\alpha.x)t$ is another term. We usually identify values of a type with the normal forms at that type. Non-norrmal terms are essentially intermediate stages of calculation in this view. $\endgroup$ – Derek Elkins Mar 21 '17 at 8:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy