Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, herzlich willkommen. Ich habe eine Ansage vorweg, wie jedes Jahr suchen wir Gleuntutoren,

wie jedes Jahr sind wir relativ verzweifelt. Das heißt, wer sich dazu irgendwie in der Lage

fühlt, der möge sich bitte bei mir melden. Ich zeige mal so unverbindlich in die Ecke da irgendwie,

ja und dann zeige ich glaube ich noch irgendwo Leute, die auf die ich nicht zeige, die können

sich auch angesprochen fühlen. Einen haben wir auch schon glaube ich gecashed heute morgen,

hier auch noch, jetzt ist es gerade nicht da. Also lassen Sie sich das nicht entgehen, macht

Riesenspaß, Sie kennen es schon. Ja, gerne direkt bei mir nach der Veranstaltung melden oder sonst

per E-Mail oder wenn Sie Angst vor mir haben bei Herrn Goncharow. Ja, der Plan für heute lautet,

ich verliere gleich noch ein paar Worte zum Thema Applikative versus normale Reduktion und ansonsten

werde ich heute, jedenfalls im Verhältnis zum Skript, einen kurzen Sprung nach vorne machen,

sprich den sogenannten Standardisierungssatz für die Lambda-Kalkülereduktion erst mal auslassen,

den holen wir dann vermutlich am Donnerstag nach und stattdessen heute schon anfangen mit dem

einfach getypten Lambda-Kalkül, das dient dem einfachen Zweck die Vorlesungen besser mit den

Übungen zu synchronisieren, weil Herr Rauch jetzt allmählich mal die Aufgaben über Typisierung

rausbringen muss. Wir kämpfen ja immer so ein bisschen mit den Feiertagen, nächsten Monat ist

gleich wieder einer. Gut, also einmal, einmal noch eine Erinnerung beziehungsweise einen Nachtrag zum

Thema Normal versus Applikativ. Einmal hatte ich so gestern, letztes nicht gestern, also nach der

letzten Sitzung hinterher das dummfe Gefühl, ich habe dir das Video jetzt noch nicht angeguckt,

ich hätte bei der Definition von normaler Reduktion ein Proviso vergessen, ich sage es deshalb sicher,

heißt es aber nochmal. Also wir hatten ja für den Fall, dass wir eine Applikation reduzieren

wollen, im Prinzip drei Fälle. Der eine Fall ist der Funktionalanteil der Applikation, also das

erste Argument ist schon eine Lambda-Abstraktion, in dem Fall schlägt ja normale Reduktion sofort

zu und reduziert halt den Better-Redux, den man dann da sieht. Es bleiben zwei Fälle, wo das T keine

Lambda-Abstraktion ist, das heißt, da wir, Moment, wir sind leftmost, das heißt wir reduzieren es nur

dann, wenn T normal ist, das heißt wir reduzieren zuerst S und dann T, wenn T normal ist und keine

Lambda-Abstraktion, denn wenn T eine Lambda-Abstraktion ist, dann greift ja die erste Klausel,

dann wollen wir also sofort diesen obersten Better-Redux reduzieren. Und das zweite, das machen wir

immer, aber auch nur in dem Fall, wo T keine Lambda-Abstraktion ist, das muss da also zweimal

stehen, ich habe so das dummfe Gefühl, ich habe es an einer Zeile vergessen letztes Mal. Trifft das zu?

Habe ich nicht vergessen, das wäre ja super. Gut, wenn ich es nicht vergessen habe, auch gut,

dann habe ich jetzt noch mal dran erinnert. So, und dann gibt es eine zweite Art, das zu sehen,

die vielleicht irgendwie handhabbarer oder fassbarer ist als das mit diesen Reduktionsregeln.

Und zwar kann man sich die Sache algorithmisch überlegen.

Und zwar kann man sich das vorstellen als zwei verschiedene Algorithmen, die jeweils gegeben

irgendeinen Termin jetzt mal mir einfach sagen, was der nächste Reduktionsschritt ist. Das sind

beides, sowohl applikative Reduktion als auch normale Reduktion, sind also völlig deterministische

Reduktionsstrategien, das heißt, gegeben einen Termin sagen die mir eindeutig, wohin ich den

reduziere, da gibt es keine Auswahlmöglichkeiten. So, und wir können also jetzt einen Algorithmus

angeben, der mir immer den nächsten Reduktionsschritt liefert. Die gesamte Reduktion

besteht dann darin, dass ich das immer iteriere. Und zwar bestehen diese Algorithmen in beiden

Fällen darin, dass ich also einfach an der Wurzel des Termbaums, ich kann ja so einen

Termin hinschreiben als Baum, also das ist ich, lambda x.xx, ja das kann ich mir als Baum so

hinmalen. Hier habe ich eine lambda-Abstraktion oben und die hat, naja lambda hat praktisch nur

ein Argument, wenn man so will, also das was unter lambda kommt und dann kommt hier eine

Applikation, die hat zwei Argumente und die heißen in diesem Falle zufällig beide x.

Das heißt, in dem Sinne stelle ich mir einen Term als Baum vor und ich traversiere den

ab der Wurzel, um jetzt einen Wetterredex zu suchen. Nun gibt es da eben einerseits

dieses Stichwort leftmost, was wir ja auch bei der Bezeichnung dieser beiden Strategien

verwendet hatten, also normal ist leftmost outermost und applikativ ist leftmost innermost.