От зависимых типов к гомотопической теории типов на Scala + Shapeless + ProvingGround

Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround, написанной на Скале с использованием Shapeless. У библиотеки имеется документация, правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT), (полу-) автоматически доказывать теоремы.

Началось все с того, что мне захотелось записать вводный курс по зависимым типам на Скале для конкурса Степика. Не хотелось повторяться, на Идрисе недавно появился хороший курс. Скала была выбрана как один из самых популярных функциональных языков. Погуглил по гитхабу по словам «Скала», «зависимые типы», «HoTT» и наиболее многообещающе выглядела ProvingGround. Сразу дисклеймер — я не утверждаю, что те или иные языки или библиотеки наиболее подходят для программирования с зависимыми типами, автоматического доказательства теорем, работы с HoTT. Можно было взять другие языки или библиотеки — был бы другой курс.

Как известно, Скала — язык с ограниченной поддержкой зависимых типов. Зависимые типы имплементируются в ней (другая точка зрения — эмулируются) с помощью path-dependent типов, type-level значений и имплицитов. Объяснять зависимые типы на голой Скале или Скале плюс Shapeless и погрязнуть в технических деталях типа отличия type members от type parameters (дженериков), имплицитов, path-dependent типов, «Aux» паттерна, type-level вычислений и т.д. не очень хотелось. Поэтому часть курса была на голой Скале, но бОльшая часть практики — на ProvingGround.

Термы и типы


Для задания переменных, термов, типов, функций и т.д. ProvingGround предоставляет свой DSL.
Так можно объявить тип A и переменную a этого типа:

val A = "A" :: Type
val a = "a" :: A

т.е. типичное объявление выглядит как

val идентификатор_переменной = "как печатать переменную" :: Тип_переменной

Напечатать терм «красиво» можно с помощью метода .fansi, вывести его тип — с помощью .typ:

println(a)
> a : (A : U_0)
println(a.fansi)
> a
println(a.typ)
> A : U_0
println(a.typ.fansi)
> A

Можно задать переменную детальнее:

val a : Term = "a" :: A

Здесь A — это тип в библиотеке ProvingGround, т.е. HoTT-тип, а Term — это тип в Скале.

Итак, если мы задаем переменную, то пишем тип после ::, а если у нас уже есть терм, то проверить его тип можно с помощью !:

a !: A

То, что эта строчка компилируется, означает, что тип указан правильно.

Зависимые типы


Небольшое напоминание о типах. Есть значения и есть типы. У каждого значения есть его тип. Зависимый тип — это тип, зависящий от значения (другого типа). Например, список двух строк и список трех строк — это значения одного и того же типа — список строк. Но если вынести информацию о числе элементов на уровень типа, то получим зависимый тип — вектор (он зависит от значения — натурального числа). И вектор двух строк и вектор трех строк — разные типы. Еще примеры зависимых типов — ненулевое число, непустой список, пара чисел, где второе число меньше первого, тип-равенство 1 =:= 2 (у которого нет значений), типы 1 =:= 1, 2 =:= 2 (у которых по одному значению) и т.д.

Так можно задать зависимый тип Ba, который зависит от значений типа A, и переменную этого типа:

val Ba = "B(_ : A)" :: A ->: Type
val b = "b" :: Ba(a)

Функции


Теперь про стрелочки. Есть 4 основных типа стрелок для функций: :->, :~>, ->:, ~>: . С двоеточиями слева — для лямбд (т.е. самих функций), с двоеточиями справа — для типов функций. С дефисами — для обычных функций, с тильдами — для зависимых функций (т.е. у которых не только значение, но и тип значения зависит от аргумента). В качестве примера — тождественная функция

val id = A :~> (a :-> a) !: A ~>: (A ->: A)

Часть проверки типов осуществляется в рантайме, но часть информации о типах видит и компилятор Скалы:

val f : FuncLike[Term, Term] = a :~> b !: a ~>: Ba(a)
val f : Term => Term = a :~> b !: a ~>: Ba(a)

Здесь зависимый функциональный тип из ProvingGround/HoTT компилятор Скалы видит как обычную функцию в Скале.

Индуктивные типы


Можно задавать индуктивные типы. Например, булев тип с конструкторами «истина» и «ложь»:

val Bool = "Boolean" :: Type
val BoolInd = ("true" ::: Bool) |: ("false" ::: Bool) =: Bool
val tru :: fls :: HNil = BoolInd.intros

то есть типичное задание индуктивного типа выглядит как

val идентификатор_объявления = (...) |: (...) |: (...) =: Имя_типа

где конструкторы значений этого типа отделены |: .

Еще пример — тип натуральных чисел с конструкторами «ноль» и «следующее число за натуральным n»:

