Что такое

11

Я смотрю на исчисление конструкций и его место в лямбда-кубе .

Если я правильно понимаю, каждая ось куба может рассматриваться как добавление еще одной операции, связанной с типами, к простому типу исчисления, λ . Первая ось добавляет операторы типа к термину, вторые операторы типа к типу и третью зависимую типизацию или операторы типа к типу. У CoC есть все три.

Тем не менее, УПС вводит термин Prop , и утверждает , что Prop:Type с помощью правил вывода , но в противном случае не используются. Я понимаю, что это для одноименных предложений, но логические предложения не определены в терминах этого.

Не могли бы вы объяснить мне, для чего Prop , где / когда он появляется, и объяснить это в терминах осей куба (если это действительно возможно)?

Майкл Роусон
источник

Ответы:

15

В традиционной теории типов Мартина-Лёфа нет различия между типами и суждениями. Это идет под лозунгом «предложения как типы». Но иногда есть причины отличать их. CoC делает именно это.

Prop:Type
Type:PropPropPropType1Type2Type3
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)

Самое интересное - это разница между вторым и четвертым случаем. Четвертые правила говорит , что если находится в -му Вселенной и находится в -й вселенной, то произведение находится в -му Вселенной. Но второе правило говорит нам , что это не просто «еще одна вселенная на дне», потому что земли в , как только не делает, не важно , насколько велика есть. Это непредикативное , потому что позволяет определить элементыAiB(x)jmax(i,j)Propx:AB(x)PropB(x)APropпутем количественного определения самого .Prop

Конкретным примером будет против Первый продукт находится в , но второй находится в (а не в , хотя мы количественно определяем элемент ). В частности, это означает , что один из возможных значений является сам.

A:Type1AA
A:PropAA
Type2PropType1Type1AA:PropAA
Андрей Бауэр
источник