Skip to main content
3 of 8
added 191 characters in body
Schonfinkel
  • 1.5k
  • 4
  • 13
  • 25

First let: $$ true = \lambda x ~ y . x $$ $$ false = \lambda x ~ y . y$$ $$ or = \lambda x ~ y .((x ~ true) y) $$

So this is what you wrote:

$$or ~ true ~ false \rhd_{\beta} true$$

$$ \Bigg ( \Big( \lambda x ~ y . (x ~ true) y \Big) true \Bigg) ~ false $$ $$ \Bigg ( \lambda y. \Big ((true ~ true) y \Big) \Bigg) false $$ $$ ((true ~ true) ~ false) $$

Unwrap $true$.

$$ \Big( (\lambda x ~ y . x) ~ true) \Big) ~ false $$ $$ \color{red}{(\lambda y . true) ~ false } \rhd true $$

In the red step, which is what's burdening you you're just consuming the $false$ symbol, why? Because there are no free $y$ variables in $\lambda y. true$.

Schonfinkel
  • 1.5k
  • 4
  • 13
  • 25