val Nat = "Nat" :: Type
val NatInd = ("0" ::: Nat) |: ("succ" ::: Nat -->>: Nat) =: Nat
val zero :: succ :: HNil = NatInd.intros
val one = succ(zero) !: Nat
val two = succ(one) !: Nat
// ...

Тип целых чисел с конструкторами «плюс натуральное n» и «минус натуральное n минус 1» использует уже определенный тип натуральных чисел:

val Int = "Integer" :: Type
val IntInd = ("pos" ::: Nat ->>: Int) |: ("neg" ::: Nat ->>: Int) =: Int
val pos :: neg :: HNil = IntInd.intros

Тип списка значений типа A имеет конструкторы «пустой список» и «список с головой типа A и хвостом типа ListA»:

val ListA = "List(A)" :: Type
val ListAInd = ("nil" ::: ListA) |: ("cons" ::: A ->>: ListA -->>: ListA) =: ListA
val nil :: cons :: HNil = ListAInd.intros

У типа бинарного дерева (для простоты без значений некоторого типа в узлах) есть конструкторы «лист» и «вилка» (второй принимает пару поддеревьев):

val BTree = "BTree" :: Type
val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: BTree -->>: BTree -->>: BTree) =: BTree
val leaf :: fork :: HNil = BTreeInd.intros

Альтернативно конструктор «вилка» могла бы принимать функцию, которая переводит ложь в одно поддерево, истину в другое:

val BTree = "BTree" :: Type
val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: (Bool -|>: BTree) -->>: BTree) =: BTree
val leaf :: fork :: HNil = BTreeInd.intros

Зависимые индуктивные типы


Если тип зависимый (indexed inductive type), например вектор Vec или тип-равенство Id, то надо использовать =:: вместо =:, стрелку с тильдой и ссылаться на тип внутри конструкторов (Имя_типа -> Имя_типа(n)) в возвращаемом типе, (Имя_типа :> Имя_типа(n)) в принимаемом типе, а не просто Имя_типа(n). Например, тип вектора длины n:

val VecA = "Vec(A)" :: Nat ->: Type
val n = "n" :: Nat
val VecAInd = ("nil" ::: (VecA -> VecA(zero) )) |: 
    {"cons" ::: n ~>>: (A ->>: (VecA :> VecA(n) ) -->>: (VecA -> VecA(succ(n)) ))} =:: VecA
val vnil :: vcons :: HNil = VecAInd.intros

Еще один полезный зависимый тип позволяет формализовать понятие натурального числа, не превышающего другое натуральное число:

val Fin = "Fin" :: Nat ->: Type
val FinInd = {"FZ" ::: n ~>>: (Fin -> Fin(succ(n)) )} |: 
    {"FS" ::: n ~>>: ((Fin :> Fin(n) ) -->>: (Fin -> Fin(succ(n)) ))} =:: Fin
val fz :: fs :: HNil = FinInd.intros

Действительно, нет способа сконструировать значение типа Fin(zero). Есть ровно одно значение типа Fin(one):

val fz0 = fz(zero) !: Fin(one)

Есть ровно два значения типа Fin(two):

val fz1 = fz(one) !: Fin(two)
val fs1 = fs(one)(fz0) !: Fin(two)

Есть ровно три значения типа Fin(three):

fz(two) !: Fin(three)
fs(two)(fz1) !: Fin(three)
fs(two)(fs1) !: Fin(three)

и т.д.

Семейства индуктивных типов


Несколько слов об отличии семейства индуктивных типов (family of inductive types) от индексированного индуктивного типа (indexed inductive type). Например, List(A) — это семейство, а Vec(A)(n) — это семейство относительно типа A, но индексированный тип относительно натурального индекса n. Индуктивный тип — это тип, конструкторы которого для «следующих» значений могут использовать «предыдущие» значения (как у типов Nat, List и т.д.). Vec(A)(n) при фиксированном A является индуктивным типом, но не является при фиксированном n. В ProvingGround в настоящее время нет семейств индуктивных типов, т.е. нельзя, имея индуктивное определение, например, типа List(A), легко получить индуктивное определение типов List(B), List(Nat), List(Bool), List(List(A)) и т.д. Но можно эмулировать семейства с помощью индексированных типов:

val List = "List" :: Type ->: Type
val ListInd = {"nil" ::: A ~>>: (List -> List(A) )} |: 
    {"cons" ::: A ~>>: (A ->>: (List :> List(A) ) -->>: (List -> List(A) ))} =:: List
val nil :: cons :: HNil = ListInd.intros
cons(Nat)(zero)(cons(Nat)(one)(cons(Nat)(two)(nil(Nat)))) !: List(Nat)  // список 0, 1, 2

и

