dmitrymitin22 мая 2017 в 09:11

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

14 мин

8.6K

Scala * Математика * Функциональное программирование *

Из песочницы

+17

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

raveclassic 22 мая 2017 в 10:18

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

жесть.

fly_style 22 мая 2017 в 15:58

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

ymn 22 мая 2017 в 18:18

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

fly_style 22 мая 2017 в 18:41

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

ymn 22 мая 2017 в 18:44

Coq, Isabelle/HOL, тысячи их.

dmitrymitin 23 мая 2017 в 09:00

Lean еще можно назвать.

Ares_ekb 22 мая 2017 в 16:41

Я даже не могу понять где тут доказательство для базы, где для шага индукции. Тот же 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.

Было бы очень интересно увидеть пример упрощения…

dmitrymitin 23 мая 2017 в 08:50

Я даже не могу понять где тут доказательство для базы, где для шага индукции.

Здесь фактически доказательства двух утверждений: первое —

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, но и типа π₁(S¹)=Z, π₂(S²)=Z, π₃(S²)=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'ами и т.д.

Ares_ekb 23 мая 2017 в 10:22

Спасибо, стало немного понятней! Но синтаксис с обилием скобок, вложенных выражений, разнообразием операторов конечно пугает.

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

HoTT расширяет класс теорем (упрощает работу с ними). То есть не только теоремы типа (n+m)+k=n+(m+k), n+n=2*n, но и типа π₁(S¹)=Z, π₂(S²)=Z, π₂(S²)=Z.

Тут пишут, что π₁(S¹) — это совокупность отображений окружностей в окружности. Например, одна окружность — это охват руки, вторая окружность — это резинка. Резинку можно просто одеть на запястье, можно обернуть 2 раза вокруг запястья, 3, 4,… и т.д. Короче, множество таких отображений изоморфно множеству целых чисел Z. Не понимаю, как это может использоваться в программировании или доказательстве теорем…

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

dmitrymitin 23 мая 2017 в 10:58

Не понимаю, как это может использоваться в программировании или доказательстве теорем…

Я не говорил, что применяется при обычном программировании (при обычном применяются типы, иногда — зависимые типы, а не высшие типы, просто интересно, что это всё связано). Что касается применений при доказательстве теорем, так π₁(S¹)=Z — это и есть теорема. Соответственно, «это» применяется, например, при доказательстве этой теоремы. Просто в вики на пальцах с помощью аналогии объяснили, что утверждение «значит», и утверждение выглядит очевидным. Но так ли очевидно, например, что π₂(S²)=Z или π₇(S⁴)=ZxZ₁₂? Уже для π₃(S²)=Z возникает красивая конструкция, расслоение Хопфа называется. Если вопрос в том, для чего нужны гомотопические группы в математике, то они имеют отношение к задаче классификации многообразий (поверхностей). Есть два как-то заданных многообразия, как понять, это одно и то же или разные? Можно, например, посчитать какие-то инварианты для них (а гомотопические группы — топологические инварианты), и если они разные, значит многообразия разные.

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

Еще есть такие видеолекции на русском:
https://www.youtube.com/channel/UCKjg3udGxUrfI1T1pEiyQYg

Ares_ekb 23 мая 2017 в 10:44

Насчет ProvingGround, Idris, Isabelle/HOL и т.п. У меня есть одна практическая задача. Мы запилили транслятор с одного языка (спецификаций) на другой (исполняемый) язык. И теперь пытаемся доказать, что транслятор преобразует выражения корректно, что семантика выражений не изменяется при преобразовании. Пока пытаюсь использовать Isabelle/HOL, из всех инструментов он выглядит самым понятным. Но, блин, всё равно всё сложно, хочется найти какой-то волшебный инструмент, где бы всё само доказывалось.

dmitrymitin 23 мая 2017 в 11:02

Coq и Lean не смотрели?
«Само» может только там, где уже куча всего доказано под капотом.

shuhray 22 мая 2017 в 23:08

Ситуация с HoTT такая. На форуме по теории типов много лет были страдания «Почему программистам не интересно то, что мы выдумываем?» Тут пришёл Воеводский с новой идеей: на языке теории типов можно говорить о так называемых гомотопиях (все эти «тип-сфера» и «тип-отрезок» как раз об этом). А гомотопная математика — большая и влиятельная часть математики. В результате возник не совсем понятный мне энтузиазм «Нафиг программистов, давайте охмурять гомотопных математиков!» Все специалисты по теории типов ушли за Воеводским изучать гомотопии и там погибли, форум же практически загнулся
http://lists.seas.upenn.edu/pipermail/types-list/2017/thread.html
Хочу предупредить: программистам «тип-сфера», «тип-отрезок» и т.п. НЕ НУЖНЫ! Возможно, для гомотопной математики будет польза.

dmitrymitin 23 мая 2017 в 09:18

Вроде на загибание не похоже :)
http://arxiv.org:443/find/all/1/AND+ti:+type+cat:+math.LO/0/1/0/all/0/1
http://arxiv.org:443/find/all/1/AND+ti:+type+cat:+cs.LO/0/1/0/all/0/1
Форумы:
https://groups.google.com/forum/#!forum/homotopytypetheory
https://groups.google.com/forum/#!forum/hott-cafe
https://nforum.ncatlab.org/

dmitrymitin 2 ноя 2018 в 14:39

Новая версия курса: stepik.org/course/49181

Зарегистрируйтесь на Хабре, чтобы оставить комментарий