Перейти к содержанию

Другие решатели

Rzk — не первый и не единственный решатель для (варианта) гомотопической теории типов. Ниже следует неполный список существующих решателей и библиотек формализаций на них.

Agda

Agda — это язык программирования с зависимыми типами, а также решатель теорем.

Хотя по умолчанию Agda не совместима с гомотопической теории типов из-за встроенной аксиомы K, решатель поддерживает опцию --without-K, позволяющей восстановить совместимость с унивалентностью. Стоит отметить основные формализации гомотопической теории типов на Agde: agda-unimath и HoTT-Agda.

Синтаксис выражений в Rzk частично вдохновлён синтаксисом Agda. Экспериментальная поддержка автоматического форматирования кода Rzk основана на стиле принятом в проектах emilyriehl/yoneda и rzk-lang/sHoTT, который в свою очередь вдохновлён стилем agda-unimath.

Agda реализована на языке программирования Haskell.

Arend

Arend — это решатель теорем для гомотопической теории типов со встроенным типом (ненаправленного) интервала, что делает его схожим с кубическими системами типов. Стандартная библиотека формализаций Arend находится в JetBrains/arend-lib.

Arend разрабатывается JetBrains и реализован на языке Java. Также существует плагин для IntelliJ IDEA, превращающий её в полноценную среду разработки для Arend.

Aya

Aya — экспериментальный кубический решатель теорем, с системой типов, схожей с Cubical Agda, redtt, и Arend. Также в Aya есть поддержка сопоставления с образцом, допускающая пересекающиеся и неупорядоченные образцы, а также возможности для функционального программирования, аналогичные Haskell и Idris.

Aya реализована на Java.

Формализации на Aya?

Мне неизвестны библиотеки формализации на Aya.

Семейство red*

cooltt, redtt, и RedPRL представляют семейство экспериментальных решателей теорем, разработанных командой RedPRL.

Существует формализация математической библиотеки redtt

Семейство решателей red* реализовано на языке программирования OCaml. Создатели семества решателей также работают над проектом A.L.G.A.E., который нацелен на реализацию ряда удобных библиотек (для OCaml) для помощи в реализации решателей теорем на основе проверки типов для ядра решателя.

Coq

Coq — это зрелый решатель теорем, основанный на исчислении индуктивных конструкций. Первая формализация гомотопической теории типов и унивалентных оснований, UniMath, начатая Владимиром Воеводским, была создана с использованием Coq и до сих пор развивается и поддерживается координационным комитетом UniMath. Ещё одна важная формализация гомотопической теории типов — это Coq-HoTT3.

Coq реализован на OCaml.

Cubical Agda

Cubical Agda (кубическая Агда) — это расширение Agda набором возможностей кубической теории типов1 2.

Хотя технически это расширение Agda, лучше рассматривать его как отдельный язык. Кубическая Agda (как и другие кубические решатели) поддерживает вариацию типов-расширений (аналогично Rzk), но только для кубических интервалов.

Важными проектами формализации на кубической Agda являются библиотека cubical и проект 1lab.

Кубическая Agda является частью Agda и также реализована на Haskell.

cubicaltt

cubicaltt — это экспериментальный кубический решатель1 и предшественник Cubical Agda.

Некоторые формализации на cubicaltt находятся в https://github.com/mortberg/cubicaltt/tree/master/examples.

cubicaltt реализован на языке Haskell.

Lean

Lean — это решатель теорем и язык программирования с зависимыми типами, основанный на исчислении индуктивных конструкций. Аналогично Coq, Lean способствует широкому использованию тактик и автоматизации.

Lean 2, как и Agda, поддерживал режим без уникальности доказательств тождеств (Uniqueness of Identity Proofs, UIP), который допускал совместимость с гомотопической теорией типов. Поэтому, существует формализация HoTT на Lean 24. Однако, Lean 2 больше не поддерживается и формализация, соответственно, тоже.

Lean 3 и 4 убрали режим, допускающий (прямую) формализацию гомотопической теории типов. Несмотря на это проект Ground Zero продолжает формализацию HoTT на Lean 4. Проект использует проверку элиминации, портированную из неподдерживаемого проекта по переносу библиотеки HoTT с Lean 2 на Lean 3. Эта проверка позволяет поддерживать окружение HoTT, совместимое со стандартным окружением Lean (по крайней мере по убеждениям авторов проекта). В частности, попытка (напрямую) доказать принцип неразличимости доказательств равенства (Uniqueness of Identity Proofs) приводит к ошибки типизации в рамках проекта Ground Zero.

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) https://doi.org/10.4230/LIPIcs.TYPES.2015.5 ↩↩

  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. https://doi.org/10.1145/3209108.3209197 ↩

  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. https://doi.org/10.1145/3018610.3018615 ↩

  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. https://doi.org/10.1007/978-3-319-66107-0_30 ↩