Festkomma-Kombinator - Fixed-point combinator

In der Mathematik und Informatik im Allgemeinen ist ein Fixpunkt einer Funktion ein Wert, der durch die Funktion auf sich selbst abgebildet wird.

In der kombinatorischen Logik für die Informatik ist ein Festkomma-Kombinator (oder Festkomma-Kombinator ) eine Funktion höherer Ordnung , die einen Festpunkt ihrer Argumentfunktion zurückgibt, falls eine existiert. ${\displaystyle {\textsf {fix}}}$

Formal hat die Funktion f einen oder mehrere Fixpunkte, dann

${\displaystyle {\textsf {fix}}\ f=f\ ({\textsf {fix}}\ f)\ ,}$

und somit bei wiederholter Anwendung

${\displaystyle {\textsf {fix}}\ f=f\ (f\ (\ldots f\ ({\textsf {fix}}\ f)\ldots ))\ .}$

Y-Kombinator

Im klassischen untypisierten Lambda-Kalkül hat jede Funktion einen Fixpunkt.

Eine besondere Implementierung von fix ist Currys paradoxer Kombinator Y , dargestellt durch

${\displaystyle {\textsf {Y}}=\lambda f.\ (\lambda xf\ (x\ x))\ (\lambda xf\ (x\ x))\ .}$

In der funktionalen Programmierung kann der Y-Kombinator verwendet werden, um rekursive Funktionen in einer Programmiersprache, die keine Rekursion unterstützt , formal zu definieren .

Dieser Kombinator kann bei der Implementierung des Curry-Paradoxons verwendet werden . Das Herz von Currys Paradox ist, dass nicht typisierte Lambda-Kalküle als deduktives System nicht stichhaltig sind, und der Y- Kombinator zeigt dies, indem er einem anonymen Ausdruck erlaubt, null oder sogar viele Werte darzustellen. Dies ist in der mathematischen Logik widersprüchlich.

Auf eine Funktion mit einer Variablen angewendet, terminiert der Y- Kombinator normalerweise nicht. Interessantere Ergebnisse erhält man, wenn man den Y- Kombinator auf Funktionen von zwei oder mehr Variablen anwendet . Die zweite Variable kann als Zähler oder Index verwendet werden. Die resultierende Funktion verhält sich wie eine while- oder eine for- Schleife in einer imperativen Sprache.

Auf diese Weise verwendet der Y- Kombinator eine einfache Rekursion. Im Lambda-Kalkül ist es nicht möglich, auf die Definition einer Funktion in einem Funktionsrumpf zu verweisen. Eine Rekursion kann nur durch die Übergabe einer Funktion als Parameter erreicht werden. Der Y- Kombinator demonstriert diesen Programmierstil.

Festkomma-Kombinator

Der Y- Kombinator ist eine Implementierung eines Festkomma-Kombinators in der Lambda-Rechnung. Festkomma-Kombinatoren können auch in anderen funktionalen und zwingenden Sprachen leicht definiert werden. Die Implementierung in Lambda-Kalkül ist aufgrund von Einschränkungen in Lambda-Kalkül schwieriger. Der Festkomma-Kombinator kann in verschiedenen Bereichen eingesetzt werden:

• Allgemeine Mathematik
• Nicht typisierte Lambda-Rechnung
• Typisierte Lambda-Rechnung
• Funktionale Programmierung
• Imperative Programmierung

Festkomma-Kombinatoren können auf eine Reihe verschiedener Funktionen angewendet werden, werden jedoch normalerweise nicht beendet, es sei denn, es gibt einen zusätzlichen Parameter. Wenn die zu korrigierende Funktion auf ihren Parameter verweist, wird ein weiterer Aufruf der Funktion aufgerufen, sodass die Berechnung nie gestartet wird. Stattdessen wird der zusätzliche Parameter verwendet, um den Start der Berechnung auszulösen.

Der Typ des Fixpunkts ist der Rückgabetyp der zu fixierenden Funktion. Dies kann eine reelle oder eine Funktion oder ein beliebiger anderer Typ sein.

Im nicht typisierten Lambda-Kalkül kann die Funktion, auf die der Festkomma-Kombinator angewendet wird, unter Verwendung einer Codierung wie der Church-Codierung ausgedrückt werden . In diesem Fall werden bestimmte Lambda-Terme (die Funktionen definieren) als Werte betrachtet. "Laufen" (beta reduzierend) des Festkomma-Kombinators bei der Codierung ergibt einen Lambda-Term für das Ergebnis, der dann als Festkomma-Wert interpretiert werden kann.

