Diskussion:Fixpunkt-Kombinator

Ganz viele Punkte

Da ich gerade wenig Lust habe, direkt am Artikel zu arbeiten, hier ein paar Punkte, die wahlweise als Kritik, Hilfestellung, dummes Gelaber oder sonstwas aufgefasst werden dürfen :)

• Der Typ eines Fixpunktoperators (je nach Drumherum ist es möglicherweise eine Familie, ein Fixpunktoperator pro Typ) sollte angegeben werden. In System-F also sowas wie $\forall X.\ (X\to X)\to X$. Logisch gesehen, mit "propositions as types", eine blatante Lüge! :)
• Die Story mit den rekursiven Definitionen ist schwamming bis komisch. Hier meine ungefähr:
  • Wir wollen Definitionen der Form $f:=\alpha$ zulassen, wobei der Name $f$ in $\alpha$ frei vorkommen darf und sich semantisch auf das hiermit definierte $f$ beziehen soll.
  • Um uns nicht so sehr mit Definitionen und Namen herumschlagen zu müssen, und uns auf die Rekursion konzentrieren zu können, fügen wir der abstrakten Syntax für Lambda-Ausdrücke $L$ eine Produktion hinzu:

    $L::=v\mid LL\mid \lambda v.L\mid \mathrm {Fix} \ v.L$.

  • Obige Definition kann man dann mit $f:=\mathrm {Fix} \ f.\ \alpha$ ersetzen; dass so eine Definition vorliegt ist im weiteren aber irrelevant. Die rechte Seite (in der $f$ nicht frei vorkommt!) ist eigenständig.
  • Von der Semantik her wollen wir $[\![\ \mathrm {Fix} \ f.\ \alpha \ ]\!]=[\![\ \alpha [\mathrm {Fix} \ f.\ \alpha \ /\ f]\ ]\!]$ haben.
  • Alternativ könnte man sich überlegen, anstelle von $\mathrm {Fix}$-Termen eine Konstante $\mathrm {Y}$ bereitzustellen:

    $L::=v\mid LL\mid \lambda v.L\mid \mathrm {Y}$,

  wobei $[\![\mathrm {Y} f]\!]=[\![f(\mathrm {Y} f)]\!]$ gelten soll.

  • Ob man nun rekursive Definitionen zulässt, oder ein solches $\mathrm {Y}$ bereitstellt, ist aber egal, denn das eine ist in das andere übersetzbar:

    $\mathrm {Fix} \ f.\ \alpha \quad \rightsquigarrow \quad \mathrm {Y} (\lambda f.\ \alpha )$,

    $\mathrm {Y} \quad \rightsquigarrow \quad \mathrm {Fix} \ Y.\ \lambda f.\ f(Yf)$.

  • Im unigetypten Lambdakalkül gibt es einen ganz normalen $\lambda$-Term ohne freie Variablen, der die Rolle von $\mathrm {Y}$ einnehmen kann. Das gilt auch für unigetypte PCAs mit $\mathrm {S}$ und $\mathrm {K}$.
  • In STLC, was einer intuitionistischen Aussagenlogik entspricht, gibt es keinen solchen $\lambda$-Term (tatsächlich sind alle $\lambda$-definierbaren Funktionen da total; $\lambda f.\ (\lambda x.\ f\ (x\ x))\ (\lambda x.\ f\ (x\ x))$ ist illegal, da nicht typbar). Wenn man dort aber Rekursion oder $\mathrm {Y}$ als Primitiv hinzufügt, wird's als Logik automatisch inkonsistent.
  • Man müsste noch so etwas wie folgendes darlegen: Nehmen wir an, wir wollen die Fibonnacci-Folge als Funktion $f\colon \mathbb {N} \to \mathbb {N}$ in einem STLC+Y definieren.

Das soll ja gerade $\mathrm {Y} (\lambda fn.\ \mathrm {if} \ n<2\ \mathrm {then} \ n\ \mathrm {else} \ f(n-1)+f(n-2))$ sein. Aber der Term, auf den $\mathrm {Y}$ angewandt wird, ist ja selbst ein normaler rekursionsfreier $\lambda$-Term. Welchen Typs und was bedeutet der für sich genommen?

Nun, der hat den Typ $(\mathbb {N} \to \mathbb {N} )\to (\mathbb {N} \to \mathbb {N} )$ und er stellt einen "Approximations-Verbesserer" für das gesuchte (bzw. von $Y$ gefundene) $f$ dar!

Er nimmt eine Approximation für $f$ (als partielle Funktion) und gibt eine neue partielle Funktion zurück, die an mehr Stellen definiert ist als das Eingabe-Approximat, und ansonsten mit ihm konsistent ist. Dieser Strang der Betrachtung geht zum Beispiel in Richtung Bereichstheorie weiter, da der Approximationsverbesserer $\lambda$-definierbar und somit bzgl. der passenden Approximations-Ordnung Scott-stetig ist.

• Das Curry-Paradoxon sollte man vll. ein wenig auswalzen. Ich verstehe zum Beispiel nicht, warum das erwähnt wird (was seit ca. einem Jahr in enWP steht, ist übrigens hochgradig hahnebüchen). Ganz ohne Rekursion können wir $Y$ aus $X\leftrightarrow (X\to Y)$ schließen (STLC):

  $\mathrm {foo} \colon ((X\to Y)\to X)\to (X\to X\to Y)\to Y$,

  $\mathrm {foo} :=\lambda fg.\ (\lambda x.gxx)(f(\lambda x.gxx))$.

Hieran ist erstmal nichts paradox. Im Spezialfall $Y=X$ haben wir als Voraussetzung die Äquivalenz $X\leftrightarrow (X\to X)$, und mit Fixpunktoperator ist dieser Typ für alle $X$ bewohnt. Für manche Typen ist er auch ohne Rekursion zu haben bewohnt. So what? Dass wir mit Fixpunktoperator Inkonsistenz haben, sieht man ja schon an seinem Typ.

Womöglich ist von ThePigDog, der den Unfug in enWP verzapft hat, nicht propositions-as-types gemeint, sondern irgendeine andere Beziehung zur Logik. Es sieht irgendwie so ähnlich aus wie folgende ziemlich dämliche Umsetzung des Lügner-Paradoxons:

• Wir können im unigetypten $\lambda$-Kalkül Booleans definieren,
• dann definieren wir die $\lnot$-Funktion auf den Booleans,
• und zeigen dann mittels $Y$, dass $\lnot$ einen Fixpunkt hat (nämlich: Nicht-Termination). Daraus schließen wir Inkonsistenz!? Käse hoch Zehn.

• Ganz sinnvoll, um nicht allzuviel Chaos zu veranstalten, ist natürlich Literatur!

Gruß, --Daniel5Ko (Diskussion) 23:50, 19. Sep. 2014 (CEST)