-1
$\begingroup$

======================= Original Post ======================

In lambda calculus, we define the boolean operators as below: $$ AND \to \lambda{}pq.pq\boldsymbol{F} \to \lambda{}p.\lambda{}q.pq(\lambda{}x.\lambda{}y.y) $$ $$ OR \to \lambda{}p.\lambda{}q.pTq \to \lambda{}p.\lambda{}q.p(\lambda{}x.\lambda{}y.x)q $$ $$ NOT \to \lambda{}p.pFT \to \lambda{}p.p(\lambda{}x.\lambda{}y.y)(\lambda{}x.\lambda{}y.x) $$

How can I show that "$AND\ (AND\ b\ c)\ d$ " and "$AND\ b\ (AND\ c\ d)$ " have the same $\beta\eta$ normal form? I can only get: $$ AND\ (AND\ b\ c)\ d \to (bcF)dF$$ $$ AND\ b\ (AND\ c\ d) \to b(cdF)F$$ Any hints are appreciated. Actually, there are another two pairs of such terms: $$ NOT\ (NOT\ b)\ and\ b$$ $$ AND\ (NOT\ b)\ (NOT\ c)\ and\ NOT\ (AND\ b\ c)$$ The question is from exercise.10-13 of Reynolds' book "Theories of Programming Languages".

======================== Answer =========================

Thanks to Anton and Henning. The following definitions work out as expected: $$ AND \to \lambda{}pqxy.p(qxy)y $$ $$ OR \to \lambda{}pqxy.px(qxy) $$ $$ NOT \to \lambda{}pxy.pyx $$ For $NOT\ (NOT\ b)$ and $b$: $$ (\lambda{}pxy.pyx)((\lambda{}pxy.pyx)b) \to \lambda{}xy.((\lambda{}pxy.pyx)b)yx \to \lambda{}xy.(\lambda{}xy.byx)yx \to \lambda{}xy.(\lambda{}u.buy)x \to \lambda{}xy.bxy \to_\eta \lambda{}x.bx \to_\eta b $$

But why the original definitions doesn't reduce to the same $\beta\eta$ normal form still needs to be tackled.

2 Answers 2

1

I think you need some additional assumptions on what $b$, $c$ and $d$ can be. If they are arbitrary lambda terms, then your sought conclusion does not hold.

For example, let $b=\lambda pqrsx.x$. Then $$(bcF)dF \mathrel{\to^*_\beta} \lambda x.x$$ but $$b(cdF)F \mathrel{\rightarrow^*_\beta} \lambda rsx.x$$ and these two results are manifestly not $\beta\eta$-equivalent.

0

Two closed lambda expressions can be automatically checked for $\beta\eta$-convertibility when some normalizing strategy against $\beta\eta$-reduction have led to one and the same normal form for both of the given terms. Their normal forms then have to be literally equal or up to $\alpha$-conversion.

However, the same does not hold true for terms having free variables. For instance, such valid lambda expressions as $x$ and $y$ cannot be said to be equal in general case. But this is not the only show-stopper.

The other one is that even for arbitrary closed terms $M$ and $N$, $$\text{AND}\; M\; N \neq \text{AND}\; N\; M.$$

When both $M$ and $N$ are boolean or can be reduced to boolean normal form, then $\text{AND}$ can be indeed considered as some kind of a commutative operation. The requirement for both $M$ and $N$ to have a normal form is crucial. Otherwise, for $M \equiv F$ and $N \equiv \Omega$, $$\text{AND}\; M\; N \rightarrow F$$ while $$\text{AND}\; N\; M$$ does not have a normal form.

  • 0
    a) $(bcF)dF$ and $b(cdF)F$ are not closed terms; b) $b$ and $c$ must be of type boolean?2011-10-07
  • 0
    Typed lambda calculus has not been introduced yet in the book. Assuming it did, how that would affect the 'decidability' of $\beta\eta$ normal form?2011-10-07
  • 0
    Since b, c and d are not bounded, these terms are not closed. As for terms being boolean, it is nothing to do with types. It is about their possible values T and F. I recommend to postpone talking about decidability till this material has been passed as decidability is a specific property of lambda terms.2011-10-07
  • 0
    Sorry if I misused terminologies such as 'decidability'. Anyway, I think enumerating all possible values for terms is not an elegant way to show $\beta\eta$ equivalence. Thus we return to the original question of how an elegant reasoning can be possible.2011-10-07
  • 0
    Again, AND M N and AND N M need not be beta-eta-convertible for arbitrary M and N. These terms are (at least, not only) beta-eta-equivalent when both M and N can be reduced to T or F.2011-10-07
  • 0
    Thanks for your efforts, Anton, but I am still confused. Can you show me how $NOT\ (NOT\ b)$ and $b$ are equivalent in a formal and primitive way with your understanding?2011-10-07
  • 0
    (\cxy.c y x) ((\cst.c t s) b) = (\cxy.c y x) (\st.b t s) = \xy.(\st.b t s) y x = \xy.b x y = \x. (\y.(b x) y) = \x.b x = b.2011-10-07
  • 0
    I know the points now. Thanks!!2011-10-08
  • 0
    $ \lambda{}xy.(\lambda{}st.b\ t\ s)\ y\ x \to_* \lambda{}xy.b\ y\ x \to_\eta \lambda{}y.by \to_\eta b $2011-10-08