Блог

Учитывая следующую функцию сложения на уровне типов для чисел Пеано

 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)) .

из книги Хотта (раздел 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 s внутри других given s случайно не создавали рекурсивные циклы, что немного раздражает.
• liftCo Отдельный метод для был необходим, потому что не допускает конструкторов типов с параметрами типа с верхними ограничениями. S[_ <: U] =:=.liftCo
• compiletime.erasedValue inline match это потрясающе! Он автоматически генерирует какие-то вещицы во время выполнения, которые позволяют нам сопоставлять шаблоны для «стертого» типа. До того, как я узнал об этом, я пытался создать соответствующие термины-свидетели вручную, но в этом нет необходимости, это предоставляется бесплатно (см. Историю редактирования для подхода с использованием терминов-свидетелей, созданных вручную).