是否有可能推导出教会编码的 Nat 的归纳法？

Question

我只是想知道是否有可能在 Idris、Agda、Coq 和类似的系统上推导出教会编码的 Nat 类型的归纳法。请注意，这与在 CoC 上执行此操作（众所周知这是不可能的）是不同的问题，因为我们对这些具有更多的表达能力（例如，我们能够提取 Sigma 的第二个元素）。

这是 Idris 上的一个糟糕的证明草图（有很多语法问题）：

CN : Type
CN = (t : Type) -> t -> (t -> t) -> t

CS : CN -> CN
CS n t z s = s (n t z s)

CZ : CN
CZ t z s = z

ind :
  (p : CN -> Type) ->
  (z : p CZ) ->
  (s : (n : CN) -> p n -> p (CS n)) ->
  (n : CN) ->
  p n

ind p z s n =
  let base_case  = the (x : CN ** p x) (CZ ** z) 
      step_case  = the ((x : CN ** p x) -> (y : CN ** p y)) (\ (n ** pf) => (CS n ** s n pf))
      result     = the (x : CN ** p x) (n (x : CN ** p x) base_case step_case)
      fst_result = fst result
      snd_result = snd result
      fst_is_n   = the (fst_result = n) ?fst_is_n
  in  ?wat

我正在构建一个从 CZ ** z 一直到 CS (CS ... CZ) ** s (s ... z) 的 Sigma 类型。问题是，虽然我知道它的第一个元素等于 n，但我不确定如何证明它。

Answer 1

我认为没有正式的证据表明这是不可能的，但普遍认为这是不可能的。参见例如this paper by Aaron Stump.

简介

Answer 2

这是related question我问的同伦类型理论。我在这里也有点深奥，所以对这一切持保留态度。

我已经证明 CN is isomorphic to Nat iff the free theorm for CN holds. Furthermore, it's known that there are no free theorems under the law of excluded middle（在 HoTT 中）。 IE。使用 LEM，您可以定义 CN，例如

foo : CN
foo T z s = if T is Bool then not z else z

这不是一个合适的自然教会，不会被归纳法所涵盖。因为排中和 HoTT 与您所询问的类型理论一致（据我所知），因此不会有 ind.

的证明

Answer 3

众所周知，这是不可证明的，因为存在结构演算模型，其中自然数的非谓词编码不是初始的（即不满足归纳法）。正如 Phil Wadler 很久以前展示的那样，它确实遵循关系参数。因此，将 Wadler 与内部关系参数 ala Moulin 和 Bernardy 结合起来可能会成功。

是否有可能推导出教会编码的 Nat 的归纳法？

Is it possible to derive induction for the church-encoded Nat?

haskell

functional-programming

coq

agda

idris