Pie语言中which-Nat克隆函数wN的正确类型定义问询

which-Nat是自然数的case消去算子，核心逻辑是对目标自然数target做分支处理：若为0则返回base，若为add1 n则返回(step n)。其正确的PIE类型声明应直接将所有参数绑定在Π中，而非嵌套多余的→（原错误就是多套了一层→，导致类型不匹配）。

正确的wN类型与代码实现 #

(claim wN
       (Π ((E      U)
           (target Nat)
           (base   E)
           (step   (→ Nat E)))
          E))

(define wN
  (λ (E target base step)
    (which-Nat target base step)))

关键解释 #

1. 对齐iN的结构：Π直接绑定所有参数——类型参数E、目标自然数target、0分支的返回值base、add1分支的处理函数step，最终返回类型为E。
2. 原错误原因：→的参数必须是类型，而target是Nat值、base是E值，不能作为→的参数类型。Π才是PIE中用于绑定带类型参数的正确构造。
3. 匹配官方签名：这个类型完全对应官方文档中which-Nat的定义：
   • target : Nat
   • base : X（对应这里的E）
   • step : (→ Nat X)
   • 返回值类型X（对应这里的E）

测试验证 #

;; 测试0的分支
(wN Nat 0 0 (λ (smaller) smaller)) ; 输出(the Nat 0)

;; 测试add1分支（17对应add1 16）
(wN Nat 17 0 (λ (smaller) smaller)) ; 输出(the Nat 16)

内容的提问来源于stack exchange，提问作者Reb.Cabin