# Proving using Beta Reductions (Lambda Calculus)

I am working on proving something by using Lambda Calculus and Beta Reductions, and I was following along a tutorial on another problem and attempted to carry over the knowledge onto a different problem and I am a little confused on the last step.

The problem is to prove $\textbf{or true false}$.

Here are my steps: (if there are any improvements or errors please let me know)

Step 1: Begin writing the identity for OR along with the parameters true and false.

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

Step 2: Replace the $x$ terms with true.

$(\lambda y.(true ~ true ~ y)) ~ false$

Step 3: Replace the $y$ terms with false.

$true ~ true ~ false \equiv (true ~ true) false$

Step 4: (I am a little shaky on this step, however I saw it done this way). Expand on one of the terms by replacing with it's identity. So we break true into:

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

Step 5: Again, replace x with true.

$(\lambda y.true) ~ false$

Step 6: $\textbf{this is the step i am most confused on}$ It looks as if since there is no way we can distribute the false to the y we simply just drop both of them since it is not an applicable function. Which then returns you with true, which stands to reason that true or false is true.

Can anyone shed light on Step 6? Or if I am correct and thats the rationale please let me know!

• I'm just going to change my answer so it answers the actual problem, which is step 6. Nov 30, 2016 at 1:00
• You should think of $\lambda y.\ z$ as a function which takes an input, discards it, and always return $z$. This is the constantly-$z$ function, in a sense. A function argument $y$ does not have to be used in its body.
– chi
Dec 1, 2016 at 10:50

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

• Sorry! Corrected to what you asked. Nov 30, 2016 at 0:32
• perfect, thanks for your help, just wanted to make sure my rationale was correct. Nov 30, 2016 at 0:33
• I'm not sure I entirely agree with this answer: the important part is that there are no free $y$ variables in $\mathrm{true}$, not in $\lambda y.\mathrm{true}$ (which cannot have free $y$ variables anyways). It's also probably useful to note that rule (e) is redundant with respect to the other rules (which is a very good exercise to understand substitution in the $\lambda$-calculus).
– cody
Dec 1, 2016 at 15:41