Alternativ kann eine Funktion als rein im Lambda-Kalkül definierter Lambda-Ausdruck betrachtet werden.

Diese unterschiedlichen Ansätze wirken sich darauf aus, wie ein Mathematiker und ein Programmierer einen Festkomma-Kombinator betrachten können. Ein Lambda-Kalkül-Mathematiker kann den Y- Kombinator, der auf eine Funktion angewendet wird, als einen Ausdruck betrachten, der die Festkommagleichung erfüllt, und daher als Lösung.

Im Gegensatz dazu kann eine Person, die einen Festkomma-Kombinator nur auf eine allgemeine Programmieraufgabe anwenden möchte, dies möglicherweise nur als Mittel zur Implementierung einer Rekursion sehen.

Werte und Domänen

Jeder Ausdruck hat einen Wert. Dies gilt in der allgemeinen Mathematik und muss in der Lambda-Kalküle wahr sein. Dies bedeutet, dass Sie in der Lambda-Kalküle durch Anwenden eines Festkomma-Kombinators auf eine Funktion einen Ausdruck erhalten, dessen Wert der Festpunkt der Funktion ist.

Dies ist jedoch ein Wert im Bereich der Lambda-Kalküle , er entspricht möglicherweise keinem Wert im Bereich der Funktion, ist also im praktischen Sinne nicht unbedingt ein Fixpunkt der Funktion, und nur im Bereich der Lambda-Kalküle ist es ein Fixpunkt der Gleichung.

Betrachten Sie zum Beispiel

${\displaystyle x^{2}=-1\Rightarrow x={\frac {-1}{x}}\Rightarrow f\ x={\frac {-1}{x}}\land {\textsf {Y }}\ f=x}$

Die Division von Zahlen mit Vorzeichen kann in der Church-Codierung implementiert werden, sodass f durch einen Lambda-Ausdruck dargestellt werden kann. Diese Gleichung hat keine Lösung in den reellen Zahlen. Aber im Bereich der komplexen Zahlen sind i und -i Lösungen. Dies zeigt, dass es Lösungen für eine Gleichung in einem anderen Bereich geben kann. Der Lambda-Term für die Lösung der obigen Gleichung ist jedoch seltsamer. Der Lambda-Term stellt den Zustand dar, in dem x entweder i oder -i als ein Wert sein könnte. Die Informationen, die diese beiden Werte unterscheiden, sind beim Domänenwechsel verloren gegangen. ${\displaystyle Y\ f}$

Für den Lambda-Kalkül-Mathematiker ist dies eine Folge der Definition von Lambda-Kalkül. Für den Programmierer bedeutet dies, dass die Beta-Reduktion des Lambda-Terms ewig durchlaufen wird und nie eine normale Form erreicht.

Funktion versus Implementierung

Der Festkomma-Kombinator kann in der Mathematik definiert und dann in anderen Sprachen implementiert werden. Die allgemeine Mathematik definiert eine Funktion basierend auf ihren Dehnungseigenschaften . Das heißt, zwei Funktionen sind gleich, wenn sie dieselbe Abbildung durchführen. Lambda-Kalkül und Programmiersprachen betrachten die Funktionsidentität als intensionale Eigenschaft. Die Identität einer Funktion basiert auf ihrer Implementierung.

Eine Lambda-Kalkül-Funktion (oder ein Term) ist eine Implementierung einer mathematischen Funktion. Im Lambda-Kalkül gibt es eine Reihe von Kombinatoren (Implementierungen), die der mathematischen Definition eines Festkomma-Kombinators genügen.

Was ist ein "Kombinator"?

Die kombinatorische Logik ist eine Funktionstheorie höherer Ordnung . Ein Kombinator ist ein geschlossener Lambda-Ausdruck, was bedeutet, dass er keine freien Variablen hat. Die Kombinatoren können kombiniert werden, um Werte an ihre richtigen Stellen im Ausdruck zu leiten, ohne sie jemals als Variablen zu benennen.

Verwendung in der Programmierung