val Vec = "Vec" :: Type ->: Nat ->: Type
val VecInd = {"nil" ::: A ~>>: (Vec -> Vec(A)(zero) )} |: 
    {"cons" ::: A ~>>: n ~>>: (A ->>: (Vec :> Vec(A)(n) ) -->>: (Vec -> Vec(A)(succ(n)) ))} =:: Vec
val vnil :: vcons :: HNil = VecInd.intros
vcons(Bool)(two)(tru)(vcons(Bool)(one)(fls)(vcons(Bool)(zero)(tru)(vnil(Bool)))) !: Vec(Bool)(succ(two))  
// 3-элементный вектор tru, fls, tru

Можно также определить гетерогенный список (HList):

val HLst = "HList" :: Type ->: Type
val HLstInd = {"nil" ::: A ~>>: (HLst -> HLst(A) )} |: 
    {"cons" ::: A ~>>: (A ->>: (B ~>>: ((HLst :> HLst(B) ) -->>: (HLst -> HLst(A) ))))} =:: HLst
val hnil :: hcons :: HNil = HLstInd.intros

Мы сейчас реализовали собственный HList в библиотеке ProvingGround, которая написана поверх Shapeless, в которой основным строительным элементом является HList.

Алгебраические типы данных


В библиотеке можно эмулировать обобщенные алгебраические типы данных (GADT). Код, который выглядит на Хаскеле

