如何在Scala中证明爆炸原理（ex falso sequitur quodlibet）？

Posted 2023-05-08

【中文标题】如何在Scala中证明爆炸原理（ex falso sequitur quodlibet）？

【英文标题】：How to prove the principle of explosion (ex falso sequitur quodlibet) in Scala?

【发布时间】：2019-03-27 00:45:19

【问题描述】：

在 Scala 中，我如何证明没有构造函数的类型的值可以得出任何结果？我想对值进行模式匹配，并让 Scala 告诉我没有模式可以匹配，但我愿意接受其他建议。下面是一个简短的示例，说明它为何有用。

证明否定

在 Scala 中，可以在类型级别定义自然数，例如使用 Peano 编码。

sealed trait Nat
sealed trait Zero extends Nat
sealed trait Succ[N <: Nat] extends Nat

由此我们可以定义一个数字是偶数的含义。零是偶数，任何比偶数多二的数也是偶数。

sealed trait Even[N <: Nat]
sealed case class Base() extends Even[Zero]
sealed case class Step[N <: Nat](evenN: Even[N]) extends Even[Succ[Succ[N]]]

由此我们可以证明，例如二是偶数：

val `two is even`: Even[Succ[Succ[Zero]]] = Step(Base())

但我无法证明一个不是偶数，即使编译器可以告诉我Base 和Step 都不能容纳该类型。

def `one is odd`(impossible: Even[Succ[Zero]]): Nothing = impossible match 
  case _: Base => ???
  case _: Step[_] => ???

编译器会很高兴地告诉我，我给出的所有情况都不可能出现错误pattern type is incompatible with expected type，但将match 块留空将是一个编译错误。

有什么方法可以建设性地证明这一点？如果空模式匹配是要走的路 - 我会接受任何版本的 Scala 甚至是宏或插件，只要在类型被占用时我仍然会收到空模式匹配的错误。也许我在找错误的树，模式是否匹配错误的想法 - EFQ 可以以其他方式显示吗？

注意：可以用另一个（但等效的）均匀度定义来证明一个是奇数 - 但这不是重点。一个简短的例子说明为什么需要 EFQ：

sealed trait Bottom
def `bottom implies anything`(btm: Bottom): Any = ???

【问题讨论】：

在您的Step 中，它不应该扩展Even[Succ[Succ[N]]] 吗？否则，它只是证明 2 是偶数。

@BrianMcCutchon 你是对的，现在应该修复它。感谢您敏锐的眼光和敏锐的头脑！

【参考方案1】：

对于 Scala 中的任意无人居住类型可能无法证明 ex falso，但仍然可以证明 Even[Succ[Zero]] => Nothing。我的证明只需要对您的 Nat 定义进行少量修改，即可解决 Scala 中缺少的功能。这里是：

import scala.language.higherKinds

case object True
type not[X] = X => Nothing

sealed trait Nat 
  // These dependent types are added because Scala doesn't support type-level
  // pattern matching, so this is a workaround. Nat is otherwise unchanged.
  type IsZero
  type IsOne
  type IsSucc

sealed trait Zero extends Nat 
  type IsZero = True.type
  type IsOne = Nothing
  type IsSucc = Nothing

sealed trait Succ[N <: Nat] extends Nat 
  type IsZero = Nothing
  type IsOne = N#IsZero
  type IsSucc = True.type


type One = Succ[Zero]

// These definitions should look familiar.
sealed trait Even[N <: Nat]
sealed case class Base() extends Even[Zero]
sealed case class Step[N <: Nat](evenN: Even[N]) extends Even[Succ[Succ[N]]]

// A version of scalaz.Leibniz.===, adapted from
// https://typelevel.org/blog/2014/07/02/type_equality_to_leibniz.html.
sealed trait ===[A <: Nat, B <: Nat] 
  def subst[F[_ <: Nat]](fa: F[A]): F[B]


implicit def eqRefl[A <: Nat] = new ===[A, A] 
  override def subst[F[_ <: Nat]](fa: F[A]): F[A] = fa


// This definition of evenness is easier to work with. We will prove (the
// important part of) its equivalence to Even below.
sealed trait _Even[N <: Nat]
sealed case class _Base[N <: Nat]()(
  implicit val nIsZero: N === Zero) extends _Even[N]
sealed case class _Step[N <: Nat, M <: Nat](evenM: _Even[M])(
  implicit val nIsStep: N === Succ[Succ[M]]) extends _Even[N]

