-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