{-# Language GADTs #-}
data Expr a where
    ELit     :: a         -> Expr a
    ESucc    :: Expr Int  -> Expr Int
    EIsZero  :: Expr Int  -> Expr Bool
    EIf      :: Expr Bool -> Expr a    -> Expr a    -> Expr a

и на чистой Скале

sealed trait Expr[A]
case class ELit[A](lit: A) extends Expr[A]
case class ESucc(num: Expr[Int]) extends Expr[Int]
case class EIsZero(num: Expr[Int]) extends Expr[Boolean]
case class EIf[A](cond: Expr[Boolean], thenExpr: Expr[A], elseExpr: Expr[A]) extends Expr[A]

запишется в ProvingGround как

val Expr = "Expr" :: Type ->: Type
val ExprInd = {"ELit" ::: A ~>>: (A ->>: (Expr -> Expr(A) ))} |:
  {"ESucc" ::: Expr(Nat) ->>: (Expr -> Expr(Nat) )} |:
  {"EIsZero" ::: Expr(Nat) ->>: (Expr -> Expr(Bool) )} |:
  {"EIf" ::: A ~>>: (Expr(Bool) ->>: Expr(A) ->>: Expr(A) ->>: (Expr -> Expr(A) ))} =:: Expr
val eLit :: eSucc :: eIsZero :: eIf :: HNil = ExprInd.intros

Классы типов


Также можно в библиотеке эмулировать классы типов. Например, функтор:

val A = "A" :: Type
val B = "B" :: Type
val C = "C" :: Type
val Functor = "Functor" :: (Type ->: Type) ->: Type
val F = "F(_ : U_0)" :: Type ->: Type
val Fmap = A ~>: (B ~>: ((A ->: B) ->: (F(A) ->: F(B) )))
val FunctorInd = {"functor" ::: F ~>>: (Fmap ->>: (Functor -> Functor(F) ))} =:: Functor
val functor :: HNil = FunctorInd.intros

Можно, например, список объявить экземпляром (instance) функтора:

val as = "as" :: List(A)
val indList_map = ListInd.induc(A :~> (as :-> (B ~>: ((A ->: B) ->: List(B) )))) // это индукция, о рекурсии и индукции идет речь ниже
val mapas = "map(as)" :: B ~>: ((A ->: B) ->: List(B))
val f = "f" :: A ->: B
val map = indList_map(A :~> (B :~> (f :->
       nil(B)
   )))(A :~> (a :-> (as :-> (mapas :-> (B :~> (f :->
       cons(B)(f(a))(mapas(B)(f))
   ))))))  !: A ~>: (List(A) ->: (B ~>: ((A ->: B) ->: List(B) )))
val listFunctor = functor(List)(A :~> (B :~> (f :-> (as :-> map(A)(as)(B)(f) )))) !: Functor(List)

Можно в класс типов добавить законы:

val fmap = "fmap" :: A ~>: (B ~>: ((A ->: B) ->: (F(A) ->: F(B) )))
val Fmap_id = A ~>: ( fmap(A)(A)(id(A)) =:= id(F(A)) )
val f = "f" :: A ->: B
val g = "g" :: B ->: C
val compose = A :~> (B :~> (C :~> (f :-> (g :-> (a :-> g(f(a)) 
    ))))) !: A ~>: (B ~>: (C ~>: ((A ->: B) ->: ((B ->: C) ->: (A ->: C)))))
val Fmap_compose = A ~>: (B ~>: (C ~>: (f ~>: (g ~>: ( 
    fmap(A)(C)(compose(A)(B)(C)(f)(g)) =:= compose(F(A))(F(B))(F(C))(fmap(A)(B)(f))(fmap(B)(C)(g)) )))))
val FunctorInd = {"functor" ::: F ~>>: (fmap ~>>: (Fmap_id ->>: (Fmap_compose ->>: (Functor -> Functor(F) ))))} =:: Functor
val functor :: HNil = FunctorInd.intros

Типы-равенства


В библиотеке уже есть встроенные сигма-тип (тип зависимой пары), пи-тип (тип зависимой функции, мы его уже видели выше), тип-равенство (identity type):

mkPair(a, b) !: Sgma(a !: A, Ba(a))
one.refl !: (one =:= one)
one.refl !: IdentityTyp(Nat, one, one)
two.refl !: (two =:= two)
(one =:= two) !: Type

но можно определить и свой, например, тип-равенство:

val Id = "Id" :: A ~>: (A ->: A ->: Type)
val IdInd = ("refl" ::: A ~>>: a ~>>: (Id -> Id(A)(a)(a) )) =:: Id
val refl :: HNil = IdInd.intros
refl(Nat)(two) !: Id(Nat)(two)(two)

Типы-равенства естественно возникают, когда начинается разговор о соответствии Карри-Ховарда. С одной стороны A ->: B — это функции из A в B, с другой — это логическая формула «из утверждения A следует B». И, с одной стороны, (A ->: B) ->: A ->: B — это тип функции высшего порядка, которая принимает на вход функцию A ->: B и значение типа A и возвращает эту функцию, примененную к этому значению, т.е. значение типа B. С другой стороны, это правило вывода в логике modus ponens — «если верно, что из A следует B, и верно A, то верно B». С такой точки зрения типы — это утверждения, а значения типов — это доказательства этих утверждений. И утверждение верно, если соответствующий тип населен, т.е. существует значение этого типа. Логическое «и» соответствует произведению типов, логическое «или» — сумме типов, логическое «не» — типу A ->: Zero, т.е. функциям в пустой тип. Так в теории типов возникает логика. Правда, не любая логика, а так называемая интуиционистская или конструктивная, т.е. логика без закона исключения третьего. Действительно, вообще говоря, нельзя сконструировать значение типа PlusTyp(A, A ->: Zero) (если не удалось доказать A, то это еще не значит, что удалось доказать не-A). Интересно, что справедливо отрицание к отрицанию закона исключения третьего:

val g = "g" :: PlusTyp(A, A ->: Zero) ->: Zero
val g1 = a :-> g(PlusTyp(A, A ->: Zero).incl1(a)) !: A ->: Zero
g :-> g(PlusTyp(A, A ->: Zero).incl2(g1)) !: (PlusTyp(A, A ->: Zero) ->: Zero) ->: Zero

Ну так вот, если типы — утверждения, а значения типов — доказательства, то раз равенство двух термов a1 =:= a2 — это утверждение, значит и тип. Тип зависимый, т.к. зависит от значений a1, a2 некоторого типа A. Если a1, a2 разные, то не должно быть способа сконструировать значение этого типа, т.к. утверждение ложно. Если одинаковые, то наоборот должен быть способ сконструировать значение, раз утверждение верно, так что у нашего индуктивного типа единственный конструктор refl(A)(a) !: Id(A)(a)(a) (или a.refl !: (a =:= a) для встроенного типа-равенства).

Еще один полезный тип при доказательстве теорем с неравенствами:

val LTE = "≤" :: Nat ->: Nat ->: Type
val LTEInd = {"0 ≤ _" ::: m ~>>: (LTE -> LTE(zero)(m) )} |: 
    {"S _ ≤ S _" ::: n ~>>: m ~>>: ((LTE :> LTE(n)(m) ) -->>: (LTE -> LTE(succ(n))(succ(m)) ))} =:: LTE
val lteZero :: lteSucc :: HNil = LTEInd.intros

Высшие индуктивные типы


Еще в библиотеке можно работать с высшими индуктивными типами. Например, окружностью

val Circle = "S^1" :: Type
val base = "base" :: Circle // конструктор
val loop = "loop" :: (base =:= base) // еще один конструктор

и сферой

val Sphere = "S^2" :: Type
val base = "base" :: Sphere // конструктор
val surf = "surf" :: (base.refl =:= base.refl) // еще один конструктор
//  val surf = "surf" :: IdentityTyp(base =:= base, base.refl, base.refl)
//  val surf = "surf" :: IdentityTyp(IdentityTyp(Sphere, base, base), base.refl, base.refl)

Рекурсия и индукция


Теперь о том, как определять (рекурсивные) функции. Библиотека для каждого индуктивного типа генерирует методы .rec, .induc, т.е. рекурсию (aka рекурсор) и индукцию — элиминаторы в постоянный и зависимый тип соответственно, с помощью которых можно осуществлять сопоставление с образцом (pattern matching), если надо — рекурсивное. Например, можно определить логическое «не»:

val b = "b" :: Bool
val recBB = BoolInd.rec(Bool)
val not = recBB(fls)(tru)

Здесь можно считать, что мы сделали сопоставление с образцом:

match {
  case true => false
  case false => true
}

Проверяем, что всё работает:

not(tru) == fls
not(fls) == tru

Также можно определить логическое «и»:

val recBBB = BoolInd.rec(Bool ->: Bool)
val and = recBBB(b :-> b)(b :-> fls)

Здесь можно считать, что мы сделали сопоставление с образцом по первому аргументу:

// псевдокод
match {
  case true => (b => b)
  case false => (b => false)
}

Проверяем:

and(fls)(tru) == fls
and(tru)(tru) == tru

Можно определить удваивание натурального числа:

val n = "n" :: Nat
val m = "m" :: Nat
val recNN = NatInd.rec(Nat)
val double = recNN(zero)(n :-> (m :-> succ(succ(m)) ))

Здесь опять можно считать, что мы сделали сопоставление с образцом:

// псевдокод
match {
  case Zero => Zero
  case Succ(n) =>
    val m = double(n)
    m + 2
}

Проверяем:

println(double(two).fansi)
> succ(succ(succ(succ(0))))

Определим сложение натуральных чисел:

val recNNN = NatInd.rec(Nat ->: Nat)
val addn = "add(n)" :: Nat ->: Nat
val add = recNNN(m :-> m)(n :-> (addn :-> (m :-> succ(addn(m)) )))

Здесь аналогично можно считать, что мы сделали сопоставление с образцом по первому аргументу:

// псевдокод
match {
  case Zero => (m => m)
  case Succ(n) =>
    val addn = add(n)
    m => addn(m) + 1
}

Проверка:

println(add(two)(three).fansi)
> succ(succ(succ(succ(succ(0)))))

Определим также конкатенацию векторов:

val vn = "v_n" :: VecA(n)
val vm = "v_m" :: VecA(m)
val indVVV = VecAInd.induc(n :~> (vn :-> (m ~>: (VecA(m) ->: VecA(add(n)(m)) ))))
val concatVn = "concat(v_n)" :: (m ~>: (VecA(m) ->: VecA(add(n)(m)) ))
val vconcat = indVVV(m :~> (vm :-> vm))(n :~> (a :-> (vn :-> (concatVn :-> (m :~> (vm :-> 
    vcons(add(n)(m))(a)(concatVn(m)(vm)) ))))))

Здесь мы используем не рекурсию, а индукцию, т.к. нам нужен элиминатор в зависимый тип
m ~>: (VecA(m) ->: VecA(add(n)(m))) — действительно, этот тип зависит от n из вектора (первый аргумент конкатенации), который мы деконструируем при сопоставлении с образцом:

// псевдокод
match {
  case (Zero, Nil) => (vm => vm)
  case (Succ(n), Cons(a)(vn)) =>
    val concatVn = concat(vn)
    vm => Cons(a)(concatVn(vm))
}

Тестируем:

val a = "a" :: A
val a1 = "a1" :: A
val a2 = "a2" :: A
val a3 = "a3" :: A
val a4 = "a4" :: A
val vect = vcons(one)(a)(vcons(zero)(a1)(vnil))
val vect1 = vcons(two)(a2)(vcons(one)(a3)(vcons(zero)(a4)(vnil)))
println(vconcat(two)(vect)(three)(vect1).fansi)
> cons(succ(succ(succ(succ(0)))))(a)(cons(succ(succ(succ(0))))(a1)(cons(succ(succ(0)))(a2)(cons(succ(0))(a3)(cons(0)(a4)(nil)))))

Покажу еще пример, как теоремы доказываются в ProvingGround. Докажем, что add(n)(n) =:= double(n).

val indN_naddSm_eq_S_naddm = NatInd.induc(n :-> (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )))
val hyp1 = "n+Sm=S(n+m)" :: (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) ))
val lemma = indN_naddSm_eq_S_naddm(m :~> succ(m).refl)(n :~> (hyp1 :-> (m :~>
    IdentityTyp.extnslty(succ)( add(n)(succ(m)) )( succ(add(n)(m)) )( hyp1(m) )
  )))  !: n ~>: m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )
