Kann mir jemand umgangssprachlich erklären, was das bedeutet? Die weiteren Definitionen bauen ja darauf auf, aber irgendwie kann ich damit nix anfangen. [img]http://www.fb18.de/gfx/16.gif[/img]

Die genaue Definition findet sich in den Folien des ersten Teils auf 13-28.

Kapitel/ Themenbereich willst du nicht verraten?

Doch!

Kapitel 13: Getypte Logik - Lambda-Kalkül.

Du hattest aber schon gesehen, dass ich nicht die Folien 13 bis 28 meinte, sondern genau Folie 13-28, oder? [img]http://www.fb18.de/gfx/25.gif[/img]

Naja. Es geht darum, ob du eine Variable einfach dazuschreiben kannst oder nicht.

Beispiel:
(\x.(x)y) x
Die einfache Beta-Substitution ergibt:

\x.(x)x
Aber das ist ja eindeutig nicht mehr das gleiche wie oben, denn das letzte x verweist jetzt auf das x des Lambdas!

Also ist y nicht "frei für x" bezüglich \x.(x)y (ich hoffe, ich hab die Formulierung hier richtigrum. Das ist immer so ungeschickt).

Vergleiche das mit den Möglichkeiten der Substitution inder Prädikatenlogik.

Ich kann leider grad nichts mit Beta-Substitution anfangen, drei Folien später gibt es die Beta-Reduktion, aber da seh ich jetzt grad nicht so den Zusammenhang.

Soll bei dir eigentlich \x ein Lambda sein, oder schon der \ ?

Hypothese:
B ist frei für x in A gdw. es bei der Substitution A{x/B} nicht zu unerwünschten Bindungen von vorher freien Variablen durch den Lambda-Operator kommt

\ ist ein Möchtegern-Lambda. Sowas wie ,\ vielleicht ;-)

Aber was meinst du denn mit Beta-Substitution?

Und stimmt meine Hypothese?

Ich kann leider grad nichts mit Beta-Substitution anfangen, drei Folien später gibt es die Beta-Reduktion, aber da seh ich jetzt grad nicht so den Zusammenhang.

Da hab ich einen Fehler gemacht :-) Also nochmal neu:

(\y.\x.(x)y)x
Beta-reduziert (wenn man es "zu einfach" betrachtet) zu

\x.(x)x
Was definitiv das falsche Ergebnis ist.

Hypothese:
B ist frei für x in A gdw. es bei der Substitution A{x/B} nicht zu unerwünschten Bindungen von vorher freien Variablen durch den Lambda-Operator kommt

Ja, so würde ich das auch sehen.

Okay, ich glaube, ich habs verstanden. Danke!