问题描述
给定以下 Peano 数的类型级加法函数
sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat
type plus[a <: Nat,b <: Nat] = a match
case O => b
case S[n] => S[n plus b]
说我们想证明定理
对于所有自然数 n,n + 0 = n
也许可以这样指定
type plus_n_0 = [n <: Nat] =>> (n plus O) =:= n
那么在为定理提供证据时,我们可以很容易地要求 Scala 编译器在特定情况下提供证据
summon[plus_n_O[S[S[O]]]] // ok,2 + 0 = 2
但是我们如何问 Scala 是否可以为 [n <: Nat]
的所有实例生成证据,从而提供 plus_n_0
的证明?
解决方法
这是一种可能的方法,尝试对本段进行字面解释:
当证明一个关于所有自然数的陈述E:N→U
时,只要证明它对于0
和succ(n)
就足够了,假设它对于n
成立,即我们构造ez:E(0)
和 es:∏(n:N)E(n)→E(succ(n))
。
来自the HoTT book (section 5.1)。
这是下面代码中实现的计划:
-
为“某些性质
P
对所有自然数成立”的陈述提出证明意味着什么。下面,我们将使用trait Forall[N,P[n <: N]]: inline def apply[n <: N]: P[n]
apply
方法的签名实质上是说“对于所有n <: N
,我们可以生成P[n]
的证据”。请注意,该方法声明为
inline
。这是确保∀n.P(n)
的证明在运行时具有建设性和可执行性的一种可能方法(但是,请参阅具有手动生成的见证条款的替代提案的编辑历史记录)。 -
假设某种自然数的归纳原理。下面,我们将使用以下公式:
If P(0) holds,and whenever P(i) holds,then also P(i + 1) holds,then For all `n`,P(n) holds
我相信应该可以使用一些元编程工具
derive
这样的归纳原则。 -
为归纳原理的基本案例和归纳案例编写证明。
-
???
-
利润
代码如下所示:
sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat
type plus[a <: Nat,b <: Nat] <: Nat = a match
case O => b
case S[n] => S[n plus b]
trait Forall[N,P[n <: N]]:
inline def apply[n <: N]: P[n]
trait NatInductionPrinciple[P[n <: Nat]] extends Forall[Nat,P]:
def base: P[O]
def step: [i <: Nat] => (P[i] => P[S[i]])
inline def apply[n <: Nat]: P[n] =
(inline compiletime.erasedValue[n] match
case _: O => base
case _: S[pred] => step(apply[pred])
).asInstanceOf[P[n]]
given liftCoUpperbounded[U,A <: U,B <: U,S[_ <: U]](using ev: A =:= B):
(S[A] =:= S[B]) = ev.liftCo[[X] =>> Any].asInstanceOf[S[A] =:= S[B]]
type NatPlusZeroEqualsNat[n <: Nat] = (n plus O) =:= n
def trivialLemma[i <: Nat]: ((S[i] plus O) =:= S[i plus O]) =
summon[(S[i] plus O) =:= S[i plus O]]
object Proof extends NatInductionPrinciple[NatPlusZeroEqualsNat]:
val base = summon[(O plus O) =:= O]
val step: ([i <: Nat] => NatPlusZeroEqualsNat[i] => NatPlusZeroEqualsNat[S[i]]) =
[i <: Nat] => (p: NatPlusZeroEqualsNat[i]) =>
given previousStep: ((i plus O) =:= i) = p
given liftPreviousStep: (S[i plus O] =:= S[i]) =
liftCoUpperbounded[Nat,i plus O,i,S]
given definitionalEquality: ((S[i] plus O) =:= S[i plus O]) =
trivialLemma[i]
definitionalEquality.andThen(liftPreviousStep)
def demoNat(): Unit = {
println("Running demoNat...")
type two = S[S[O]]
val ev = Proof[two]
val twoInstance: two = new S[S[O]]
println(ev(twoInstance) == twoInstance)
}
它编译、运行和打印:
true
表示我们已经成功调用了递归定义的
two plus O =:= two
类型的可执行证据项的方法。
一些进一步的评论
-
trivialLemma
是必要的,以便其他summon
中的given
不会意外生成递归循环,这有点烦人。 - 需要用于
liftCo
的单独的S[_ <: U]
方法,因为=:=.liftCo
不允许具有上限类型参数的类型构造函数。 -
compiletime.erasedValue
+inline match
很棒!它会自动生成某种运行时小工具,允许我们对“已擦除”类型进行模式匹配。在我发现这一点之前,我试图手动构建适当的见证条款,但这似乎根本没有必要,它是免费提供的(请参阅手动构建见证条款的方法的编辑历史记录)。