val lemma1 = IdentityTyp.extnslty(succ)( add(n)(succ(n)) )( succ(add(n)(n)) )( lemma(n)(n) )
val indN_naddn_eq_2n = NatInd.induc(n :-> ( add(n)(n) =:= double(n) ))
val hyp = "n+n=2*n" :: ( add(n)(n) =:= double(n) )
val lemma2 = IdentityTyp.extnslty( m :-> succ(succ(m)) )( add(n)(n) )( double(n) )(hyp)
indN_naddn_eq_2n(zero.refl)(n :~> (hyp :->
    IdentityTyp.trans(Nat)( add(succ(n))(succ(n)) )( succ(succ(add(n)(n))) )( double(succ(n)) )(lemma1)(lemma2)
  ))  !: n ~>: ( add(n)(n) =:= double(n) )

Окружность не получается определить как обычный индуктивный тип через (...) |: (...) =:: ... (действительно, конструктор loop возвращает не значение типа Circle, как было бы для обычного индуктивного типа). Поэтому и рекурсию с индукцией приходится определять вручную:

val recCirc = "rec_{S^1}" :: A ~>: a ~>: (a =:= a) ->: Circle ->: A
val B = "B(_ : S^1)" :: Circle ->: Type
val b = "b" :: B(base)
val c = "c" :: Circle
val indCirc = "ind_{S^1}" :: B ~>: b ~>: (( IdentityTyp.transport(B)(base)(base)(loop)(b) =:= b ) ->: c ~>: B(c) )

