给定以下 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]
说我们想证明定理for all natural numbers 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
的证明?
最佳答案
这是一种可能的方法,它是对这一段的字面解释的尝试:
When proving a statement
E:N→U
about all natural numbers, it suffices to prove it for0
and forsucc(n)
, assuming it holds forn
, i.e., we constructez:E(0)
andes:∏(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
-method 本质上说“对于所有 n <: N
,我们可以生成 P[n]
的证据”。请注意,该方法声明为
inline
.这是确保∀n.P(n)
证明的一种可能方式。在运行时具有 build 性和可执行性(但是,请参阅手动生成见证条款的替代提案的编辑历史记录)。 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
s 里面的其他 given
s 不小心生成递归循环,有点烦人。 liftCo
-方法为S[_ <: U]
需要,因为 =:=.liftCo
不允许具有上限类型参数的类型构造函数。 compiletime.erasedValue
+ inline match
太棒了!它会自动生成某种运行时小工具,允许我们对“已删除”类型进行模式匹配。在我发现这一点之前,我试图手动构建适当的见证条款,但这似乎根本没有必要,它是免费提供的(请参阅编辑历史以了解手动构建见证条款的方法)。 关于scala - 如何询问 Scala 是否存在所有类型参数实例化的证据?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/67093833/