En härledning i λ
Vad sägs om en härledning som visar att efterföljaren till 0 är 1?
Givet har vi funktionen Succ:
Succ := (λwyx.y(wyx))
och heltalet 0:
0 := (λsz.z),
och vi ska visa att Succ 0 = 1:
S0 = (λwyx.y(wyx)) (λsz.z) = λyx.y((λsz.z)yx) = λyx.yx = 1.
Steg för steg:
Vi utgår från S0 = (λwyx.y(wyx)) (λsz.z):
1. Vi ska ‘beräkna’ funktionen, så vi använder substitution. w i funktionen ersätts med 0, dvs (λsz.z), vi får då kvar λyx.y((λsz.z)yx).
2. Nu appliceras den inre funktionen på y. Alla s ska ersättas med y, men det finns inga s i funktionskroppen, så kvar får vi λyx.y((λz.z)x).
3. Den kvarvarande inre funktionen är förståss identitetsfunktionen, applicerad på x, och vi får λyx.yx som är 1.
