Не понимаю, как это может использоваться в программировании или доказательстве теорем…
Я не говорил, что применяется при обычном программировании (при обычном применяются типы, иногда — зависимые типы, а не высшие типы, просто интересно, что это всё связано). Что касается применений при доказательстве теорем, так π1(S1)=Z — это и есть теорема. Соответственно, «это» применяется, например, при доказательстве этой теоремы. Просто в вики на пальцах с помощью аналогии объяснили, что утверждение «значит», и утверждение выглядит очевидным. Но так ли очевидно, например, что π2(S2)=Z или π7(S4)=ZxZ12? Уже для π3(S2)=Z возникает красивая конструкция, расслоение Хопфа называется. Если вопрос в том, для чего нужны гомотопические группы в математике, то они имеют отношение к задаче классификации многообразий (поверхностей). Есть два как-то заданных многообразия, как понять, это одно и то же или разные? Можно, например, посчитать какие-то инварианты для них (а гомотопические группы — топологические инварианты), и если они разные, значит многообразия разные.
Я даже не могу понять где тут доказательство для базы, где для шага индукции.
Здесь фактически доказательства двух утверждений: первое —
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. 1234
И ещё 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'ами и т.д.
Хм, все еще 404)
https://github.com/dzolotov/bytecode выдает 404
«Само» может только там, где уже куча всего доказано под капотом.
Я не говорил, что применяется при обычном программировании (при обычном применяются типы, иногда — зависимые типы, а не высшие типы, просто интересно, что это всё связано). Что касается применений при доказательстве теорем, так π1(S1)=Z — это и есть теорема. Соответственно, «это» применяется, например, при доказательстве этой теоремы. Просто в вики на пальцах с помощью аналогии объяснили, что утверждение «значит», и утверждение выглядит очевидным. Но так ли очевидно, например, что π2(S2)=Z или π7(S4)=ZxZ12? Уже для π3(S2)=Z возникает красивая конструкция, расслоение Хопфа называется. Если вопрос в том, для чего нужны гомотопические группы в математике, то они имеют отношение к задаче классификации многообразий (поверхностей). Есть два как-то заданных многообразия, как понять, это одно и то же или разные? Можно, например, посчитать какие-то инварианты для них (а гомотопические группы — топологические инварианты), и если они разные, значит многообразия разные.
Еще есть такие видеолекции на русском:
https://www.youtube.com/channel/UCKjg3udGxUrfI1T1pEiyQYg
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/
Здесь фактически доказательства двух утверждений: первое — второе —
Для доказательства второго мне было нужно первое и пришлось его доказать тоже. В Идрисе первое — это стандартное plusSuccRightSucc.
У первого база — шаг — т.е. аргументы, к которым применена индукция
indN_naddSm_eq_S_naddm.У второго база — шаг — т.е. аргументы, к которым применена индукция
indN_naddn_eq_2n.Мощных эвристик особо не заметил :) Сиддхартха как-то пробует применять методы machine learning.
1 2 3 4
HoTT расширяет класс теорем (упрощает работу с ними). То есть не только теоремы типа (n+m)+k=n+(m+k), n+n=2*n, но и типа π1(S1)=Z, π2(S2)=Z, π3(S2)=Z.
Следует отличать учебный инструмент от индустриального инструмента.
В Идрисе, например, доказательство того, что если хвосты равны, то после приклеивания одинаковых голов списки опять равны, выглядит просто как
В ProvingGround — как
которое можно записать короче:
В Идрисе доказательство того, то n+0=n — это
В ProvingGround —
или короче
Первое написать проще (и при реальной работе удобнее), но второе имхо лучше для понимания что происходит (когда разбираешься, когда пишешь учебный курс). Иначе вся магия спрятана за строчкой типа функция от
ReflравнаRefl, заrewrite'ами и т.д.