由于定义上相等(Definitional Equality)作用在所有情况,由此,当遇到不一致(Inconsistent)的时候,会导致其结果是不确定的,即会无限展开(unfolding forever)下去。
原文中,是通过一个定义在自然数(ℕ)的大于关系(>)上的可达类型(Accessibility Type)来论证,这个看原文很好理解,这里就不再赘述了。
关键点:要证明 acc x,x ∈ℕ,那么所有,r y x 的 y 都是 acc y,r ≡ >,即 y > x。由此,在自然数中,有无数个比 x 大的自然数,这样导致不能证明 acc x。如果给定一个 a,其类型为 acc x,那么,在使用该 a: acc x 时,就会对 a 进行无限地展开(unfolding),导致无法停止(Non-terminated)。
下面列出其证明过程:
函数 f 的类型:f : (n: ℕ) → Acc n → 1, 且,1 ≡ Unit, ():Unit,即 ():1.
其中函数 g: ∀y.y>x → 1 ≡ (y: ℕ) → h: (y>x) → 1,意思是,给定一个自然数 y,以及,证明 y > x,那么,该函数就会返回 ()。也就是说,当无法给入 g 的输入参数时,是无法调用 g 的。
另外,函数 g,是在可达类型的使用规则里,给定的,表示使用规则中的前果。因此,根据 可达类型的使用规则(Elimination Rule),即使用函数 rec,函数 g 为 前果,有
g (n + 1) (p n) ≡ f (n + 1) a
≡ f (n+1) (intro (inv a))
≡ f (n+1) (inv a (n + 1) (p n) )
≡ f (n+1) (h (n + 1) (p n) )
其中,h 为 ∀y.y>x → acc y 的证明(proof)。
由此,其步进规则,有
当 n = 0,a : Acc n,即 a : Acc 0,有 a ≡ intro (inv a) ,那么
因此
口