agda中的非平凡否定

Question

所有的否定,即我见过的形式A - >底部格式的结论来自荒谬的模式匹配.还有其他可以在agda中得到否定的情况吗？依赖类型理论中是否存在其他可能的情况？

Answer 1

类型理论通常没有模式匹配的概念(并且通过扩展荒谬的模式),但它们可以证明你所描述的那种类型的否定.

首先,我们必须查看数据类型.如果没有模式匹配,您可以通过引入和删除规则来表征它们.引言规则基本上是构造函数,它们告诉您如何构造该类型的值.另一方面,消除规则告诉您如何使用该类型的值.还有相关的计算规则(β减少,有时是η减少),但我们现在不需要处理它们.

消除规则看起来有点像折叠(至少对于正面类型).例如,这里是自然数的消除规则在Agda中的样子:

?-elim : ? {p} (P : ? ? Set p)
  (s : ? {n} ? P n ? P (suc n))
  (z : P 0) ?
  ? n ? P n
?-elim P s z zero    = z
?-elim P s z (suc n) = s (?-elim P s z n)

虽然Agda确实有引入规则(构造函数),但它没有消除规则.相反,它有模式匹配,如上所示,我们可以用它恢复消除规则.但是,我们也可以进行相反的操作:我们可以使用消除规则来模拟模式匹配.说实话,它通常更加不方便,但它可以做到 - 上面提到的消除规则基本上在最外层的构造函数上进行模式匹配,如果我们需要更深入,我们可以再次应用消除规则.

所以,我们可以模拟模式匹配.荒谬的模式怎么样？举个例子,我们将采用第四个Peano公理:

peano : ? n ? suc n ? zero ? ?

然而,有一个技巧涉及(事实上,它是非常关键的;在Martin-Löf的没有宇宙的类型理论中,如果没有这个技巧你就无法做到,请参阅本文).我们需要构造一个函数,它将根据其参数返回两个不同的类型:

Nope : (m n : ?) ? Set
Nope (suc _) zero = ?
Nope _    _       = ?

如果m ? n,我们应该能够证明Nope m n持有(居住).事实上,这很容易:

nope : ? m n ? m ? n ? Nope m n
nope zero    ._ refl = _
nope (suc m) ._ refl = _

您现在可以看到它的前进方向.如果我们申请nope"坏"证明suc n ? zero,Nope (suc n) zero将减少到?,我们将获得所需的功能:

peano : ? n ? suc n ? zero ? ?
peano _ p = nope _ _ p

现在,你可能会注意到我有点作弊.我使用了模式匹配,尽管我之前说过,这些类型的理论没有模式匹配.我将为下一个例子补救,但我建议你尝试证明peano没有模式匹配的数字(?-elim上面给出的用法); 如果你真的想要一个硬核版本,那么在没有相等的模式匹配的情况下做它并使用这个消除器代替:

J : ? {a p} {A : Set a} (P : ? (x : A) y ? x ? y ? Set p)
  (f : ? x ? P x x refl) ? ? x y ? (p : x ? y) ? P x y p
J P f x .x refl = f x

另一种流行的荒谬模式是某种类型的东西Fin 0(从这个例子中,你会知道如何模拟其他如此荒谬的匹配).所以,首先,我们需要消除器Fin.

Fin-elim : ? {p} (P : ? n ? Fin n ? Set p)
  (s : ? {n} {fn : Fin n} ? P n fn ? P (suc n) (fsuc fn))
  (z : ? {n} ? P (suc n) fzero) ?
  ? {n} (fn : Fin n) ? P n fn
Fin-elim P s z fzero    = z
Fin-elim P s z (fsuc x) = s (Fin-elim P s z x)

是的,这种类型真的很难看.无论如何,我们将使用相同的技巧,但这一次,我们只需要依赖一个数字:

Nope : ? ? Set
Nope = ?-elim (? _ ? Set) (? _ ? ?) ?

请注意,这相当于:

Nope zero    = ?
Nope (suc _) = ?

现在,请注意上面的消除器(即s和zcase)的两种情况都返回了类型P (suc n) _.如果我们选择P = ? n _ ? Nope n,我们将不得不?为两种情况返回类型- 但这很容易!事实上,这很简单:

bad : Fin 0 ? ?
bad = Fin-elim (? n _ ? Nope n) (? _ ? _) _

您可能想知道的最后一件事是我们如何获得任何类型的值?(在逻辑中称为ex falso quodlibet).在Agda,我们显然有:

?-elim : ? {w} {Whatever : Set w} ? ? ? Whatever
?-elim ()

但事实证明,这恰恰是消除器?,因此在类型理论中定义这种类型时给出了它.