haskell - 是否有可能在具有简单不一致公理的构造演算中提取 Sigma 的第二个元素？

Question

它seems to be impossible提取构造微积分上西格玛的第二个元素。此外，似乎没有已知的、简单的方法可以在不失去一致性的情况下通过相关消除来扩展构造微积分。因此，如何利用一个简单但不一致公理(例如 Type : Type 或无限制递归，例如 μ )来提取 Sigma 的第二个元素？

也就是说，给定以下 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 ？

Answer 1

在类型理论(例如 Martin-Löf 类型理论或构造微积分)的背景下，我们所说的“不一致”通常指的是逻辑不一致:能够导出一个术语 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 开发的证明检查器。