Y-Kombinator: Einige Funktionen haben keine festen Punkte

Das Problem mit Lambda-Ausdrücken ist, dass sie nicht als Funktionen in einem mathematischen Sinn interpretiert werden können, d. h. Abbildungen von einer Menge zu einer anderen.

Der Grund ist die Kardinalität des Satzes von Funktionen von einem Set A auf sich selbst ist immer größer als die Kardinalität von A , so dass nicht alle Funktionen von A bis A ein Element von% sein können Code%. Das heißt, es gibt eine Funktion A , für die der Ausdruck f: A -> A keinen Sinn ergibt.

Dies ist wie die "Menge aller Mengen, die sich nicht selbst enthalten", was logisch keinen Sinn ergibt.

JavaScript ist kein Modell des Lambda-Kalküls.

Das Problem mit Ihrem Beispiel ist das

sollte äquivalent zu

Es ist jedoch nicht in Ihrem JavaScript-Programm, wo f(f) die Indikatorfunktion von g ist.

0 ist immer x x . Daher wird die erste Zeile als undefined ausgewertet. Die zweite Zeile ergibt g (undefined) = 0 . Das bedeutet, dass Ihr JavaScript-Modell des Lambda-Kalküls tatsächlich kein Modell ist.

Da für jede nicht leere Menge g (g (undefined)) = g (0) = 1 eine Funktion von D bis D ohne einen festen Punkt existiert, kann natürlich kein Modell des Lambda-Kalküls existieren. Ich denke, es sollte sogar möglich sein zu beweisen, dass es keine Implementierung des Y-Kombinators in einer Turing-vollständigen Sprache geben kann.

Soweit ich Wikipedia-Artikel verstehe, bedeutet das nicht, dass "jede JavaScript-Funktion einen festen Punkt hat" und dieses Beispiel zeigt einfach, wie man einen Y-Kombinator für Funktionen implementiert, die es nach ihrer Spezifikation haben.

Und nein, gemäß den Definitionen in diesem Artikel und einem Artikel zum Fixpunkt kann JavaScript " t ein untypisierter Lambda-Kalkül sein, weil er Funktionen formulieren kann, die offensichtlich keine "Fixpunktprüfung" haben, wie function f(x){ return x + 1 } oder x ^ 1 , wenn Sie Nicht-Nummern einschließen wollen und somit fehlschlagen "hat jede Funktion mindestens eine feste Punkt "überprüfen Sie auch.

Festpunkttheorie kommt in Aromen. Die für Programmiersprachen werden unter der Überschrift Denotationssemantik untersucht. Sie sind auf Werte angewiesen, die eine strukturierte zählbare Menge mit speziellen Eigenschaften bilden. Lattice und Komplette Teilbestellungen sind zwei Beispiele. Alle diese Mengen haben ein "bottom" -Element, was sich als der Fixpunkt herausstellt, der "kein nützliches Ergebnis" bedeutet. Tatsächlich sind die einzigen Fixpunktoperatoren, an denen Sie mit Computerprogrammen interessiert sind, kleinste Festkommaoperatoren: diejenigen, die den kleinsten minimalen Fixpunkt finden, der in der strukturierten Menge von Werten am niedrigsten ist. (Beachten Sie, dass alle Ganzzahlen auf derselben "Ebene" in diesen strukturierten Mengen sind. Nur das untere Element lebt darunter. Die restlichen Schichten bestehen aus komplexeren Typen wie Funktions- und Tupeltypen, dh Strukturen.) Wenn Sie etwas diskrete Mathematik haben das legt es sehr schön hin. Tarskys Fixpunkttheorem sagt eigentlich, dass jede Funktion, die monoton (oder alternativ stetig ) ist, einen festen Punkt hat. Siehe die obige Referenz für Definitionen. In operationellen Computerprogrammen entspricht das untere Element einer nicht endenden Berechnung: einer unendlichen Rekursion.

Der Punkt von all dem ist, dass Sie, wenn Sie ein strenges mathematisches Berechnungsmodell haben, anfangen können, interessante Dinge über Typsysteme und Programmkorrektheit zu beweisen. Es ist also nicht nur eine akademische Übung.