时间戳

首页 > 解决方案 > 依赖对的 Church 编码

coq - 依赖对的 Church 编码

问题描述

人们可以轻松地对这样的对进行 Church-encode：

Definition prod (X Y:Set) : Set := forall (Z : Set), (X -> Y -> Z) -> Z.

Definition pair (X Y:Set)(x:X)(y:Y) : prod X Y := fun Z xy => xy x y.

Definition pair_rec (X Y Z:Set)(p:X->Y->Z) (xy : prod X Y) : Z := xy Z p.

Definition fst (X Y:Set)(xy:prod X Y) : X := pair_rec X Y X (fun x y => x) xy.

Definition snd (X Y:Set)(xy:prod X Y) : Y := pair_rec X Y Y (fun x y => y) xy.

然后很容易将其推广到这样的依赖对：

Definition dprod (X:Set)(Y:X->Set) : Set :=
forall (Z : Set), (forall (x:X),Y x->Z)->Z.

Definition dpair (X:Set)(Y:X->Set)(x:X)(y:Y x) : dprod X Y :=
fun Z xy => xy x y.

Definition dpair_rec (X:Set)(Y:X->Set)(Z:Set)(p:forall (x:X),Y x->Z)
(xy : dprod X Y) : Z := xy Z p.

Definition dfst (X:Set)(Y:X->Set)(xy:dprod X Y) : X :=
dpair_rec X Y X (fun x y => x) xy.

Definition dsnd (X:Set)(Y:X->Set)(xy:dprod X Y) : Y (dfst X Y xy) :=
dpair_rec X Y (Y (dfst X Y xy)) (fun x y => y) xy.

但是最后一个定义失败并显示错误消息：

In environment
X : Set
Y : X -> Set
xy : dprod X Y
x : X
y : Y x
The term "y" has type "Y x"
while it is expected to have type 
"Y (dfst X Y xy)".

我理解这里的问题。但是解决方案是什么？换句话说，如何对依赖对进行 Church 编码？

标签： coqagdadependent-typechurch-encoding

解决方案

首先，让我们正确理解术语。

你所说dprod的实际上是一个“依赖和”，而“依赖积”是你可能会想称之为“依赖函数”的东西。原因是依赖函数泛化了常规产品，你只需要巧妙地使用Bool：

prod : Set -> Set -> Set
prod A B = (b : Bool) -> case b of { True -> A; False -> B; }
{-
The type-theoretic notation would be:
prod A B = Π Bool (\b -> case b of { True -> A; False -> B; })
-}

mkPair : (A B : Set) -> A -> B -> prod A B
mkPair A B x y = \b -> case b of { True -> x; False -> y; }

elimProd : (A B Z : Set) -> (A -> B -> Z) -> prod A B -> Z
elimProd A B Z f p = f (p True) (p False)

本着同样的精神，从属对（通常表示为Σ）概括了正则和：

sum : Set -> Set -> Set
sum A B = Σ Bool (\b -> case b of { True -> A; False -> B; })

mkLeft : (A B : Set) -> A -> sum A B
mkLeft A B x = (True, x)

mkRight : (A B : Set) -> B -> sum A B
mkRight A B y = (False, y)

elimSum : (A B Z : Set) -> (A -> Z) -> (B -> Z) -> sum A B -> Z
elimSum A B Z f _ (True, x) = f x
elimSum A B Z _ g (False, y) = g y

这可能会令人困惑，但另一方面，Π A (\_ -> B)是常规函数的类型，而是Σ A (\_ -> B)常规对的类型（例如，请参见此处）。

所以，再一次：

  • 相关产品 = 相关函数的类型
  • 依赖总和 = 依赖对的类型

您的问题可以用以下方式重新表述：

是否存在通过依赖产品对依赖总和进行 Church 编码？

之前已经在 Math.StackExchange 上问过这个问题，这里有一个答案，它给出了与你的编码基本相同的编码。

但是，阅读对此答案的评论，您会注意到它显然缺乏预期的归纳原则。还有一个类似的问题，但关于自然数的 Church-encoding，这个答案（特别是评论）可以解释为什么 Coq 或 Agda 不足以推导出归纳原理，您需要额外的假设，例如参数性。MathOverflow 上还有另一个类似的问题，虽然对于 Agda/Coq 的具体情况，答案没有给出明确的“是”或“否”，但它们暗示这很可能是不可能的。

最后，我不得不提一下，与当今许多其他类型论问题一样，显然HoTT 就是答案。引用 Mike Shulman 博客文章的开头：

在这篇文章中，我将争辩说，在 Awodey-Frey-Speight 之前的工作的基础上，（更高的）归纳类型可以使用具有完全依赖归纳原则的禁言编码来定义——特别是，在没有任何截断假设的情况下消除所有类型族——在普通（命令式）Book HoTT 中没有任何进一步的花里胡哨。

（尽管您将获得的（不可预测的）编码很难称为 Church 编码。）

推荐阅读