diff --git a/docs/config/en/mkdocs.yml b/docs/config/en/mkdocs.yml index 74ef3a0e3..13e3e5379 100644 --- a/docs/config/en/mkdocs.yml +++ b/docs/config/en/mkdocs.yml @@ -14,6 +14,7 @@ nav: - Tools: tools.md - Contributors: CONTRIBUTORS.md - Changelog: CHANGELOG.md + - Other proof assistants: related.md - Getting Started: - getting-started/index.md - Install: getting-started/install.md diff --git a/docs/config/ru/mkdocs.yml b/docs/config/ru/mkdocs.yml index 92de3931e..a6304c282 100644 --- a/docs/config/ru/mkdocs.yml +++ b/docs/config/ru/mkdocs.yml @@ -14,6 +14,7 @@ nav: - Инструменты: tools.md - Участники (англ.): CONTRIBUTORS.md - История изменений (англ.): CHANGELOG.md + - Другие решатели: related.md - Первые шаги: - getting-started/index.md - Установка: getting-started/install.md diff --git a/docs/docs/en/index.md b/docs/docs/en/index.md index 89e52dd36..4f851a823 100644 --- a/docs/docs/en/index.md +++ b/docs/docs/en/index.md @@ -68,3 +68,8 @@ A Zulip chat is available for all to join and chat about Rzk, including formaliz [^5]: Nikolai Kudasov. Experimental prover for Tope logic. SCAN 2023, pages 37–39. 2023. + +## Other proof assistants for HoTT + +Rzk is not the first or the only proof assistant where it's possible to do (a variant of) homotopy type theory. +See a [brief comparison of Rzk with other proof assistants](related.md). diff --git a/docs/docs/en/related.md b/docs/docs/en/related.md new file mode 100644 index 000000000..8e01fb8aa --- /dev/null +++ b/docs/docs/en/related.md @@ -0,0 +1,123 @@ +# Other proof assistants for HoTT + +Rzk is not the first or the only proof assistant where it's possible to do (a variant of) homotopy type theory. +Here is an incomplete list of such proof assistants and corresponding formalization libraries. + +## Agda + +[Agda](https://agda.readthedocs.io/en/latest/) is a dependently typed programming language (and also a proof assistant). + +While by default Agda is not compatible with HoTT because of built-in Axiom K, +it supports [`--without-K` option](https://agda.readthedocs.io/en/v2.6.1/language/without-k.html#without-k), allowing to restore the compatibility with univalence. +Some notable HoTT libraries in Agda include [`agda-unimath`](https://unimath.github.io/agda-unimath/), +[`HoTT-Agda`](https://github.com/hott/hott-agda/). + +Rzk's syntax for expressions is partially inspired by Agda. +Rzk's (experimental) formatter is based on the code style accepted in [emilyriehl/yoneda](https://github.com/emilyriehl/yoneda) and [rzk-lang/sHoTT](https://github.com/rzk-lang/sHoTT) projects, +which comes largely from the [code style of `agda-unimath`](https://unimath.github.io/agda-unimath/CODINGSTYLE.html). + +Agda is implemented in Haskell. + +## Arend + +[Arend](https://arend-lang.github.io) is a theorem prover based on homotopy type theory with an interval type, +making it similar to cubical type theories. Arend features a standard library at [JetBrains/arend-lib](https://github.com/JetBrains/arend-lib). + +Arend is developed by JetBrains, and is implemented in Java. +It also features a [plugin for IntelliJ IDEA](https://arend-lang.github.io/about/intellij-features) turning it into an IDE for Arend. + +## Aya + +[Aya](https://www.aya-prover.org) is an experimental cubical proof assistant, +featuring type system features similar to Cubical Agda, redtt, and Arend. +It also features overlapping and order-independent pattern matching, as well as +some functional programming features similar to Haskell and Idris. + +Aya is implemented in Java. + +!!! question "Formalizations in Aya?" + + I do not know of existing formalization libraries in Aya. + +## The red* family + +[cooltt](https://github.com/redprl/cooltt), [redtt](https://github.com/redprl/redtt), and [RedPRL](https://redprl.readthedocs.io/en/latest/) are a family of experimental proof assistants developed by the [RedPRL Development Team](https://redprl.org). + +There is a [redtt mathematical library](https://github.com/RedPRL/redtt/tree/master/library) + +The red* family of proof assistants is implemented in OCaml. +The developers also have a related [A.L.G.A.E. project](https://redprl.org/#algae), +which aims to provide composable (OCaml) libraries that facilitate the construction of a usable proof assistant from a core type checker. + +## Coq + +Coq is a mature proof assistant, based on the Calculus of Inductive Constructions. +The original HoTT formalization, [UniMath](https://github.com/UniMath/UniMath), +initiated by Vladimir Voevodsky, is done in Coq and is maintained to this day by +[The UniMath Coordinating Committee](https://github.com/UniMath/UniMath#the-unimath-coordinating-committee). +Other notable formalizations of HoTT in Coq include [Coq-HoTT](https://github.com/HoTT/Coq-HoTT)[^3] + +Coq is implemented in OCaml. + +## Cubical Agda +[Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) is a mode extending Agda with a variety of features from Cubical Type Theory[^1] [^2]. + +Although technical a mode within Agda, it is probably best seen as a separate language. +Cubical Agda (as well as other cubical proof assistants) supports a variant of extension types found in Rzk, +albeit restricted to the use with cubical intervals. + +Some notable formalizations in Cubical Agda include [`cubical`](https://github.com/agda/cubical) and [1lab](https://1lab.dev). + +Cubical Agda as part of Agda is implemented in Haskell. + +## `cubicaltt` + +`cubicaltt` is an experimental cubical proof assistant[^1] and a precursor to Cubical Agda. + +Several formalizations in `cubicaltt` can be found at . + +`cubicaltt` is implemented in Haskell. + +## Lean + +[Lean](https://lean-lang.org) is a teorem prover and a dependently typed programming language, based on the Calculus of Inductive Constructions. +Similarly to Coq, Lean encourages heavy use of tactics and automation. + +Lean 2, similarly to Agda, supported a mode without uniqueness of identity proofs (UIP), +which allowed for HoTT formalizations. +Hence, a formalization of [HoTT in Lean 2](https://github.com/leanprover/lean2/tree/master/hott)[^4] exists. +However, since Lean 2 is not supported anymore, the formalization is also unmantained. + +Lean 3 and 4 has dropped the mode that allowed (direct) HoTT formalization. +There is, however, an unmaintained [port of Lean 2 HoTT Library to Lean 3](https://github.com/gebner/hott3). + +Lean 2 and 3 are implemented in C++. +Lean 4 is implemented in itself (and a bit of C++)! + +[^1]: + Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. + _Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom_. + In 21st International Conference on Types for Proofs and Programs (TYPES 2015). + Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018) + + +[^2]: + Thierry Coquand, Simon Huber, and Anders Mörtberg. + 2018. _On Higher Inductive Types in Cubical Type Theory_. + In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18). + Association for Computing Machinery, New York, NY, USA, 255–264. + + +[^3]: + Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. + 2017. _The HoTT library: a formalization of homotopy type theory in Coq_. + In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). + Association for Computing Machinery, New York, NY, USA, 164–172. + + +[^4]: + Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. + 2017. _Homotopy Type Theory in Lean_. + In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. + Lecture Notes in Computer Science(), vol 10499. Springer, Cham. + diff --git a/docs/docs/ru/index.md b/docs/docs/ru/index.md index 9bfca47e7..f294ea201 100644 --- a/docs/docs/ru/index.md +++ b/docs/docs/ru/index.md @@ -82,3 +82,8 @@ Rzk и сопутствующие инструменты разработаны Международный коллектив авторов. _Гомотопическая теория типов: унивалентные основания математики_. ИНСТИТУТ ПЕРСПЕКТИВНЫХ ИССЛЕДОВАНИЙ. Перевод и редактирование: ГЕННАДИЙ ЧЕРНЫШЕВ. + +## Другие решатели для гомотопической теории типов + +Rzk — не первый и не единственный решатель для (варианта) гомотопической теории типов. +См. [краткое сравнение Rzk с другими решателями](related.md). diff --git a/docs/docs/ru/related.md b/docs/docs/ru/related.md new file mode 100644 index 000000000..81dd4a28d --- /dev/null +++ b/docs/docs/ru/related.md @@ -0,0 +1,136 @@ +# Другие решатели + +Rzk — не первый и не единственный решатель для (варианта) гомотопической теории типов. +Ниже следует неполный список существующих решателей и библиотек формализаций на них. + +## Agda + +[Agda](https://agda.readthedocs.io/en/latest/) — это язык программирования с зависимыми типами, а также решатель теорем. + +Хотя по умолчанию Agda не совместима с гомотопической теории типов из-за встроенной аксиомы K, +решатель поддерживает [опцию `--without-K`](https://agda.readthedocs.io/en/v2.6.1/language/without-k.html#without-k), +позволяющей восстановить совместимость с унивалентностью. +Стоит отметить основные формализации гомотопической теории типов на Agde: +[`agda-unimath`](https://unimath.github.io/agda-unimath/) и +[`HoTT-Agda`](https://github.com/hott/hott-agda/). + +Синтаксис выражений в Rzk частично вдохновлён синтаксисом Agda. +Экспериментальная поддержка автоматического форматирования кода Rzk +основана на стиле принятом в проектах [emilyriehl/yoneda](https://github.com/emilyriehl/yoneda) и [rzk-lang/sHoTT](https://github.com/rzk-lang/sHoTT), +который в свою очередь вдохновлён [стилем `agda-unimath`](https://unimath.github.io/agda-unimath/CODINGSTYLE.html). + +Agda реализована на языке программирования Haskell. + +## Arend + +[Arend](https://arend-lang.github.io) — это решатель теорем для гомотопической теории типов со встроенным типом (ненаправленного) интервала, +что делает его схожим с кубическими системами типов. +Стандартная библиотека формализаций Arend находится в [JetBrains/arend-lib](https://github.com/JetBrains/arend-lib). + +Arend разрабатывается JetBrains и реализован на языке Java. +Также существует [плагин для IntelliJ IDEA](https://arend-lang.github.io/about/intellij-features), +превращающий её в полноценную среду разработки для Arend. + +## Aya + +[Aya](https://www.aya-prover.org) — экспериментальный кубический решатель теорем, +с системой типов, схожей с Cubical Agda, redtt, и Arend. +Также в Aya есть поддержка сопоставления с образцом, допускающая пересекающиеся и неупорядоченные образцы, +а также возможности для функционального программирования, аналогичные Haskell и Idris. + +Aya реализована на Java. + +!!! question "Формализации на Aya?" + + Мне неизвестны библиотеки формализации на Aya. + +## Семейство red* + +[cooltt](https://github.com/redprl/cooltt), +[redtt](https://github.com/redprl/redtt), +и [RedPRL](https://redprl.readthedocs.io/en/latest/) +представляют семейство экспериментальных решателей теорем, +разработанных [командой RedPRL](https://redprl.org). + +Существует формализация [математической библиотеки redtt](https://github.com/RedPRL/redtt/tree/master/library) + +Семейство решателей red* реализовано на языке программирования OCaml. +Создатели семества решателей также работают над [проектом A.L.G.A.E.](https://redprl.org/#algae), +который нацелен на реализацию ряда удобных библиотек (для OCaml) для помощи в реализации +решателей теорем на основе проверки типов для ядра решателя. + +## Coq + +Coq — это зрелый решатель теорем, основанный на исчислении индуктивных конструкций. +Первая формализация гомотопической теории типов и унивалентных оснований, [UniMath](https://github.com/UniMath/UniMath), +начатая Владимиром Воеводским, была создана с использованием Coq и до сих пор развивается и поддерживается +[координационным комитетом UniMath](https://github.com/UniMath/UniMath#the-unimath-coordinating-committee). +Ещё одна важная формализация гомотопической теории типов — это [Coq-HoTT](https://github.com/HoTT/Coq-HoTT)[^3]. + +Coq реализован на OCaml. + +## Cubical Agda +[Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) (кубическая Агда) +— это расширение Agda набором возможностей кубической теории типов[^1] [^2]. + +Хотя технически это расширение Agda, лучше рассматривать его как отдельный язык. +Кубическая Agda (как и другие кубические решатели) поддерживает вариацию типов-расширений (аналогично Rzk), +но только для кубических интервалов. + +Важными проектами формализации на кубической Agda являются библиотека [`cubical`](https://github.com/agda/cubical) +и проект [1lab](https://1lab.dev). + +Кубическая Agda является частью Agda и также реализована на Haskell. + +## `cubicaltt` + +`cubicaltt` — это экспериментальный кубический решатель[^1] и предшественник Cubical Agda. + +Некоторые формализации на `cubicaltt` находятся в . + +`cubicaltt` реализован на языке Haskell. + +## Lean + +[Lean](https://lean-lang.org) — это решатель теорем и язык программирования с зависимыми типами, +основанный на исчислении индуктивных конструкций. +Аналогично Coq, Lean способствует широкому использованию тактик и автоматизации. + +Lean 2, как и Agda, поддерживал режим без уникальности доказательств тождеств (Uniqueness of Identity Proofs, UIP), +который допускал совместимость с гомотопической теорией типов. +Поэтому, существует формализация [HoTT на Lean 2](https://github.com/leanprover/lean2/tree/master/hott)[^4]. +Однако, Lean 2 больше не поддерживается и формализация, соответственно, тоже. + +Lean 3 и 4 убрали режим, допускающий (прямую) формализацию гомотопической теории типов. +Однако, существует ныне неподдерживаемый [проект по переносу библиотеки HoTT с Lean 2 на Lean 3](https://github.com/gebner/hott3). + +Lean 2 и 3 реализованы на C++. +Lean 4 реализован в основном на самом себе (и немного на C++)! + +[^1]: + Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. + _Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom_. + In 21st International Conference on Types for Proofs and Programs (TYPES 2015). + Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018) + + +[^2]: + Thierry Coquand, Simon Huber, and Anders Mörtberg. + 2018. _On Higher Inductive Types in Cubical Type Theory_. + In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18). + Association for Computing Machinery, New York, NY, USA, 255–264. + + +[^3]: + Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. + 2017. _The HoTT library: a formalization of homotopy type theory in Coq_. + In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). + Association for Computing Machinery, New York, NY, USA, 164–172. + + +[^4]: + Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. + 2017. _Homotopy Type Theory in Lean_. + In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. + Lecture Notes in Computer Science(), vol 10499. Springer, Cham. +