Was ist

11

Ich betrachte die Konstruktionsrechnung und ihren Platz im Lambda-Würfel .

Wenn ich das richtig verstehe, kann man sich vorstellen, dass jede Achse des Würfels eine weitere Operation mit Typen zum einfach typisierten Kalkül hinzufügt λ. Die erste Achse fügt Typ-zu-Term-Operatoren, die zweiten Typ-zu-Typ-Operatoren und die dritte abhängige Typisierung oder Term-zu-Typ-Operatoren hinzu. Der CoC hat alle drei.

Der CoC führt jedoch einen Begriff Prop und gibt an, dass Prop:Type nach den Inferenzregeln , aber ansonsten nicht verwendet wird. Ich verstehe, dass es für die gleichnamigen Sätze ist, aber die logischen Sätze sind nicht in Bezug darauf definiert.

Könnten Sie mir erklären, wofür Prop ist, wo / wann es erscheint, und es anhand der Achsen des Würfels erklären (falls dies tatsächlich möglich ist)?

Michael Rawson
quelle

Antworten:

15

In der traditionellen Martin-Löf-Typentheorie gibt es keinen Unterschied zwischen Typen und Sätzen. Dies steht unter dem Motto "Sätze als Typen". Aber es gibt manchmal Gründe, sie zu unterscheiden. CoC macht genau das.

Es gibt viele Varianten von CoC, aber die meisten hätten aber nicht T y p e : P r o p . Ein weiterer Unterschied zeigt sich, wenn wir unendlich viele Typuniversen haben und P r o p improvisieren (dies ist, was Coq tut). Betrachten Sie konkret eine Variante von CoC, bei der wir P r o p und unendlich viele Typuniversen T y p e 1 , T y p e haben

Prop:Type
Type:PropPropPropType1 , T y p e 3 mit P r o pType2Type3 Die Bildungsregel fürmuss erklären, wiex gebildet wird:AB(x),wennAentweder ein Satz oder ein Typ ist undB(x)entweder ein Satz oder ein Typ ist. Es gibt vier Kombinationen:
Prop:Type1Type1:Type2Type2:Type3
x:AB(x)AB(x)
  1. A:Propx:AB(x):Propx:AB(x):Prop
  2. A:Typeix:AB(x):Propx:AB(x):Prop
  3. A:Propx:AB(x):Typeix:AB(x):Typei
  4. A:Typeix:AB(x):Typejx:AB(x):Typemax(i,j)

The most interesting is the difference between the second and the fourth case. The fourth rules says that if A is in the i-th universe and B(x) is in the j-th universe, then the product is in the max(i,j)-th universe. But the second rule is telling us that Prop is not just "one more universe at the bottom", because x:AB(x) lands in Prop as soon as B(x) does, no matter how big A is. This is impredicative because it allows us to define elements of Prop by quantifying over Prop itself.

A concrete example would be

A:Type1AA
versus
A:PropAA
The first product lives in Type2, but the second one is in Prop (and not in Type1, even though we are quantifying over an element of Type1). In particular, this means that one of the possible values for A is A:PropAA itself.
Andrej Bauer
quelle