Strikte Positivität

10

Aus dieser Referenz: Strikte Positivität

Die strenge Positivitätsbedingung schließt Erklärungen wie z

data Bad : Set where
 bad : (Bad → Bad) → Bad
         A      B       C
 -- A is in a negative position, B and C are OK

Warum ist A negativ? Auch warum ist B erlaubt? Ich verstehe, warum C erlaubt ist.

Pushpa
quelle
1
Ich bin nicht sicher, warum dies als "negativ" bezeichnet wird, aber es ist allgemeiner durch den Fehler bekannt, den es erzeugt: Stapelüberlauf :) Dieser Code kann eine unendliche Erweiterung des AStapels verursachen und ihn schließlich explodieren lassen (in stapelbasierten Sprachen).
wvxvw
Ich verstehe, dass Sie beliebige Dinge schreiben können und daher die Berechnung nicht beendet wird. danke
Pushpa
1
Ich denke, es wäre eine gute Sache, die Nichtbeendigung im Text Ihrer Frage zu erwähnen . Ich habe meine Antwort basierend auf Ihrem Kommentar aktualisiert.
Anton Trunov
@wvxvw Nicht unbedingt, es kann nur für immer laufen, ohne den Stapel in die Luft zu jagen, vorausgesetzt, der Compiler implementiert die Schwanzrekursion, z. B. mein Beispiel in OCaml unten explodiert den Stapel nicht.
Anton Trunov
1
@AntonTrunov sicher, es war eher ein Wortspiel auf den Namen der Site als ein Versuch, genau zu sein.
wvxvw

Antworten:

17

ABAB

Nun zu induktiven Datentypen.

TTT

In der Algebra ist es üblich, dass eine Operation eine endliche Anzahl von Argumenten akzeptiert, und in den meisten Fällen werden null (konstant), ein (unär) oder zwei (binär) Argumente verwendet. Es ist zweckmäßig, dies für Konstruktoren von Datentypen zu verallgemeinern. Angenommen, es chandelt sich um einen Konstruktor für einen Datentyp T:

  • Wenn ces sich um eine Konstante handelt, können wir sie als Funktion unit -> Toder gleichwertig betrachten (empty -> T) -> T.
  • Wenn ces unär ist, können wir es uns als eine Funktion T -> Toder gleichwertig vorstellen (unit -> T) -> T.
  • Wenn ces binär ist, können wir es uns als eine Funktion T -> T -> Tvorstellen T * T -> T, oder gleichwertig oder gleichwertig (bool -> T) -> T.
  • Wenn wir einen Konstruktor cmit sieben Argumenten wollten , könnten wir ihn als eine Funktion betrachten, (seven -> T) -> Tbei der sevenes sich um einen zuvor definierten Typ mit sieben Elementen handelt.
  • Wir können auch einen Konstruktor haben, cder unendlich viele Argumente akzeptiert, das wäre eine Funktion (nat -> T) -> T.

Diese Beispiele zeigen, dass die allgemeine Form eines Konstruktors sein sollte

c : (A -> T) -> T

wo wir Adie Arität von nennen cund uns cals einen Konstruktor Avorstellen , der viele Argumente vom Typ verwendet T, um ein Element von zu erzeugen T.

Hier ist etwas sehr Wichtiges: Die Aritäten müssen definiert werden, bevor wir sie definieren T, sonst können wir nicht sagen, was die Konstruktoren tun sollen. Wenn jemand versucht, einen Konstruktor zu haben

broken: (T -> T) -> T

dann die Frage "Wie viele Argumente braucht brokenman?" hat keine gute Antwort. Sie könnten versuchen, es mit "es braucht- Tviele Argumente" zu beantworten , aber das geht nicht, weil Tes noch nicht definiert ist. Wir könnten versuchen, aus dem Cunundrum herauszukommen, indem wir eine ausgefallene Festpunkttheorie verwenden, um einen Typ Tund eine injizierende Funktion zu finden (T -> T) -> T, und würden Erfolg haben, aber wir würden auch das Induktionsprinzip für Tunterwegs brechen . Es ist also nur eine schlechte Idee, so etwas auszuprobieren.

λvλvcB

c : B * (A -> T) -> T

Tatsächlich können viele Konstrukteure auf diese Weise neu geschrieben werden, aber nicht alle, brauchen wir einen weiteren Schritt, nämlich sollten wir zulassen , dass hängen auf :AB

c : (∑ (x : B), A x -> T) -> T

Dies ist die endgültige Form eines Konstruktors für einen induktiven Typ. Es ist auch genau das, was W-Typen sind. Die Form ist so allgemein, dass wir immer nur einen einzigen Konstruktor brauchen c! In der Tat, wenn wir zwei davon haben

d' : (∑ (x : B'), A' x -> T) -> T
d'' : (∑ (x : B''), A'' x -> T) -> T

dann können wir sie zu einem kombinieren

d : (∑ (x : B), A x -> T) -> T

wo

B := B' + B''
A(inl x) := A' x
A(inr x) := A'' x

Übrigens, wenn wir die allgemeine Form curry sehen, sehen wir, dass es äquivalent zu ist

c : ∏ (x : B), ((A x -> T) -> T)

