0

I have to prove "1 not True == False" in Lambda Calculus which is (left side of eq):

(λs.λz.s z) (λx.x (λt.λf.f)(λt.λf.t))(λt.λf.t)

I come to this step: (which I know is still correct, just brackets could be wrong but I would not know how do get further with different brackets as well)

λf.(λt.λf.f) (λt.λf.t)

So how does one come from here to λt.λf.f (False)?

As far as I know there are no special rules that let me shorten anything like that...

Peybro
  • 103
  • 2
    How do 1 and not translate here? And what would 1 not True mean at all? Anyway, formally, applying $\lambda x$ with $x=F=(\lambda t.\lambda f.f)$ we get the result. – Berci Mar 08 '22 at 21:03
  • From the task 1 = λs.λz.s z and not = λx.x (λt.λf.f)(λt.λf.t). I don't understand what you mean exactly - how do I apply λx with x in λf.(λt.λf.f) (λt.λf.t) – Peybro Mar 09 '22 at 09:25

1 Answers1

2

Let's write $T:=\lambda t.\, \lambda f.\,t$ and $F:=\lambda t. \,\lambda f.\,f$, and $N$ for the middle part: $N:=\lambda x.\,x\,F\,T$.

Then our term looks like $$(\lambda s.\,\lambda z.\,s\,z)\,N\,T$$ and $\beta$-reduction leads it to $N\,T$ since it substitutes $N$ for $s$ and $T$ for $z$ while removing their $\lambda$-prefix.

Writing it further, $$N\,T\ =\ (\lambda x.\,x\,F\,T)\,T\ \overset\beta\leadsto\ T\,F\,T\ =$$ $$=\ (\lambda t.\,\lambda f.\,t)\,F\,T\ \overset\beta\leadsto\ F$$ where the last step (trickily) substitutes $F$ for $t$ and $T$ for $f$.

Berci
  • 90,745
  • Thanks, I like this 'short way' style instead of writing out the whole term - I think I'll keep this. But I'm still not sure about the last step: the substitution F for t is clear, but how to substitute T for f - what is the tricky part here? I mean there is no f in (λf.(λt.λf.f))T I could use for the first f, right?! – Peybro Mar 11 '22 at 08:31
  • 1
    The 'trick' is that the letters and their substituted terms are just the opposite, but this is simply because of the order of $\lambda$-bounded variables: in the case of $(\lambda t.,\lambda f.,t),A,B$ we replace $A$ for $t$ and $B$ for $f$, and indeed as $f$ is not present in the term itself (only beside $\lambda$), this would $\beta$-reduce to $A$ exactly, while $B$ would be simply ignored. Here we apply this with $A=F$ and $B=T$. – Berci Mar 11 '22 at 17:31
  • I see. I didn't know an argument can be ignored if it is not called inside the function but it makes sense if I think aubout it.. Thanks for the explanation! – Peybro Mar 12 '22 at 12:12