Soweit ich weiß, sind die Hauptmodelle der Berechenbarkeit λ-Kalkül, Turing-Maschinen und rekursive Funktionen . Mir ist die Situation bezüglich der Komplexität rekursiver Funktionen nicht bekannt, sie können für die Komplexität unbrauchbar sein oder auch nicht.
Es kann als glücklicher Zufall angesehen werden, dass Turing-Maschinen, die nicht so sehr ineffiziente Maschinen sind, auch ein sehr gutes Modell für Komplexität sind. Was die Dinge natürlich gemacht hat, ist, dass es viele Transformationen gibt, an denen polynomielle TMs beteiligt sind. (Universalmaschine, Simulation einer getapten Maschine mit einer 1-getapten Maschine, von einem beliebigen Alphabet zu einem binären, Simulation eines PRAM , ...) und dass Polynome eine Klasse von Funktionen sind, die durch arithmetische Operationen und Kompositionen stabil sind - Das macht sie zu einem guten Kandidaten für die Komplexitätstheorie.n
Reine λ-Rechnung war an sich für die Komplexität nutzlos. Es kam jedoch ein einfaches Typsystem ins Spiel, das auf sehr einfache Weise Kündigungsgarantien für einige λ-Terme ermöglichte. Dann erlaubten einige andere Systeme (Systeme T , F , ..) eine große Ausdruckskraft, während die Terminierung beibehalten wurde.
Effizienz oder Komplexität sind eine Verfeinerung der Terminierung und der Typen, die eng mit der Logik verbunden sind. Später kamen leichte lineare Logiken, die mehrere Komplexitätsklassen charakterisieren. ( Elementary , P und einige Variationen für PSPACE und andere). Die Forschung auf diesem Gebiet ist sehr aktiv und nicht auf diese Komplexitätsklassen beschränkt, und sie ist nicht einmal auf den λ-Kalkül beschränkt.
tl; dr: λ-Kalkül war nützlich für die Berechenbarkeits-, Terminierungs- und Komplexitätstheorie.
Kredit zu geben, wo Kredit fällig ist Turing-Maschinen sind eine gute und einstimmige Methode, um die Komplexität zu definieren. Dies gilt jedoch nur für lose Grenzen wie "Polynom", nicht für enge Grenzen, für die PRAM-ähnliche Modelle besser geeignet sind.
In Bezug auf die zeitliche Komplexität denke ich, dass dies für die Lambda-Rechnung schwierig ist. Der Grund ist, dass der Einheitsberechnungsschritt in der Lambda-Berechnung Reduktion ( Wikipedia-Eintrag ) ist: Alle Ausdrücke, unabhängig davon von ihrer Länge würde Rechenzeitschritt unter diesem Modell dauern .( λ x . t e r m ) v → t e r m [ x : = v ] 1β
quelle
Über die Einbeziehung des λ-Kalküls in das Standardkomplexitätsmodell finden Sie hier die Zusammenfassung einiger (sehr) neuer Forschungen zu diesem Thema. Es gibt eine Antwort auf diese Frage für eine eingeschränkte Form der β-Reduktion. Grundsätzlich ähnelt die Komplexität des Standardkostenmodells der Zählung von β-Reduktionsschritten, wenn sie auf die Kopfreduktion beschränkt ist (einschließlich Call-by-Name- und Call-by-Value-Strategien).
Zur Invarianz des Einheitskostenmodells für die Kopfreduktion von Beniamino Accattoli und Ugo Dal Lago. (WST2012, Link zum Verfahren )
quelle