"Bewachte" negative Vorkommen bei der Definition von induktiven Typen, immer schlecht?

11

Ich weiß, wie einige negative Ereignisse definitiv schlecht sein können:

data False

data Bad a = C (Bad a -> a)

selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x

yc :: (a -> a) -> a
yc f = selfApp $ C (\x -> f (selfApp x))

false :: False
false = yc id

Ich bin mir jedoch nicht sicher, ob:

Alle induktiven Typen mit negativen Vorkommen können falsch werden.
wenn ja, gibt es einen bekannten mechanischen Weg, dies zu tun;

Zum Beispiel habe ich versucht, diesen Typ falsch zu machen:

type Not a = a -> False

data Bad2 a = C2 (Bad2 (Not a) -> a)

Jeder Hinweis auf Literatur zu diesem Thema wäre willkommen.

lo.logic type-theory soundness Ptival
quelle

1

Ist das Coq? Haskell? Pseudotyp-Theorie? Was meinst du mit "schief gehen"?

Dave Clarke

@ DaveClarke Entschuldigung, der Code ist Haskell, aber es geht mehr um Sprachen wie Coq oder Agda, in denen negative Vorkommen verboten sind. Mit "schief gehen" meine ich, einen Begriff schreiben zu können, der divergiert, und somit False bewohnen zu können, wie ich es in meinem Beispiel in Haskell getan habe.

Ptival

10

Der Grund für das Verbot negativer Vorkommen kann in Analogie zum Knaster-Tarski-Theorem verstanden werden. Dieser Satz sagt das

Wenn ein vollständiges Gitter ist und eine monotone Funktion auf , dann ist die Menge der Fixpunkte von auch ein vollständiges Gitter. Insbesondere gibt es einen kleinsten Fixpunkt und einen größten Fixpunkt . $L$ $f : L \to L$ $L$ $f$ $\mu{f}$ $\nu f$

In der traditionellen Modelltheorie können Gitter als Sätze angesehen werden, und die Ordnungsbeziehung kann als Folge verstanden werden (dh, dass die Wahrheit von die Wahrheit von ). $L$ $p \leq q$ $q$ $p$

Wenn wir von der Modelltheorie zur Beweistheorie übergehen, verallgemeinern sich Gitter auf Kategorien. Typen können als Objekte einer Kategorie , und eine Karte repräsentiert einen Beweis dafür, dass von abgeleitet werden kann . $\mathbb{C}$ $e : P \to Q$ $Q$ $Q$

Wenn wir versuchen, durch rekursive Gleichungen definierte Typen zu interpretieren, ist ee, ist es naheliegend, nach einer Verallgemeinerung des Knaster-Tarski-Theorems zu suchen. Anstelle einer monotonen Funktion auf einem Gitter möchten wir also einenFunktor , der Objekte an Objekte sendet, aber die Monotoniebedingung verallgemeinert, so dass jede Karte eine Karte erhält (mit den Kohärenzbedingungen, dass Identitäten an Identitäten sendet und Kompositionen beibehält, so dass $\mathbb{N} = \mu \alpha.\;1 + \alpha$ $F : \mathbb{C} \to \mathbb{C}$ $e : P \to Q$ $F(e) : F(P) \to F(Q)$ $F$ ). $F(g \circ f) = F(g) \circ F(f)$

Wenn Sie also einen induktiven Datentyp möchten müssen Sie auch eine Funktionsaktion zu Begriffen für den Typoperator bereitstellen, um sicherzustellen, dass der gewünschte Fixpunkt vorhanden ist. Die strenge Positivitätsbedingung in Agda und Coq ist einesyntaktischeBedingung, die diesesemantischeEinschränkungimpliziert. Wenn Sie einen Typoperator aus Summen und Produkten erstellen, können Sie die Funktionsaktion immer zusammenstellen. Daher sollte jeder auf diese Weise gebildete Typ einen festen Punkt haben. $\mu \alpha.\;F(\alpha)$ $F$

In Sprachen mit abhängiger Eingabe haben Sie auch indizierte und parametrisierte Typen, sodass Ihre eigentliche Aufgabe komplizierter ist. Bob Atkey (der hier und hier darüber gebloggt hat ) sagt mir, dass ein guter Ort, um nach der Geschichte zu suchen, ist:

Strukturelle Induktion und Koinduktion in einem fibrationalen Umfeld , Claudio Hermida und Bart Jacobs 1997.
Fibrationsinduktionsregeln für anfängliche Algebren , Neil Ghani, Patricia Johann und Clement Fumex 2010.

Wie Andrej bemerkt, hängt es grundsätzlich davon ab, welches Modell der Typentheorie Sie verwenden, ob ein negatives Auftreten in Ordnung ist oder nicht. Wenn Sie eine rekursive Definition haben, suchen Sie grundsätzlich nach einem Fixpunkt, und in der Mathematik gibt es viele Fixpunktsätze.

Eines, von dem ich persönlich viel Gebrauch gemacht habe, ist Banachs Fixpunktsatz, der besagt, dass wenn Sie eine streng kontraktive Funktion auf einem metrischen Raum haben, er einen eindeutigen Fixpunkt hat. Diese Idee wurde von (IIRC) Maurice Nivat in die Semantik eingeführt, von Amerika und Rutten eingehend untersucht und kürzlich von Birkedal und seinen Mitarbeitern mit einer beliebten Operationstechnik namens "Step-Indexing" in Verbindung gebracht.