// With this fact, we only need to prove not[_Even[One]] and not[Even[One]]
// will follow.
def `even implies _even`[N <: Nat]: Even[N] => _Even[N] = 
  case b: Base => _Base[Zero]()
  case s: Step[m] =>
    val inductive_hyp = `even implies _even`[m](s.evenN) // Decreasing on s
    _Step[N, m](inductive_hyp)


def `one is not zero`: not[One === Zero] = 
  oneIsZero =>
    type F[N <: Nat] = N#IsSucc
    oneIsZero.subst[F](True)


def `one is not _even` : not[_Even[One]] = 
  case base: _Base[One] =>
    val oneIsZero: One === Zero = base.nIsZero
    `one is not zero`(oneIsZero)
  case step: _Step[One, m] =>
    val oneIsBig: One === Succ[Succ[m]] = step.nIsStep
    type F[N <: Nat] = N#IsOne
    oneIsBig.subst[F](True)


def `one is odd`: not[Even[One]] =
  even1 => `one is not _even`(`even implies _even`(even1))

【讨论】：

这很有趣。可以添加even(N)⇒not(even(succ(N))) 的证明吗？ not(even(N))⇒even(succ(N)) 呢？我很难构建这些。

@n.m.也许我稍后会尝试这些。如果有帮助，我首先在 Coq 中证明了这一点，然后将其翻译成 Scala，使用 Coq Print 命令查看生成的更复杂定理的代码。 ===.subst 大致相当于 Coq 的 eq_ind。翻译是最难的部分。

【参考方案2】：

Ex falso quodlibet 意思是“从矛盾中，任何事情都随之而来”。 在标准 Curry-Howard 编码中，Nothing 对应于 假的，所以下面这个简单的函数实现了原理 爆炸：

def explode[A]: Nothing => A = n => n

它可以编译，因为Nothing是如此无所不能 替换任何东西 (A)。

然而，这并没有给你带来任何东西，因为你最初的 假设从

There is no proof for `X`

这样

There must be proof for `X => _|_`

不正确。这不仅对于直觉/建设性逻辑是不正确的，而且在一般情况下：只要您的系统能够计数，就会出现 是不能被证明的真实陈述，所以在每一个一致的 带有Peano naturals的系统必须有一些陈述X 这样X 不能被证明（由 Goedel），并且它们的否定 X => _|_ 也无法证明（通过一致性）。

看来你在这里需要的是某种“反转引理”（在 Pierce 的“类型和编程语言”的意义上），它限制了某些类型的术语可以构造的方式，但我不'在 Scala 的类型系统中看不到任何可以为您提供此类引理的类型级编码的东西。

【讨论】：

非常感谢您的回答。我无意暗示排中律一般是正确的。在我上面的尝试证明中，编译器高兴地告诉我我的情况是不可能的——所以在某种程度上它已经知道错误已经发生了。同样的证明应该在直觉逻辑中起作用，或者在例如。阿格达。 Bottom 类型应该与 Nothing 同构，因为它们具有相同的构造函数。但是Nothing 通过成为所有事物的子类型，从编译器那里获得了神奇的属性，这是explode 使用的属性。

@DrPhil 您再次混淆了对象语言和元语言的级别。陈述“有X 的证据” 不是对*“有`X => _|_"*. Those are two meta-theoretic statements about two different types X` 和X => _|_ 是否有人居住的证据的否定。这与 LEM 所在的领域完全不同。LEM（对于这种特殊情况）将是 [X].(X \/ (X => _|_)) 类型的术语，其中 \/ 是连词（对应于大致类似于 Either-type 构造函数的东西）， [X] 是对类型变量 X 的通用量化。

@DrPhil 我希望你能认识到声明 "Step(Base()) 的类型是 Even[Succ[Succ[Zero]]]" 并且声明 "Bob 坐在他的面前计算机并且找不到 Even[Succ[Zero]] => Nothing" 类型的 Scala 术语，它们生活在完全不同的领域。

@DrPhil 还有一句话：不，Bottom 类型与没有任何构造函数或值的简单类型不同。从 Curry-Howard-Lambek 同构的角度来看，重要的正是通用属性：对于 Bottom 类型，它必须持有 对于每个其他 X 存在来自 @ 的唯一态射987654348@到X，即必须是初始对象。上面的def explode 证明了Nothing 具有这个通用属性。

@DrPhil 在第二条评论中，您会看到如果将元语言与对象语言混合会发生什么：我在_|_ 之后忘记了一个反引号，现在降价搞砸了，并且整个句子都是灰色的……