Festkomma-Kombinatoren können verwendet werden, um eine rekursive Definition von Funktionen zu implementieren . In der praktischen Programmierung werden sie jedoch selten verwendet. Stark normalisierende Typsysteme wie der einfach typisierte Lambda-Kalkül verbieten eine Nicht-Terminierung und daher können Festkomma-Kombinatoren oft keinem Typ zugewiesen werden oder erfordern komplexe Typsystem-Merkmale. Darüber hinaus sind Festkomma-Kombinatoren im Vergleich zu anderen Strategien zur Implementierung von Rekursionen oft ineffizient, da sie mehr Funktionsreduktionen erfordern und für jede Gruppe von sich gegenseitig rekursiven Definitionen ein Tupel konstruieren und auseinandernehmen.

Die Fakultätsfunktion

Die Fakultätsfunktion liefert ein gutes Beispiel dafür, wie der Festkomma-Kombinator angewendet werden kann. Das Ergebnis zeigt eine einfache Rekursion, wie sie in einer imperativen Sprache in einer einzelnen Schleife implementiert würde. Die Definition der verwendeten Zahlen wird in der Codierung der Kirche erklärt .

Die Funktion, die sich selbst als Parameter nimmt, ist

${\displaystyle F\ f\ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiplizieren} \ n\ (f\ (\operatorname {pred} \ n)))\ .}$

Dies ergibt YF n as

${\displaystyle {\begin{aligned}{\textsf {fix}}\ F\ n&=F\ ({\textsf {fix}}\ F)\ n\\&=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (({\textsf {fix}}\ F)\ (\operatorname {pred} \ n)))\ .\end{ausgerichtet}}}$

Einstellung gibt ${\displaystyle {\textsf {fix}}\ F=\operatorname {fact} }$

${\displaystyle \operatorname {fact} \ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (\operatorname {fact} \ (\operatorname {pred} \ n))) \ .}$

Diese Definition setzt F in die Rolle des Körpers einer zu iterierenden Schleife und entspricht der mathematischen Definition von Fakultät:

${\displaystyle \operatorname {fact} \ n={\begin{cases}1&{\text{if}}~n=0\\n\times \operatorname {fact} \ (n-1)&{\text{ sonst.}}\end{cases}}}$

Festkomma-Kombinatoren im Lambda-Kalkül

Der von Haskell B. Curry entdeckte Y- Kombinator ist definiert als

${\displaystyle Y=\lambda f.(\lambda xf\ (x\ x))\ (\lambda xf\ (x\ x))\ .}$

Beta-Reduktion davon gibt:

${\displaystyle Y\ g}$	${\displaystyle =(\lambda f.(\lambda xf\ (x\ x))\ (\lambda xf\ (x\ x)))\ g}$	(per Definition von Y )
	${\displaystyle =(\lambda xg\ (x\ x))\ (\lambda xg\ (x\ x))}$	(durch β-Reduktion von λf: Y auf g angewendet)
	${\displaystyle =g\ ((\lambda xg\ (x\ x))\ (\lambda xg\ (x\ x)))}$	(durch β-Reduktion von λx: linke Funktion auf rechte Funktion angewendet)
	${\displaystyle =g\ (Y\g)}$	(durch zweite Gleichheit)

Wiederholtes Anwenden dieser Gleichheit ergibt:

${\displaystyle Y\ g=g\ (Y\ g)=g\ (g\ (Y\ g))=g\ (\ldots g\ (Y\ g)\ldots )}$

(Die obige Gleichheit sollte man sich als eine Folge von mehrstufigen β-Reduktionen von links nach rechts vorstellen. Der Lambda-Term darf im Allgemeinen nicht auf den Term β-reduzieren . Man kann die Gleichheitszeichen stattdessen als β-Äquivalenzen interpretieren von mehrstufigen β-Reduktionen, um in beide Richtungen gehen zu können.) ${\displaystyle g\ (Y\ g)}$${\displaystyle Y\ g}$

Äquivalente Definition eines Festkomma-Kombinators

Dieser Festkomma-Kombinator kann als y definiert werden , da in

${\displaystyle x=f\x\land y\f=x}$

Ein Ausdruck für y kann unter Verwendung von Regeln aus der Definition eines let-Ausdrucks abgeleitet werden . Erstens mit der Regel

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

gibt

${\displaystyle \operatorname {let} x=f\ x\operatorname {in} y\ f=x\ .}$

Auch mit

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\to \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)}$

gibt

${\displaystyle y\ f=\operatorname {let} x=f\ x\operatorname {in} x\ .}$

Und dann mit der eta-Reduktionsregel ,

