给定皮亚诺数的以下类型级加法函数
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)
and es:∏(n:N)E(n)→E(succ(n))
.
from HoTT 书(第 5.1 节) https://hott.github.io/book/nightly/hott-online-1287-g1ac9408.pdf.
以下是在下面的代码中实现的计划:
-
明确证明“某些财产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
这种归纳原理使用一些元编程工具。
-
写出归纳原理的基本情况和归纳情况的证明。
-
???
-
Profit
代码如下所示:
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
.
一些进一步的评论
- The
trivialLemma
是必要的,以便summon
s 在其他的里面given
不会意外地生成递归循环,这有点烦人。
- 分开的
liftCo
- 方法S[_ <: U]
需要,因为=:=.liftCo
不允许具有上限类型参数的类型构造函数。
-
compiletime.erasedValue
+ inline match
太棒了!它会自动生成某种运行时小发明,使我们能够对“已擦除”类型进行模式匹配。在我发现这一点之前,我试图手动构建适当的见证条款,但这似乎根本没有必要,它是免费提供的(有关手动构建见证条款的方法,请参阅编辑历史记录)。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)