`roland`

ein bischen lambda-kalkuel...

(fuer alle die damit etwas anfangen koennen - alle anderen duerfen einfach nur die bunten farben dieser seite bewundern ;), oder diese einfuehrung in den lambda-kalkuel lesen)

(fuer das einfaerben der klammern hatte ich uebrigens einen kleinen "sklaven" namens colorparenth.pl)

vorgaenger

und hier ist mein vorgaenger: (nur echt mit der 42 !):
rkpred = \nsz.n(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)

und fuer alle, die das nicht glauben - und da beispiele ja bekanntermassen die anschaulichkeit verbessern - habe ich hier ein paar ausfuehrliche beispiele:

rkpred (\sz.z) =
= (\nsz.n(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)) (\uv.v)
= (\sz.(\uv.v)(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x))
= (\sz.((\a.az(\dc.czd))) (\xy.x))
= (\sz.(((\xy.x)z(\dc.czd))))
= (\sz.(((z))))
= \sz.z

rkpred (\sz.sz) =
= (\nsz.n(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)) (\uv.uv)
= (\sz.(\uv.uv)(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd))) (\xy.x))
= (\sz.(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((\a.az(\dc.czd)))(\xy.y))) (\xy.x))
= (\sz.(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) (((\xy.y)z(\dc.czd))))) (\xy.x))
= (\sz.(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((((\dc.czd)))))) (\xy.x))
= (\sz.(((((((\dc.czd))))(\ba.a(s(((((\dc.czd)))) 42 (\xy.x)))b)) )) (\xy.x))
= (\sz.(((((((\dc.czd))))(\ba.a(s((((((\xy.x) z 42))))))b)) )) (\xy.x))
= (\sz.(((((((\dc.czd))))(\ba.a(s((((((z)))))))b)))) (\xy.x))
= (\sz.(((((((\c.cz(\ba.a(s((((((z)))))))b)))))))) (\xy.x))
= (\sz.((((((((\xy.x)z(\ba.a(s((((((z)))))))b)))))))))
= (\sz.((((((((z)))))))))
= \sz.z

rkpred (\sz.s(s(z))) =
= (\nsz.n(\p(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)) (\uv.u(uv))
= (\sz.(\uv.u(uv))(\p(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(\a.az(\dc.czd)))) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)))) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((\a.az(\dc.czd)))(\xy.y)))) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) (((\xy.y)z(\dc.czd)))))) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((((\dc.czd))))))) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(((((((\dc.czd))))(\ba.a(s(((((\dc.czd)))) 42 (\xy.x)))b))))) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(((((((\dc.czd))))(\ba.a(s((((((\xy.x) z 42))))))b))))) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(((((((\dc.czd))))(\ba.a(s((((((z)))))))b))))) (\xy.x))
= (\sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(((((((\c.cz(\ba.a(s((((((z)))))))b))))))))) (\xy.x))
= (\sz.(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((((((((\c.cz(\ba.a(s((((((z)))))))b))))))))(\xy.y)))) (\xy.x))
= (\sz.(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) (((((((((\xy.y)z(\ba.a(s((((((z)))))))b))))))))))) (\xy.x))
= (\sz.(((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((((((((((\ba.a(s((((((z)))))))b)))))))))))) (\xy.x))
= (\sz.(((((((((((((\ba.a(s((((((z)))))))b))))))))))(\ba.a(s(((((((((((\ba.a(s((((((z)))))))b)))))))))) 42 (\xy.x)))b)))) (\xy.x))
= (\sz.(((((((((((((\ba.a(s((((((z)))))))b))))))))))(\ba.a(s((((((((((((\xy.x)(s((((((z)))))))42))))))))))))b)))) (\xy.x))
= (\sz.(((((((((((((\ba.a(s((((((z)))))))b))))))))))(\ba.a(s(((((((((((((s((((((z))))))))))))))))))))b)))) (\xy.x))
= (\sz.(((((((((((((a.a(s((((((z)))))))(\bo.o(s(((((((((((((s((((((z))))))))))))))))))))b)))))))))))))) (\xy.x))
= (\sz.((((((((((((((\xy.x)(s((((((z)))))))(\bo.o(s(((((((((((((s((((((z))))))))))))))))))))b)))))))))))))))
= (\sz.(((((((((((((((s((((((z))))))))))))))))))))))
= \sz.sz

na gut, ohne die ganzen (eigentlich unnoetigen) klammern ist es doch etwas kuerzer:

rkpred \sz.z =
= (\nsz.n(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)) (\uv.v)
= \sz.(\uv.v)(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)
= \sz.(\a.az(\dc.czd)) (\xy.x)
= \sz.((\xy.x)z(\dc.czd))
= \sz.z

rkpred \sz.sz =
= (\nsz.n(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)) (\uv.uv)
= \sz.(\uv.uv)(\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)
= \sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd))) (\xy.x)
= \sz.((\q.q(\ba.a(s(q 42 (\xy.x)))b)) (\a.az(\dc.czd))(\xy.y)) (\xy.x)
= \sz.((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((\xy.y)z(\dc.czd))) (\xy.x)
= \sz.((\q.q(\ba.a(s(q 42 (\xy.x)))b)) (\dc.czd)) (\xy.x)
= \sz.((\dc.czd)(\ba.a(s((\dc.czd) 42 (\xy.x)))b)) (\xy.x)
= \sz.((\dc.czd)(\ba.a(s((\xy.x) z 42))b)) (\xy.x)
= \sz.((\dc.czd)(\ba.a(sz)b)) (\xy.x)
= \sz.(\c.cz(\ba.a(sz)b)) (\xy.x)
= \sz.(\xy.x)z(\ba.a(sz)b)
= \sz.z

rkpred \sz.s(sz) =
= (\nsz.n(\p(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)) (\uv.u(uv))
= \sz.(\uv.u(uv))(\p(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y))) (\a.az(\dc.czd)) (\xy.x)
= \sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(\a.az(\dc.czd)))) (\xy.x)
= ... (see "rkpred \sz.sz")
= \sz.((\p.(\q.q(\ba.a(s(q 42 (\xy.x)))b)) (p(\xy.y)))(\c.cz(\ba.a(sz)b))) (\xy.x)
= \sz.((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((\c.cz(\ba.a(sz)b))(\xy.y))) (\xy.x)
= \sz.((\q.q(\ba.a(s(q 42 (\xy.x)))b)) ((\xy.y)z(\ba.a(sz)b))) (\xy.x)
= \sz.((\q.q(\ba.a(s(q 42 (\xy.x)))b)) (\ba.a(sz)b)) (\xy.x)
= \sz.((\ba.a(sz)b)(\ba.a(s((\ba.a(sz)b) 42 (\xy.x)))b)) (\xy.x)
= \sz.((\ba.a(sz)b)(\ba.a(s(((\xy.x)(sz)42)))b)) (\xy.x)
= \sz.((\ba.a(sz)b)(\ba.a(s(sz))b)) (\xy.x)
= \sz.(a.a(sz)(\bo.o(s(sz))b)) (\xy.x)
= \sz.((\xy.x)(sz)(\bo.o(s(sz))b))
= \sz.sz

uebungen

wer jetzt bis hierhin alles gelesen hat, und auch meint es verstanden zu haben, fuer den habe ich auch noch eine uebungsaufgabe:

was passiert wohl, wenn ich meinem vorgaenger einen (original-)leibniz-butterkeks ueberreiche ?
(ihr wisst schon, den mit den 52 zaehnen...)
und was passiert dann mit der 42 ?
loesung bitte genauso ausfuehrlich wie oben *g*

;o) rk, 2002-05-05/2003-04-04