с двумя аксиомами comp_base и comp_loop:

val l = "l" :: ( IdentityTyp.transport(B)(base)(base)(loop)(b) =:= b )
val comp_base = "comp_base" :: B ~>: b ~>: l ~>: ( indCirc(B)(b)(l)(base) =:= b )
val P = "P(_ : A)" :: A ->: Type
val f = "f" :: a ~>: P(a)
val dep_map = "dep_map" :: A ~>: (P ~>: (f ~>: (a ~>: (a1 ~>: (( a =:= a1 ) ->: ( f(a) =:= f(a1) )))))) // dep_map аналогично IdentityTyp.extnslty(f), но для зависимой f
val comp_loop = "comp_loop" :: B ~>: b ~>: l ~>: ( dep_map(Circle)(B)(indCirc(B)(b)(l))(base)(base)(loop) =:= l )


Несколько слов о том, как запускать код на ProvingGround. Есть 3 способа.

  1. Первый и рекомендуемый — из консоли (загружается Ammonite REPL) с помощью команды
    sbt mantle/test:run (из корня проекта ProvingGround после клонирования репозитория github.com/siddhartha-gadgil/ProvingGround.git, в случае ошибки запуска Ammonite REPL создать пустую директорию ProvingGround/mantle/target/web/classes/test).

  2. Второй — с помощью команды sbt server/run и затем открыть в браузере http://localhost:8080.

  3. Третий — из IDE. В IntelliJ Idea 2017.1.3 проект может импортироваться после модификации build.sbt, но код может не запускаться. Решение — импортировать в Идею не весь проект, а только подпроект ProvingGround/core. Для этого нужно положить новый build.sbt сюда: ProvingGround/core/build.sbt .

    Список импортов:

    import provingground._
    import HoTT._
    import TLImplicits._
    import shapeless._
    //import ammonite.ops._
    import FansiShow._

Если кому интересна эта тема (теория типов, гомотопическая теория типов, зависимые типы, вычисления на уровне типов, автоматическое доказательство теорем), добро пожаловать на мой курс. Он вводный. По HoTT скорее даже не введение, а введение во введение, но по остальным направлениям, думаю, дотягивает до уровня просто введения. Спасибо за внимание.
Поделиться публикацией
AdBlock похитил этот баннер, но баннеры не зубы — отрастут

Подробнее
Реклама

