Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

======================= 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.

share|improve this question

2 Answers 2

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.

share|improve this answer
    
a) $(bcF)dF$ and $b(cdF)F$ are not closed terms; b) $b$ and $c$ must be of type boolean? –  yousong Oct 7 '11 at 5:24
    
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? –  yousong Oct 7 '11 at 5:31
    
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. –  user13300 Oct 7 '11 at 12:01
    
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. –  yousong Oct 7 '11 at 12:11
    
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. –  user13300 Oct 7 '11 at 12:20

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.