Ja, herzlich willkommen. Wie Sie sich vielleicht entsinnen, stecken wir so ein bisschen in so

einem Cliffhanger in einem Beweis fest, den wir noch nicht fertig haben. Ich erinnere nochmal

an den Standardisierungssatz, das ist das, was wir gerade beweisen. Wenn ein Term überhaupt

auf irgendeine Weise zu einer Normalform S reduziert, dann reduziert er zu dieser Normalform

unter normaler Reduktion, also unter leftmost, outermost Reduktion, wo ich also eine Reduktion

betreibe, indem ich einfach den Term von oben traversiere, depth first und nach links und

sobald ich einen Wetterredex finde, reduziere ich ihn. Man kann das, wenn man sich den Term

syntaktisch anschaut, noch etwas einfacher sagen, weil ja das Lambda von weiter außen

stehenden Wetterredexen. Jeder Wetterredex enthält ja einen Lambda, denn er hat ja diese

Form hier. Jeder Wetterredex enthält einen Lambda und Lambdas, die weiter außen sind,

die sind natürlich auch weiter links. Das heißt, ich sage bei leftmost, outermost im

Grunde zweimal weiter links. Das heißt, wenn ich mir den Term syntaktisch angucke, dann

reduziere ich einfach denjenigen Wetterredex zuerst, dessen Lambda am weitesten links

steht. Das ist für den Menschen, der den Term vor sich sieht, ganz einfach. So, und

das ist also dieser Standardisierungsatz, zentrales Resultat, der sagt, wenn es überhaupt

terminiert, dann terminiert es per normaler Reduktion. Das hat eben erstmal moralischen,

relativ einfachen Grund. Bei normaler Reduktion nutze ich es auf optimale Weise aus, dass

ich eventuell nicht terminierende Unterterme, die als Argumente irgendwo auftauchen, einfach

wegwerfe, wenn diese Argumente in Wirklichkeit von der Funktion gar nicht verwendet werden.

So, wir hatten den Beweis angefangen. Der Beweis beruht auf einem zentralen technischen

Gadget, das ist die Angro-Reduktion. Die hatten wir letztes Mal formal definiert. Die lässt

sich kurz fassen als

diese Politik. Ich reduziere auf einmal beliebig viele Beta-Redexe in einem Term, wobei das

so ein bisschen kongranosales zu lesen ist, denn sobald ich einen Beta-Redex reduziert

habe, ist T ja nicht mehr T, sondern was anderes. Was gemeint ist, ist, ich reduziere beliebig

viele Beta-Redexe, die alle in diesem Term T im Prinzip oben sichtbar sind. Sie verteilen

sich dann, wenn ich einmal was Beta reduziere, irgendwie womöglich anders über den Term,

dann also Beta-Redaktion heißt ja das hier. Ich reduziere das auf T mit s substituiert

für x, das heißt, überall wo vorher jetzt hier in dem T x Stand steht, hinterher s,

das heißt, dass s das wandert hier so ein bisschen durch den Term. Also erstens ändert

es seinen Ort von ganz hinten zu irgendwo mittendrin und zweitens verändert sich dabei

die Anzahl Kopien, die ich von s habe, zu mehrere, vielleicht eins oder eben auch gar

keine. Und das s kann ja selber weitere Beta-Redexe enthalten und wenn ich also sage mehrere

auf einmal reduzieren, meine ich also damit auch die in s, womöglich eben dann an der

anderen Stelle, wo das s eben landet, nachdem es selber in so einer Beta-Reduktion involviert

war. So, das ist also diese Augrurreduktion, die schreibt sich mit einem G, Englisch Grand

Reduction. So, da hatten wir uns verschiedene Eigenschaften überlegt, die zum Teil relativ

offensichtlich sind, also zum Beispiel, dass ich immer, gemäß der rekursiven Definition

von dieser Grand Reduction, die ich nicht nochmal anschreibe, zum Beispiel eben auch

keinen Beta-Redux reduzieren kann, das ist erlaubt. Und aber auch, dass ich andersherum

jede Grand Reduction auch tatsächlich durch Beta-Reduktion eben einzeln schrittweise nachstellen

kann, was also letztlich ergibt, dass also die transitive Hülle dieser Augrurreduktion

dasselbe ist, wie die der normalen Beta-Reduktion. So, das war die eine Eigenschaft, die andere

Eigenschaft, die wiederhole ich vielleicht nochmal. Ach so, um die zu formulieren, erinnere

ich auch noch an die andere Reduktionsrelation, die da involviert ist. Die hatte ich mit so

einem O indiziert für Outer-Mirrors, das ist also eine Reduktionsrelation, die nur

ganz außen liegende Beta-Redux reduziert, also wirklich ganz ohne Kontext drumrum. Und

das Lemma lautete, wenn ich so eine Augrurreduktion habe von T nach S, dann folgt, es existiert

ein Term U, so dass T erstmal durch Reduktion jeweils ganz außen liegender Beta-Redux zu

U reduziert. Wohlgemerkt, außen liegen kann heißen, dass erst nach dieser Reduktion dann