Комментарии 15

    +2
    val indN_naddSm_eq_S_naddm = NatInd.induc(n :-> (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )))
    val hyp1 = "n+Sm=S(n+m)" :: (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) ))
    val lemma = indN_naddSm_eq_S_naddm(m :~> succ(m).refl)(n :~> (hyp1 :-> (m :~>
        IdentityTyp.extnslty(succ)( add(n)(succ(m)) )( succ(add(n)(m)) )( hyp1(m) )
      )))  !: n ~>: m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )
    val lemma1 = IdentityTyp.extnslty(succ)( add(n)(succ(n)) )( succ(add(n)(n)) )( lemma(n)(n) )
    val indN_naddn_eq_2n = NatInd.induc(n :-> ( add(n)(n) =:= double(n) ))
    val hyp = "n+n=2*n" :: ( add(n)(n) =:= double(n) )
    val lemma2 = IdentityTyp.extnslty( m :-> succ(succ(m)) )( add(n)(n) )( double(n) )(hyp)
    indN_naddn_eq_2n(zero.refl)(n :~> (hyp :->
        IdentityTyp.trans(Nat)( add(succ(n))(succ(n)) )( succ(succ(add(n)(n))) )( double(succ(n)) )(lemma1)(lemma2)
      ))  !: n ~>: ( add(n)(n) =:= double(n) )
    


    жесть.
      0

      Если доказательство n+n = 2*n — это жесть, то что же тогда доказательство реально сложных выкладок?

        0
        Для «реально сложных выкладок» есть более подходящие инструменты.
          0

          Приведите пример, пожалуйста :)

            0
            Coq, Isabelle/HOL, тысячи их.
              0
              Lean еще можно назвать.
          +1
          Я даже не могу понять где тут доказательство для базы, где для шага индукции. Тот же Isabelle/HOL выглядит гораздо понятнее. Интересно, если
          Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор.
          то по идее в ProvingGround должны быть какие-то очень мощные эвристики. Человек в статье пишет какое-нибудь равенство и затем пишет «это может быть легко доказано по индукции». А ProvingGround автоматически это доказывает и человеку не нужно писать эту жесть?

          Например, в Isabelle/HOL есть «кувалда», а в ProvingGround есть что-то подобное? И ещё HoTT как-то упрощает формулировку и доказательство теорем по сравнению с другими подходами? Тут пишут, что да:
          HoTT allows mathematical proofs to be translated into a computer programming language for computer proof assistants much more easily than before. This approach offers the potential for computers to check difficult proofs.
          Было бы очень интересно увидеть пример упрощения…
            +2
            Я даже не могу понять где тут доказательство для базы, где для шага индукции.

            Здесь фактически доказательства двух утверждений: первое —
            n ~>: m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )
            
            второе —
            n ~>: ( add(n)(n) =:= double(n) )
            

            Для доказательства второго мне было нужно первое и пришлось его доказать тоже. В Идрисе первое — это стандартное plusSuccRightSucc.
            У первого база —
            m :~> succ(m).refl
            
            шаг —
            n :~> (hyp1 :-> (m :~> 
                IdentityTyp.extnslty(succ) ...
            
            т.е. аргументы, к которым применена индукция indN_naddSm_eq_S_naddm.
            У второго база —
            zero.refl
            
            шаг —
            n :~> (hyp :->
                IdentityTyp.trans(Nat) ...
            
            т.е. аргументы, к которым применена индукция indN_naddn_eq_2n.

            … то по идее в ProvingGround должны быть какие-то очень мощные эвристики.

            Мощных эвристик особо не заметил :) Сиддхартха как-то пробует применять методы machine learning.
            1 2 3 4

            И ещё HoTT как-то упрощает формулировку и доказательство теорем по сравнению с другими подходами?

            HoTT расширяет класс теорем (упрощает работу с ними). То есть не только теоремы типа (n+m)+k=n+(m+k), n+n=2*n, но и типа π1(S1)=Z, π2(S2)=Z, π3(S2)=Z.

            Тот же Isabelle/HOL выглядит гораздо понятнее.

            Следует отличать учебный инструмент от индустриального инструмента.
            В Идрисе, например, доказательство того, что если хвосты равны, то после приклеивания одинаковых голов списки опять равны, выглядит просто как
            same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
            same_cons Refl = Refl
            
            В ProvingGround — как
            val as = "as" :: ListA
            val as1 = "as1" :: ListA
            val as2 = "as2" :: ListA
            val pf = "as=as1" :: ( as =:= as1 )
            a :~> (as :~> (as1 :~> (pf :-> IdentityTyp.extnslty(as2 :-> cons(a)(as2))(as)(as1)(pf)
                  ))) !:  a ~>: as ~>: as1 ~>: (( as =:= as1 ) ->: ( cons(a)(as) =:= cons(a)(as1) ))
            
            которое можно записать короче:
            val as = "as" :: ListA
            val as1 = "as1" :: ListA
            a :~> (as :~> (as1 :~> IdentityTyp.extnslty(cons(a))(as)(as1)
                  )) !:  a ~>: as ~>: as1 ~>: (( as =:= as1 ) ->: ( cons(a)(as) =:= cons(a)(as1) ))
            

            В Идрисе доказательство того, то n+0=n — это
            plus_n_zero : (n : Nat) -> n + 0 = n
            plus_n_zero Z = Refl
            plus_n_zero (S n) = rewrite plus_n_zero n
                                  in Refl
            
            В ProvingGround —
            val indN_nadd0_eq_n = NatInd.induc(n :-> ( add(n)(zero) =:= n ))
            val hyp = "n+0=n" :: ( add(n)(zero) =:= n )
            indN_nadd0_eq_n(zero.refl)(n :~> (hyp :-> IdentityTyp.extnslty(succ)( add(n)(zero) )(n)(hyp)
                  )) !:  n ~>: ( add(n)(zero) =:= n )
            
            или короче
            val indN_nadd0_eq_n = NatInd.induc(n :-> ( add(n)(zero) =:= n ))
            indN_nadd0_eq_n(zero.refl)(n :~> IdentityTyp.extnslty(succ)( add(n)(zero) )(n)
                  ) !:  n ~>: ( add(n)(zero) =:= n )
            

            Первое написать проще (и при реальной работе удобнее), но второе имхо лучше для понимания что происходит (когда разбираешься, когда пишешь учебный курс). Иначе вся магия спрятана за строчкой типа функция от Refl равна Refl, за rewrite'ами и т.д.
              0
              Спасибо, стало немного понятней! Но синтаксис с обилием скобок, вложенных выражений, разнообразием операторов конечно пугает.

              В Isabelle/HOL лемма про одинаковые хвосты не требует доказательства. Как я понимаю, это автоматически выводится просто упрощением на символьном уровне.

              HoTT расширяет класс теорем (упрощает работу с ними). То есть не только теоремы типа (n+m)+k=n+(m+k), n+n=2*n, но и типа π1(S1)=Z, π2(S2)=Z, π2(S2)=Z.
              Тут пишут, что π1(S1) — это совокупность отображений окружностей в окружности. Например, одна окружность — это охват руки, вторая окружность — это резинка. Резинку можно просто одеть на запястье, можно обернуть 2 раза вокруг запястья, 3, 4,… и т.д. Короче, множество таких отображений изоморфно множеству целых чисел Z. Не понимаю, как это может использоваться в программировании или доказательстве теорем…

              Начал слушать курс лекций 15-819 Homotopy Type Theory. Там с самых основ рассказывается про теорию типов, немного логики, немного аналогий из теории категорий. Может кому-то пригодится.
                +1
                Не понимаю, как это может использоваться в программировании или доказательстве теорем…

                Я не говорил, что применяется при обычном программировании (при обычном применяются типы, иногда — зависимые типы, а не высшие типы, просто интересно, что это всё связано). Что касается применений при доказательстве теорем, так π1(S1)=Z — это и есть теорема. Соответственно, «это» применяется, например, при доказательстве этой теоремы. Просто в вики на пальцах с помощью аналогии объяснили, что утверждение «значит», и утверждение выглядит очевидным. Но так ли очевидно, например, что π2(S2)=Z или π7(S4)=ZxZ12? Уже для π3(S2)=Z возникает красивая конструкция, расслоение Хопфа называется. Если вопрос в том, для чего нужны гомотопические группы в математике, то они имеют отношение к задаче классификации многообразий (поверхностей). Есть два как-то заданных многообразия, как понять, это одно и то же или разные? Можно, например, посчитать какие-то инварианты для них (а гомотопические группы — топологические инварианты), и если они разные, значит многообразия разные.

                Начал слушать курс лекций...

                Еще есть такие видеолекции на русском:
                https://www.youtube.com/channel/UCKjg3udGxUrfI1T1pEiyQYg
                0
                Насчет ProvingGround, Idris, Isabelle/HOL и т.п. У меня есть одна практическая задача. Мы запилили транслятор с одного языка (спецификаций) на другой (исполняемый) язык. И теперь пытаемся доказать, что транслятор преобразует выражения корректно, что семантика выражений не изменяется при преобразовании. Пока пытаюсь использовать Isabelle/HOL, из всех инструментов он выглядит самым понятным. Но, блин, всё равно всё сложно, хочется найти какой-то волшебный инструмент, где бы всё само доказывалось.
                  +2
                  Coq и Lean не смотрели?
                  «Само» может только там, где уже куча всего доказано под капотом.
            0
            Ситуация с HoTT такая. На форуме по теории типов много лет были страдания «Почему программистам не интересно то, что мы выдумываем?» Тут пришёл Воеводский с новой идеей: на языке теории типов можно говорить о так называемых гомотопиях (все эти «тип-сфера» и «тип-отрезок» как раз об этом). А гомотопная математика — большая и влиятельная часть математики. В результате возник не совсем понятный мне энтузиазм «Нафиг программистов, давайте охмурять гомотопных математиков!» Все специалисты по теории типов ушли за Воеводским изучать гомотопии и там погибли, форум же практически загнулся
            http://lists.seas.upenn.edu/pipermail/types-list/2017/thread.html
            Хочу предупредить: программистам «тип-сфера», «тип-отрезок» и т.п. НЕ НУЖНЫ! Возможно, для гомотопной математики будет польза.
            0
            Новая версия курса: stepik.org/course/49181

            Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

            Самое читаемое