Das ist näher an dem, was die Leute tatsächlich in Beweisassistenten aufschreiben. Die Proof-Assistenten ermöglichen es uns, die Konstruktoren auf bequeme Weise aufzuschreiben, aber diese entsprechen der obigen allgemeinen Form (Übung!).

Andrej Bauer
quelle
1
Nochmals vielen Dank Andrej nach meinem Mittagessen, das wird für mich am schwersten zu verdauen sein. Prost.
Pushpa
9

Das erste Vorkommen von Badwird als "negativ" bezeichnet, da es ein Funktionsargument darstellt, dh sich links vom Funktionspfeil befindet (siehe Rekursive Typen kostenlos von Philip Wadler). Ich denke, der Ursprung des Begriffs "negative Position" ergibt sich aus dem Begriff der Kontravarianz ("Kontra" bedeutet Gegenteil).

Es ist nicht erlaubt, den Typ in einer negativen Position zu definieren, da man damit nicht terminierende Programme schreiben kann, dh eine starke Normalisierung schlägt in seiner Gegenwart fehl (mehr dazu weiter unten). Dies ist übrigens der Grund für den Namen der Regel "strikte Positivität": Wir erlauben keine negativen Positionen.

Wir erlauben das zweite Auftreten von, Badda es keine Nichtbeendigung verursacht, und wir möchten den Typ, der definiert wird ( Bad), irgendwann in einem rekursiven Datentyp ( vor dem letzten Pfeil seines Konstruktors) verwenden.

Es ist wichtig zu verstehen, dass die folgende Definition nicht gegen die strenge Positivitätsregel verstößt.

data Good : Set where
  good : Good → Good → Good

Die Regel gilt nur für Konstruktorargumente ( Goodin diesem Fall beide ) und nicht für einen Konstruktor selbst (siehe auch Adam Chlipalas " Zertifizierte Programmierung mit abhängigen Typen ").

Ein weiteres Beispiel, das gegen strikte Positivität verstößt:

data Strange : Set where
  strange : ((Bool → Strange) → (ℕ → Strange)) → Strange
                       ^^     ^
            this Strange is   ...this arrow
            to the left of... 

Vielleicht möchten Sie diese Antwort auch auf negative Positionen überprüfen .


Weitere Informationen zur Nichtbeendigung ... Die Seite, auf die Sie verwiesen haben, enthält einige Erklärungen (zusammen mit einem Beispiel in Haskell):

Nicht streng positive Deklarationen werden abgelehnt, weil man damit eine nicht terminierende Funktion schreiben kann. Informationen zum Schreiben einer Schleifendefinition mit dem Datentyp Bad von oben finden Sie unter BadInHaskell .

Hier ist ein analoges Beispiel in Ocaml, das zeigt, wie rekursives Verhalten implementiert wird, ohne (!) Die Rekursion direkt zu verwenden:

type boxed_fun =
  | Box of (boxed_fun -> boxed_fun)

(* (!) in Ocaml the 'let' construct does not permit recursion;
   one have to use the 'let rec' construct to bring 
   the name of the function under definition into scope
*)
let nonTerminating (bf:boxed_fun) : boxed_fun =
  match bf with
    Box f -> f bf

let loop = nonTerminating (Box nonTerminating)

Die nonTerminatingFunktion "entpackt" eine Funktion aus ihrem Argument und fügt sie dem ursprünglichen Argument hinzu. Was hier wichtig ist, ist, dass die meisten Typsysteme keine Übergabe von Funktionen an sich selbst zulassen, so dass ein Begriff wie f f"nicht typecheck" ist, da es keinen Typ gibt f, der den typechecker erfüllt. Einer der Gründe für die Einführung von Typsystemen ist die Deaktivierung der Selbstanwendung (siehe hier ).

Das Umschließen von Datentypen wie dem oben eingeführten kann verwendet werden, um diese Straßensperre auf dem Weg zur Inkonsistenz zu umgehen.

Ich möchte hinzufügen, dass nicht terminierende Berechnungen zu Inkonsistenzen bei Logiksystemen führen. Im Fall von Agda und Coq hat der Falseinduktive Datentyp keine Konstruktoren, sodass Sie niemals einen Beweisbegriff vom Typ False erstellen können. Aber wenn nicht terminierende Berechnungen erlaubt wären , könnte man dies zum Beispiel so machen (in Coq):

Fixpoint loop (n : nat) : False = loop n

Dann loop 0würde typecheck geben loop 0 : False, also würde es unter Curry-Howard-Korrespondenz bedeuten, dass wir eine falsche Aussage bewiesen haben.

Fazit : Die strenge Positivitätsregel für induktive Definitionen verhindert nicht terminierende Berechnungen, die für die Logik katastrophal sind.

Anton Trunov
quelle
Jetzt bin ich verwirrt. Speziell Daten Gut: Legen Sie fest, wo gut: Gut → Gut →. Wir werden versuchen zu verstehen und in einer Stunde zurück zu kommen /
Pushpa
Die Regel gilt nicht für den Konstruktor selbst, sondern nur für seine Argumente, dh Pfeile auf der obersten Ebene einer Konstruktordefinition spielen keine Rolle. Ich habe auch ein weiteres (indirektes) Verstoßbeispiel hinzugefügt.
Anton Trunov