${\displaystyle f\ x=y\iff f=\lambda xy\ ,}$

gibt

${\displaystyle y=\lambda f.\operatorname {let} x=f\ x\operatorname {in} x\ .}$

Herleitung des Y-Kombinators

Der Y-Kombinator von Curry kann leicht aus der Definition von y erhalten werden .

Beginnen mit,

${\displaystyle \lambda f.\operatorname {let} x=f\ x\operatorname {in} x\ ,}$

Eine Lambda-Abstraktion unterstützt keinen Verweis auf den Variablennamen im angewendeten Ausdruck, daher muss x als Parameter an x übergeben werden . Wir können uns das als Ersetzen von x durch xx vorstellen , aber formal ist dies nicht korrekt. Stattdessen definieren Sie y durch gibt ${\displaystyle \forall z,y\z=x}$

${\displaystyle \lambda f.\operatorname {let} y\ z=f\ (y\ z)\operatorname {in} y\ z\ .}$

Der let-Ausdruck kann als Definition der Funktion y angesehen werden , wobei z der Parameter ist. Instanziierung z wie y im Anruf ergibt

${\displaystyle \lambda f.\operatorname {let} y\ z=f\ (y\ z)\operatorname {in} y\ y\ .}$

Und da der Parameter z immer die Funktion y übergibt ,

${\displaystyle \lambda f.\operatorname {let} y\ z=f\ (z\ z)\operatorname {in} y\ y\ .}$

Mit Hilfe der eta Reduktion Regel,

${\displaystyle f\ x=y\equiv f=\lambda xy\ ,}$

gibt

${\displaystyle \lambda f.\operatorname {let} y=\lambda zf\ (z\ z)\operatorname {in} y\ y\ .}$

Ein let-Ausdruck kann als Lambda-Abstraktion ausgedrückt werden ; mit

${\displaystyle n\not\in FV(E)\to (\operatorname {let} n=E\operatorname {in} L\equiv (\lambda nL)\ E)}$

gibt

${\displaystyle \lambda f.(\lambda yy\ y)\ (\lambda zf\ (z\ z))\ .}$

Dies ist möglicherweise die einfachste Implementierung eines Festkomma-Kombinators in der Lambda-Rechnung. Eine Beta-Reduktion ergibt jedoch die symmetrischere Form von Currys Y-Kombinator:

${\displaystyle \lambda f.(\lambda zf\ (z\ z))\ (\lambda zf\ (z\ z))\ .}$

Siehe auch Übersetzen zwischen let- und Lambda-Ausdrücken .

Andere Festkomma-Kombinatoren

In nicht typisierten Lambda-Kalkülen sind Festkomma-Kombinatoren nicht besonders selten. Tatsächlich gibt es unendlich viele davon. 2005 zeigte Mayer Goldberg, dass die Menge der Fixkomma-Kombinatoren der untypisierten Lambda-Kalküle rekursiv aufzählbar ist .

Der Y- Kombinator kann im SKI-Kalkül ausgedrückt werden als

${\displaystyle Y=S(K(SII))(S(S(KS)K)(K(SII)))\ .}$

Der einfachste Fixpunktkombinator im SK-Kalkül, gefunden von John Tromp , ist