Lösung reflexiver Domänengleichungen in einer Kategorie vollständiger metrischer Räume , Pierre America und Jan JMM Rutten 1989.
Die kategorietheoretische Lösung rekursiver metrischer Raumgleichungen , Lars Birkedal, Kristian Støvring und Jacob Thamsborg. 2010.

Dies führt zu Typentheorien, bei denen negative Vorkommen in rekursiven Typen zulässig sind, jedoch nur dann, wenn die negativen Vorkommen unter einem speziellen Konstruktor vom Typ "Schutz" auftreten. Diese Idee wurde von Hiroshi Nakano eingeführt, und die Verbindung zu Banachs Theorem wurde sowohl von mir und Nick Benton als auch von Lars Birkedal und seinen Mitautoren hergestellt.

Eine Modalität für die Rekursion , Hiroshi Nakano, 2000.
Ultrametrische Semantik reaktiver Programme , Nick Benton und Neel Krishnaswami, 2011.
Ein metrisches Modell der vorsichtigen Rekursion , Lars Birkedal, Jan Schwinghammer und Kristian Støvring, 2010.

Neel Krishnaswami
quelle

7

Manchmal kann man rekursive Gleichungen "durch Glück" lösen.

A ≅ (A \to \emptyset) \to A .

$A \cong (A \to \emptyset) \to A.$

$A$ $A \to \emptyset \cong \emptyset$
$A ≅ \emptyset \to A ≅ 1.$ $A \cong \emptyset \to A \cong 1.$ $1$
$A$ $\emptyset \cong (\emptyset \to \emptyset) \to \emptyset \cong 1 \to \emptyset \cong \emptyset$

Fazit: Es gibt zwei Lösungen, den leeren Typ (den Sie aufgerufen haben False) und den Einheitentyp ().

A ≅ (A \to 2) \to 2,

$A \cong (A \to 2) \to 2,$

data Cow a = Moo ((a -> Bool) -> Bool)

$A \cong 2^{2^A}$ $A$ $2^{2^A}$

N ≅ 2^{2^{N}} .

$\mathbb{N} \cong 2^{2^\mathbb{N}}.$

2^{N}

$2^\mathbb{N}$

2^{2^{N}}

$2^{2^\mathbb{N}}$ Integer(Integer -> Bool) -> Bool

Andrej Bauer
quelle

3

Es ist schwer, Andrejs oder Neels Erklärungen etwas hinzuzufügen, aber ich werde es versuchen. Ich werde versuchen, den syntaktischen Standpunkt anzusprechen, anstatt zu versuchen, die zugrunde liegende Semantik aufzudecken, da die Erklärung elementarer ist und ich eine einfachere Antwort auf Ihre Frage gebe.

$\lambda$

Die entscheidende Referenz ist die folgende:

Mendler, N. (1991). Induktive Typen und Typbeschränkungen im Lambda-Kalkül zweiter Ordnung. Ich fürchte, ich habe online keine Referenz gefunden. Die Aussagen und Beweise finden sich jedoch in Nax ' Dissertation (eine sehr empfehlenswerte Lektüre!).

$\mathrm{Bad}$

B a d = B a d \to A

$\mathrm{Bad} = \mathrm{Bad}\rightarrow A$

$A$

λ x : B a d . x x : B a d \to A

$\lambda x:\mathrm{Bad}.x\ x: \mathrm{Bad}\rightarrow A$

und so

(λ x : B a d . x x) (λ x : B a d . x x) : A

$(\lambda x:\mathrm{Bad}.x\ x)\ (\lambda x:\mathrm{Bad}.x\ x): A$

B a d = F (B a d)

$\mathrm{Bad} = F(\mathrm{Bad})$

F (X)

$F(X)$

X

$X$

F (X)

$F(X)$

Natürlich arbeiten Sie nicht mit gleichwertig definierten Typen, sondern mit Konstruktoren , dh Sie haben

data Bad = Pack (Bad -> A)

eher als strenge Gleichheit. Sie können jedoch definieren

unpack :: Bad -> (Bad -> A)
unpack (Pack f) = f

was ausreicht, damit dieses Ergebnis weiterhin gilt:

 (\x:Bad -> unpack x x) (Pack (\x:Bad -> unpack x x))

$A$

In Ihrem zweiten Beispiel sind die Dinge etwas kniffliger, da Sie etwas in der Art von haben

B a d = {B a d}^{'} \to A

$\mathrm{Bad} = \mathrm{Bad}' \rightarrow A$

$\mathrm{Bad}'$ $\mathrm{Bad}$ $\mathrm{Bad}\ a$ $\mathrm{Bad}\ (\mathrm{Not}\ a)$

type Not a = a -> False

mit

data Not a = Not a

Es wäre leicht zu lösen, wenn Haskell solche Typdefinitionen zulassen würde:

type Acc = Not Acc

In diesem Fall können Sie einen Schleifenkombinator genauso erstellen wie zuvor. Ich vermute, Sie können eine ähnliche (aber komplexere) Konstruktion mit tragen

data Acc = D (Not Acc)

Das Problem hierbei ist, einen Isomorphismus aufzubauen

Bad Acc <-> Bad (Not Acc)

Sie müssen mit gemischten Varianz umgehen.

Cody
quelle

"Bewachte" negative Vorkommen bei der Definition von induktiven Typen, immer schlecht?

Antworten: