Und zwar, ich würde jetzt heute noch die Quizaufgabe wiederholen und falls Sie irgendwie,

ich finde da an einer Stelle hätte die Angabenstellung ein bisschen genauer sein sollen, dann sagt

ich jetzt bitte, weil dann können wir das für das nächste Mal fixen.

Ok, ja fangen wir einfach mal an.

Und zwar die Quizaufgabe, die erste, der ungetübte Lambda-Kalkül ist stark normalisierend.

Und zwar ist, ich glaube die hatte eigentlich auch so gut wie jeder richtig, also es hieß

explizit, begründen Sie die Antwort, also führt effektiv ein Beweis, die Aussage in

der ersten Par, der ungetübte Lambda-Kalkül ist stark normalisierend, das heißt effektiv

für alle Terme t, also t-Term gilt, alle von t ausgehenden Reduktionsfolgen sind endlich,

also es gibt keine unendliche Folge, irgendein IT, T-Strich und so weiter.

Es gibt zwei Möglichkeiten, entweder das ist wahr oder das ist falsch.

Für den Fall, der ungetübte Lambda-Kalkül ist stark normalisierend, für den Fall, dass

ihr beweisen wollt, dass das richtig ist, dann müsst ihr irgendwie beweisen, dass es

für jeden Term eben keine unendliche Folge geben kann, das sollte ziemlich unmöglich

sein es zu beweisen.

Für den Fall, dass ihr beweisen wollt, dass die Aussage falsch ist, für den Fall, dass

nicht diese Aussage gilt, heißt es, es gibt ein Term, sodass es gibt eine unendliche

Folge, also diese zwei Aussagen sind äquivalent.

Ja, das heißt, was muss ich machen, um zu beweisen, dass die These 1 falsch ist?

Na, ich muss einen Term angeben, haben etliche gemacht, zum Beispiel der hier, und ich muss

zeigen, dass zu diesem Term eine unendliche Reduktionsfolge existiert.

Also es genügt nicht nur den Term hinzuschreiben, sondern ich muss auch zeigen, dass es eine

unendliche Folge gibt.

Manche haben geschrieben, bla bla bla, dieser Term hat eine unendliche Reduktionsfolge,

dann habe ich das durchgehen lassen, aber streng genommen und eventuell auch in der

Klausur genügt das nicht einfach nur zu sagen, hier, der hat eine unendliche Folge, ich muss

auch die Folge angeben, und es genügt zum Beispiel zu sagen, dass lässt sich Beta reduzieren

zu Lambda x, Lambda x, dieser 2 ist natürlich identisch, das heißt, ich habe hier eine

unendliche Beta-Reduktionsfolge, das ist irgendwie...

Also wenn man eine Übungsabgabe macht, muss man hier jetzt noch dazuschreiben, sei T

gleich dieser Term, dieser hat eine unendliche Reduktionsfolge, daraus folgt, T ist nicht

stark normalisierend, daraus folgt, der ungetübte Lambda-Kalkül ist nicht stark normalisierend.

Streng genommen sagt die Aussage noch mehr als hier steht, das heißt eigentlich, der

Term, es gibt keine unendliche Folge und die Normalform ist eindeutig, und dadurch, es

gibt einen Term, für T, für den gilt, es gibt eine unendliche Folge oder die Normalform

ist nicht eindeutig.

Das heißt, man hätte auch theoretisch sagen können, ich beweise, um diese These zu widerlegen,

zeige ich, es gibt irgendein Term, dessen Normalform nicht eindeutig ist.

Das wäre auch gegangen, wenn ich mir jetzt nur die Formel anschaue, aber für dieses

Beispiel vom Lambda-Kalkül geht es nicht, weil der Lambda-Kalkül eben konfluent ist,

das heißt, die Normalform ist immer eindeutig, das heißt, um die komplette Aussage zu widerlegen,

müsst ihr eine unendliche Reduktionsfolge suchen.

Und ein paar Mal wurde auch Lambda x, Punkt x einfach angegeben, aber das Problem ist,

das ist in Normalform.

Und hätte man explizit die Reduktionsfolge angegeben, hätte man auch gemerkt, dass

das mit dem irgendwie nicht klappt, denn der ist in Normalform.

Und das ist in it.

Ja, geht das so?

Ne.

Und links.