Можно ли извлечь второй элемент сигмы по исчислению конструкций с простыми несовместными аксиомами?

Это кажется невозможным для извлечения второго элемента сигмы по исчислению конструкций. Более того, похоже, что не существует известного простого способа расширить исчисление конструкций с зависимыми исключениями без потери согласованности. Таким образом, как можно использовать простую но непоследовательную аксиому (такую ​​как Type : Type или неограниченную рекурсию, такую ​​как μ) для извлечения второго элемента сигмы?

То есть, учитывая следующий конструктор Sigma:

Sigma =
  λ A : *
  λ B : A -> *
  λ a : A
  λ b : B
  λ Data : *
  λ Sigma :
    ∀ fst : A
    ∀ snd : B fst
    Data
  Sigma a b

Можно ли на языке, эквивалентном исчислению конструкций, за исключением Type : Type или какой-либо другой простой непоследовательной аксиомы, реализовать функцию, которая по заданному термину, такому как Sigma Nat (\x -> Nat) 3 6, извлекает второе значение, 6?


functional-programming haskell idris coq agda
person MaiaVictor    schedule 15.12.2017    source источник
comment
ИМХО надо конкретизировать свой вопрос, в частности какие у вас условия добычи. Очевидно, что если мое исчисление непоследовательно, я могу извлечь все, что захочу, посредством исключения дна.   -  person ejgallego    schedule 15.12.2017
comment
@ejgallego может быть очевидным для вас, но не для меня! Я сделал вопрос более точным, как и просили.   -  person MaiaVictor    schedule 15.12.2017
comment
Действительно, вопрос теперь более точен, поскольку вы хотите, чтобы извлечение восстановило исходный термин по модулю правил редукции. Я не имел в виду, что вопрос был очевиден, но на самом деле добавление противоречивых аксиом обычно подразумевает, что вы можете определить тривиальную функцию извлечения, поэтому нужно быть осторожным с точным определением.   -  person ejgallego    schedule 15.12.2017

Ответы (1)


arrow_upward
5
arrow_downward

В контексте теории типов, такой как теория типов Мартина-Лёфа или исчисление конструкций, под «несогласованностью» мы обычно подразумеваем логическую несогласованность: возможность вывести терм contra типа forall T : Type, T. При этом любой другой тип T становится обитаемым: достаточно применить к нему contra.

К сожалению, в большинстве теорий типов обитаемость ничего не говорит нам о конвертируемости или равенстве определений, потому что ни один тип не выражает, что два термина x и y могут быть конвертируемы. Это означает, что нет способа вывести термины

fst : Sigma A B -> A
snd : forall s : Sigma A B, B (fst s)

так что fst (Sigma _ _ x y) упрощается до x, а snd (Sigma _ _ x y) упрощается до y, ссылаясь на логическое противоречие. (Я немного злоупотребил обозначениями и использовал Sigma как для конструктора, так и для типа.) Однако вы можете использовать contra, чтобы постулировать существование fst и snd и утверждать, что соответствующие уравнения выполняются пропозиционально.

В простом CoC мы говорим, что два термина x1 и x2 пропозиционально равны, если существует термин типа

forall T, T x1 -> T x2

(Иногда это известно как равенство Лейбница: два термина равны, если каждый предикат, который выполняется для первого, выполняется и для второго.) Утверждение аналогичного для snd несколько сложнее, потому что snd (Sigma _ _ x y) и y не имеют одинаковых типов ( первый имеет тип B (fst (Sigma _ _ x y)), а второй — тип B x). Мы можем исправить это, утверждая леммы об упрощении для fst и snd одновременно:

forall (T : forall x : A, B x -> Type),
  T (fst (Sigma _ _ x y)) (snd (Sigma _ _ x y)) -> 
  T x y

Редактировать

Что касается вашего комментария: поскольку конвертируемость обычно не может быть выражена с помощью типа, нам нужно изменить его определение в теории типов, чтобы иметь истинный сигма-тип с первой и второй проекциями - более тонкая операция, чем просто постулирование того, что определенные аксиомы выполняются. Есть несколько систем, которые это позволяют, например Dedukti, средство проверки доказательств, разработанное в Inria.

person Arthur Azevedo De Amorim    schedule 15.12.2017
comment
Ах, проницательно и отвечает на вопрос. Однако мне интересно, какая аксиома используется для его извлечения. На Coq это возможно, но я не уверен, что за этим стоит логика. Но спасибо за ответ, это то, что я спросил. - person MaiaVictor; 17.12.2017
comment
@MaiaVictor Добавлено несколько деталей. - person Arthur Azevedo De Amorim; 18.12.2017