可以为教会编码的Nat归纳吗？ [英] Is it possible to derive induction for the church-encoded Nat?

问题描述

我只是想知道是否有可能对Idris，Agda，Coq等类似物的教堂编码Nat类型进行归纳。请注意，这与在CoC上进行处理（这是不可能的）不同，因为我们在CoC上具有更高的表达能力（例如，我们可以提取Sigma的第二个元素）。

I was just wondering if it is possible to derive induction for the church-encoded Nat type on Idris, Agda, Coq and similar. Notice this is a different issue from doing it on CoC (which is known to be impossible) because we have much more expressivity on those (we're able to, for example, extract the second element of Sigma).

以下是有关Idris的一个不可靠的草图（有很多语法问题）：

Here is a poor proof sketch on Idris (had a lot of syntax issues):

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开始构建Sigma类型来做到这一点* * z 一直到 CS（CS ... CZ）** s（s ... z）。问题是，虽然我知道它的第一个元素将等于 n ，但我不确定如何证明它。

I'm doing it by building a Sigma type starting from CZ ** z all way up to CS (CS ... CZ) ** s (s ... z). Problem is that, while I know the first element of it will be equal to n, I'm not sure how to prove it.

推荐答案

这是一个相关问题我问了同型类型理论。我在这里也不太了解我的情况，所以请带些盐。

Here's a related question I asked about homotopy type theory. I am also a little out my depth here, so take all this with a grain of salt.

我证明了 CN 同构为 Nat c 的自由定理成立，则code>。此外，我们知道根据排除法则没有自由定理中间（在HoTT中）。即使用LEM，您可以定义 CN ，例如

I've proved that 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 (in HoTT). I.e. with LEM, you could could define CNs such as

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

适当的自然教会，不会被归纳原则涵盖。由于排除的中位和HoTT与您所询问的类型理论一致（据我所知），因此得出结论，不会有 ind 的证据。

which is not a proper church natural and would not be covered by the induction principle. Because excluded middle and HoTT are consistent with the type theories you are asking about (as far as I know), it follows that there will not be a proof of ind.

这篇关于可以为教会编码的Nat归纳吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！