Skip to main content
7 of 8
added 14 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$, why? Because there are no free $y$ variables in $true \equiv (\lambda x~ y. x)$. This is rule-(e) for substitution.

Definition 1.12 (Substitution) For any $M, N, x$, define $[N/x]M$ to be the result of substituting $N$ for every free occurrence of $x$ in $M$, and changing bound variables to avoid clashes. The precise definition is by induction on $M$, as follows (after [CF58, p.94]).

(a) $[N/x]x \equiv N$

(b) $[N/x]a \equiv a$ for all atoms $a \not \equiv x$

(c) $[N/x](PQ) \equiv ([N/x]P)([N/x]Q)$

(d) $[N/x](\lambda x.P) \equiv (\lambda x.P)$

(e) $[N/x](\lambda y.P) \equiv P$ if $x \not \in FV(P)$.

(f) $[N/x](\lambda y.P) \equiv \lambda y. [N/x]P$ if $x \in FV(P)$ and $y \not \in FV(N)$.

(g) $[N/x](\lambda y.P) \equiv \lambda z. [N/x][z/y]P$ if $x \in FV(P)$ and $y \in FV(N)$.

Note: $FV(P)$ stands for the set of free variables of $P$.

Schonfinkel
  • 1.5k
  • 4
  • 13
  • 25