Ich habe drei verwandte Unterfragen, die unten durch Aufzählungszeichen hervorgehoben sind (nein, sie konnten nicht geteilt werden, wenn Sie sich fragen). Andrej Bauer schrieb hier , dass einige Funktionen durch eine Turing-Maschine realisierbar sind, aber nicht durch eine Lambda-Rechnung. Ein wichtiger Schritt seiner Überlegungen ist:
Wenn wir jedoch den Lambda-Kalkül verwenden, soll [das Programm] c aus einem Lambda-Term, der eine Funktion f darstellt, eine Ziffer berechnen, die eine Turing-Maschine darstellt. Dies ist nicht möglich (ich kann erklären, warum, wenn Sie es als separate Frage stellen).
- Ich würde gerne eine Erklärung / einen informellen Beweis sehen.
Ich verstehe nicht, wie ich den Satz von Rice hier anwenden soll. es würde auf das Problem zutreffen "Sind diese Drehmaschine T und dieser Lambda-Term L äquivalent?", weil das Anwenden dieses Prädikats auf äquivalente Terme das gleiche Ergebnis ergibt. Die erforderliche Funktion kann jedoch unterschiedliche, aber äquivalente TMs für unterschiedliche, aber äquivalente Lambda-Terme berechnen.
- Wenn das Problem in der Introspektion eines Lambda-Terms besteht, denke ich, dass es auch akzeptabel wäre, eine Gödel-Codierung eines Lambda-Terms zu übergeben, oder?
Einerseits bin ich nicht sehr überrascht, da sein Beispiel die Berechnung der Anzahl von Schritten in der Lambda-Rechnung beinhaltet, die eine Turing-Maschine benötigt, um eine gegebene Aufgabe zu erfüllen.
- Aber da hier die Lambda-Rechnung ein Problem mit der Turingmaschine nicht lösen kann, frage ich mich, ob man ein ähnliches Problem für die Lambda-Rechnung definieren und es für Turingmaschinen als unlösbar beweisen kann, oder ob es tatsächlich einen Unterschied in der Leistung zugunsten von gibt Turing Machines (was mich überraschen würde).
quelle
Was Neel gesagt hat und auch folgendes.
Ich möchte (betonen erneut , wieder und wieder ) , dass die Darstellung von Eingangs- und Ausgangsfragen. Wenn wir Darstellungen ändern dürfen, können wir fast alles erreichen (zum Beispiel eine gegebene Funktion berechenbar machen). Es ist also nicht akzeptabel , von einer Repräsentation der Funktionen durch -terms zu einer Repräsentation durch Gödel-Zahlen zu gelangen, wenn unser Berechnungsmodell -calculus ist (weil dann die aktuelle Operation wird durch -calculus unberechenbar).N→N λ λ λ
Eine Aussage, die im term-Modell, aber nicht im Turing-Maschinenmodell realisierbar ist, ist "nicht jede Funktion hat einen Gödel-Code", was irgendwie albern ist. Ich werde versuchen, eine bessere zu finden und diese Antwort zu bearbeiten.λ N→N
Edit on 2013-10-07: Hier ist, was ich mit "Currying wird unberechenbar" gemeint habe. Angenommen, wir verwenden das untypisierte -calculus als unser Rechenmodell, aber dann entscheiden wir, dass wir Maps mit Gödel-Codes darstellen sollen (von Turing-Maschinen, codiert als Church-Zahlen). Klingt harmlos, oder? Schließlich glauben wir, dass das Mantra "Turingmaschinen und Kalkül gleichwertig sind".λ N→N λ
Nun, damit diese neue Repräsentation tatsächlich eine gültige Repräsentation von , müssen wir auch die Anwendung und das Currying realisieren (weil "Funktionen darstellen" dasselbe bedeutet wie "eine repräsentieren" exponentielles Objekt "). Genauer gesagt, wir brauchen eine -term , so dass, wann immer der Kirche Zeichen steht dann dargestellt wird . (Hier schreibe ich für die Nummer der Kirche, die die Nummer .) Eine solcheN→N λ app n¯¯¯ f:N→N f(k) appn¯¯¯k¯¯¯ n¯¯¯ n app ist leicht verfügbar, da es sich um einen Interpreter für Turing-Maschinen handelt, der im -calculus implementiert ist.λ
Aber wie wäre es mit Curry? Dafür brauchen wir folgendes. Angenommen, ist eine dargestellte Menge. Bei einer gegebenen Map die mit einem -term berechnet wurde , müssen wir zeigen, dass die Transposition wird auch von einigen berechnet -term . Betrachten Sie jedoch das Beispiel, in dem die Menge von die durch -terms dargestellt wird, und die Anwendung ist. Dann wäre eine Map, die als Identität fürX f:X×N→N λ t f~:X→(N→N) λ s X N→N λ f f~ N→N , aber sein Realisator ist ein Term, der Terms, die Maps in entsprechende Gödel-Codes umwandelt . Ein solches -term existiert nicht (zum Beispiel, weil es in einem topologischen semantischen Modell diskontinuierlich wäre).λ λ N→N λ
Sie könnten einwenden, dass ich die spezifisch dargestellte Menge von Maps die durch -terms dargestellt werden, nicht hätte verwenden sollen, weil wir uns darauf geeinigt haben, dass diese durch Gödel-Codes dargestellt werden sollen . Aber du würdest dich irren. Zuallererst hätte ich ein anderes mit einem komplizierteren Beweis verwenden können, der sich Ihnen entziehen würde, aber dennoch das gleiche Ergebnis erzielen würde. Zweitens ist in der Kategorie vorhanden, und die Definition des Exponentials erfordert, dass das Currying in Bezug auf alle Objekte funktioniert . Sie müssen die Kategorie respektieren. Sie können es nicht einfach nach dem Zufallsprinzip schlachten und einige Gegenstände herausnehmen (na ja, Sie können es, aber dann sind Sie ein Metzger).X N→N λ X X
quelle