${\displaystyle Y'=SSK(S(K(SS(S(SSK))))K)\ .}$

Beachten Sie jedoch, dass es nicht in normaler Form ist, die länger ist. Dieser Kombinator entspricht dem Lambda-Ausdruck

${\displaystyle Y'=(\lambda xy.xyx)(\lambda yx.y(xyx))\ .}$

Der folgende Festkomma-Kombinator ist einfacher als der Y-Kombinator und β-reduziert sich in den Y-Kombinator; es wird manchmal als Y-Kombinator selbst zitiert:

${\displaystyle X=\lambda f.(\lambda x.xx)(\lambda xf(xx))\ .}$

Ein weiterer gebräuchlicher Fixkombinator ist der Turing-Fixkombinator (benannt nach seinem Entdecker Alan Turing ):

${\displaystyle \Theta =(\lambda xy.y(xxy))\ (\lambda xy.y(xxy))\ .}$

Der Vorteil gegenüber ist , dass Beta-reduziert sich auf , während und nur auf einen gemeinsamen Begriff Beta-verringern. ${\displaystyle {\textsf {Y}}}$${\displaystyle \Theta\f}$${\displaystyle f\ (\Theta f)}$${\displaystyle {\textsf {Y}}\ f}$${\displaystyle f\ ({\textsf {Y}}f)}$

${\displaystyle \Theta}$ hat auch ein einfaches Call-by-Value-Formular:

${\displaystyle \Theta_{v}=(\lambda xy.y(\lambda z.xxyz))\ (\lambda xy.y(\lambda z.xxyz))\ .}$

Das Analogon für die gegenseitige Rekursion ist ein polyvariadischer Fixpunktkombinator , der als Y* bezeichnet werden kann.

Strenger Festkomma-Kombinator

In einer strengen Programmiersprache wird der Y-Kombinator bis zum Stack-Überlauf erweitert oder im Falle einer Tail-Call-Optimierung nie angehalten. Der Z- Kombinator funktioniert in strikten Sprachen (auch als Eager-Sprachen bezeichnet, bei denen die applikative Bewertungsreihenfolge angewendet wird). Der Z- Kombinator hat das nächste Argument explizit definiert, wodurch die Entwicklung von Z g auf der rechten Seite der Definition verhindert wird:

${\displaystyle Zgv=g(Zg)v\ .}$

und im Lambda-Kalkül ist es eine eta-Erweiterung des Y- Kombinators:

${\displaystyle Z=\lambda f.(\lambda xf(\lambda v.xxv))\ (\lambda xf(\lambda v.xxv))\ .}$

Nicht-Standard-Festkomma-Kombinatoren

Im untypisierten Lambda-Kalkül gibt es Terme, die denselben Böhm-Baum wie ein Festkomma-Kombinator haben, also dieselbe unendliche Ausdehnung λx.x (x (x ... )) haben. Diese werden als nicht standardmäßige Festkomma-Kombinatoren bezeichnet . Jeder Festkomma-Kombinator ist auch ein Nicht-Standard-Kombinator, aber nicht alle Nicht-Standard-Festpunkt-Kombinatoren sind Festkombinatoren, weil einige von ihnen die Gleichung nicht erfüllen, die die "Standard"-Kombinatoren definiert. Diese seltsamen Kombinatoren werden als streng nicht standardmäßige Festkomma-Kombinatoren bezeichnet ; ein Beispiel ist der folgende Kombinator:

${\displaystyle N=BM(B(BM)B)}$

wo

${\displaystyle B=\lambda xyz.x(yz)}$

${\displaystyle M=\lambda x.xx\ .}$

Der Satz von Nicht-Standard-Festkomma-Kombinatoren ist nicht rekursiv aufzählbar.

Umsetzung in anderen Sprachen

(Der Y-Kombinator ist eine spezielle Implementierung eines Festkomma-Kombinators in der Lambda-Kalkül. Seine Struktur wird durch die Einschränkungen der Lambda-Kalküle bestimmt. Es ist nicht notwendig oder hilfreich, diese Struktur bei der Implementierung des Festkomma-Kombinators in anderen Sprachen zu verwenden. )

Einfache Beispiele von Festkomma-Kombinatoren, die in einigen Programmierparadigmen implementiert sind, sind unten angegeben.

Lazy funktionale Implementierung

In einer Sprache, die Lazy-Evaluation unterstützt , wie in Haskell , ist es möglich, einen Festkomma-Kombinator unter Verwendung der Definitionsgleichung des Festkomma-Kombinators zu definieren, die herkömmlich bezeichnet wird fix. Da Haskell faule Datentypen hat, kann dieser Kombinator auch verwendet werden, um Fixpunkte von Datenkonstruktoren zu definieren (und nicht nur um rekursive Funktionen zu implementieren). Die Definition wird hier gegeben, gefolgt von einigen Anwendungsbeispielen. In Hackage ist das Originalbeispiel:

fix, fix' :: (a -> a) -> a
fix f = let x = f x in x         -- Lambda dropped. Sharing.
                                 -- Original definition in Data.Function.
-- alternative:
fix' f = f (fix' f)              -- Lambda lifted. Non-sharing.

fix (\x -> 9)                    -- this evaluates to 9

fix (\x -> 3:x)                  -- evaluates to the lazy infinite list [3,3,3,...]

fact = fix fac                   -- evaluates to the factorial function
  where fac f 0 = 1
        fac f x = x * f (x-1)

fact 5                           -- evaluates to 120

Strenge funktionale Umsetzung

In einer strengen funktionalen Sprache wird das Argument zu f zuvor erweitert, was eine unendliche Aufruffolge ergibt,

${\displaystyle f\ (f...(f\ (\operatorname {fix} \ f))...)\ x}$.

Dies kann gelöst werden, indem fix mit einem zusätzlichen Parameter definiert wird.

let rec fix f x = f (fix f) x (* note the extra x; here fix f = \x-> f (fix f) x *)

let factabs fact = function   (* factabs has extra level of lambda abstraction *)
   0 -> 1
 | x -> x * fact (x-1)

let _ = (fix factabs) 5       (* evaluates to "120" *)

Imperative Sprachimplementierung

Dieses Beispiel ist eine leicht interpretierende Implementierung eines Festkomma-Kombinators. Eine Klasse wird verwendet, um die Fix- Funktion namens fixer zu enthalten . Die zu reparierende Funktion ist in einer Klasse enthalten, die von fixer erbt. Die Fix- Funktion greift als virtuelle Funktion auf die zu fixierende Funktion zu. Was die strikte funktionale Definition betrifft , wird fix explizit ein zusätzlicher Parameter x angegeben , was bedeutet, dass eine verzögerte Auswertung nicht erforderlich ist.

template <typename R, typename D>
class fixer
{
public:
    R fix(D x)
    {
        return f(x);
    }
private:
    virtual R f(D) = 0;
};

class fact : public fixer<long, long>
{
    virtual long f(long x)
    {
        if (x == 0)
        {
            return 1;
        }
        return x * fix(x-1);
    }
};

long result = fact().fix(5);

In einer imperativen-funktionalen Sprache wie Lisp , Scheme oder Racket schlägt Landin (1963) die Verwendung einer Variablenzuweisung vor, um einen Festkomma-Kombinator zu erstellen:

(define Y!
  (lambda (f-maker)
    ((lambda (f)
       (set! f (f-maker (lambda (x) (f x)))) ;; assignment statement
       f)
     'NONE)))

Mit einem Lambda-Kalkül mit Axiomen für Zuweisungsanweisungen kann gezeigt werden, dass Y! erfüllt das gleiche Festkomma-Gesetz wie der Call-by-Value-Y-Kombinator:

${\displaystyle ({\textsf {Y}}_{!}\ \lambda xe)e'=(\lambda xe)\ ({\textsf {Y}}_{!}\ \lambda xe)e'}$

Tippen

Im System F (polymorpher Lambda-Kalkül) hat ein polymorpher Festkomma-Kombinator Typ;

∀a.(a → a) → a

wobei a eine Typvariable ist . Das heißt, fix nimmt eine Funktion, die a → a abbildet und verwendet sie, um einen Wert vom Typ a zurückzugeben.

In dem einfach typisierten Lambda-Kalkül, der um rekursive Datentypen erweitert wird , können Festkomma-Operatoren geschrieben werden, aber der Typ eines "nützlichen" Festkomma-Operators (einer, dessen Anwendung immer zurückgibt) kann eingeschränkt sein.

Im einfach typisierten Lambda-Kalkül kann dem Festkomma-Kombinator Y kein Typ zugewiesen werden, da er irgendwann den Selbstanwendungs-Teilterm durch die Anwendungsregel behandeln würde: ${\displaystyle x~x}$

${\displaystyle {\Gamma \vdash x\!:\!t_{1}\to t_{2}\quad \Gamma \vdash x\!:\!t_{1}} \over {\Gamma \vdash x~ x\!:\!t_{2}}}$

wobei hat den unendlichen Typ . Tatsächlich kann kein Festkomma-Kombinator typisiert werden; in diesen Systemen muss jede Unterstützung für Rekursion der Sprache explizit hinzugefügt werden. ${\displaystyle x}$${\displaystyle t_{1}=t_{1}\to t_{2}}$

Typ für den Y-Kombinator

In Programmiersprachen, die rekursive Datentypen unterstützen , ist es möglich, den Y-Kombinator einzugeben, indem die Rekursion auf Typebene entsprechend berücksichtigt wird. Die Notwendigkeit, die Variable x selbst anzuwenden, kann mit einem Typ (Rec a) verwaltet werden, der so definiert ist, dass er isomorph zu (Rec a -> a) ist.

Im folgenden Haskell-Code haben wir beispielsweise Inund outdie Namen der beiden Richtungen des Isomorphismus mit Typen:

In :: (Rec a -> a) -> Rec a
out :: Rec a -> (Rec a -> a)

was uns schreiben lässt:

newtype Rec a = In { out :: Rec a -> a }

y :: (a -> a) -> a
y = \f -> (\x -> f (out x x)) (In (\x -> f (out x x)))

Oder äquivalent in OCaml:

type 'a recc = In of ('a recc -> 'a)
let out (In x) = x

let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))

Alternative:

let y f = (fun x -> f (fun z -> out x x z)) (In (fun x -> f (fun z -> out x x z)))

Allgemeine Information

Da Festpunkt - Kombinatoren können verwendet werden , die Rekursion zu implementieren, ist es möglich , sie zu verwenden , um bestimmte Typen von rekursiven Berechnungen, wie sie in beschreiben Fixpunktiteration , iterativen Methoden , verbindet rekursiven in relationalen Datenbanken , Datenflußanalyse , FIRST und FOLGE Sätzen von Nichtterminals in einer kontextfreien Grammatik , transitivem Abschluss und anderen Arten von Abschlussoperationen .

Eine Funktion, bei der jede Eingabe ein Fixpunkt ist, wird als Identitätsfunktion bezeichnet . Formal:

${\displaystyle \forall x(f\ x=x)}$

Im Gegensatz zur universellen Quantifizierung über alle konstruiert ein Festkomma-Kombinator einen Wert, der ein Festpunkt von ist . Die bemerkenswerte Eigenschaft eines Fixpunktkombinators besteht darin, dass er einen Fixpunkt für eine beliebige gegebene Funktion konstruiert . ${\displaystyle x}$${\displaystyle f}$${\displaystyle f}$

Andere Funktionen haben die besondere Eigenschaft, dass nach einmaliger Anwendung weitere Anwendungen keine Wirkung haben. Formeller:

${\displaystyle \forall x(f\ (f\ x)=f\ x)}$

Solche Funktionen werden als idempotent bezeichnet (siehe auch Projektion (Mathematik) ). Ein Beispiel für eine solche Funktion ist die Funktion, die 0 für alle geraden ganzen Zahlen und 1 für alle ungeraden ganzen Zahlen zurückgibt .

Beim Lambda-Kalkül führt aus rechnerischer Sicht das Anwenden eines Festkomma-Kombinators auf eine Identitätsfunktion oder eine idempotente Funktion typischerweise zu einer nicht terminierenden Berechnung. Zum Beispiel erhalten wir

${\displaystyle (Y\ \lambda xx)=(\lambda x.(xx)\ \lambda x.(xx))}$

wobei sich der resultierende Term nur auf sich selbst reduzieren lässt und eine Endlosschleife darstellt.

Festkomma-Kombinatoren existieren nicht unbedingt in restriktiveren Berechnungsmodellen. Sie existieren beispielsweise nicht in einfach typisiertem Lambda-Kalkül .

Der Y-Kombinator ermöglicht es, Rekursion als einen Satz von Rewrite-Regeln zu definieren , ohne dass native Rekursionsunterstützung in der Sprache erforderlich ist.

In Programmiersprachen , die anonyme Funktionen unterstützen , ermöglichen Festkomma - Kombinatoren die Definition und Verwendung anonymer rekursiver Funktionen , dh ohne solche Funktionen an Bezeichner binden zu müssen . In dieser Einstellung wird die Verwendung von Festkomma-Kombinatoren manchmal als anonyme Rekursion bezeichnet .

Siehe auch

• Anonyme Funktion
• Festkomma-Iteration
• Lambda-Kalkül#Rekursion und Fixpunkte
• Lambda-Anhebung
• Lassen Sie Ausdruck

Anmerkungen

Verweise

• Werner Kluge, Abstrakte Rechenmaschinen: eine Lambda-Kalkül-Perspektive , Springer, 2005, ISBN  3-540-21146-2 , S. 73–77
• Mayer Goldberg, (2005) Zur rekursiven Aufzählbarkeit von Festkomma-Kombinatoren , BRICS-Bericht RS-05-1, Universität Aarhus
• Matthias Felleisen , ein Vortrag über die Warum von Y .

Externe Links

• Rekursionstheorie und Freude , Manfred von Thun, (2002 oder früher)
• The Lambda Calculus - Notizen von Don Blaheta, 12. Oktober 2000
• Y-Kombinator
• "Eine Verwendung des Y-Kombinators in Ruby"
• "Funktionale Programmierung in Ada"
• Rosetta-Code - Y-Kombinator