20260322: Олег Доманов, Наблюдательная теория типов в семантике естественного языка
Выступление Олега Доманова «Наблюдательная теория типов в семантике естественного языка» на заседании кружка аналитической философии 22 марта 2026 г. Аннотация: Наблюдательная теория типов (Higher Observational Type Theory, HOTT) является третьим из популярных подходов к построению гомотопической теории типов (HoTT) помимо HoTT Book и кубической теории типов. От первой она отличается конструктивностью (унивалентность выполнена по определению), от второй — относительной простотой и «автономностью оснований». Ядром HOTT является определённая теория равенства. Доклад содержит введение в HOTT и некоторые подходы к её использованию для формализации естественного языка (родо-видовые отношения, копредикация). Некоторые источники: 1. Mike Shulman, Higher Observational Type Theory: An autonomous foundation for univalent mathematics (2022) (https://home.sandiego.edu/~shulman/papers/chapman-fall2022.pdf). 2. Mike Shulman, Higher Observational Type Theory (2025) (https://home.sandiego.edu/~shulman/papers/txst-seminar.pdf) 3. Mike Shulman, From HoTT to HOTT: Autonomy in new foundations for mathematics (2024) (https://home.sandiego.edu/~shulman/papers/philsci.pdf). 4. Observational higher dimensions (Narya) (https://narya.readthedocs.io/en/latest/observational.html) 5. nLab: https://ncatlab.org/nlab/show/higher+observational+type+theory (более полный список литературы). 6. Bahramian H.; Nematollahi N.; Sabry A. - Copredication in homotopy type theory (2018).
Выступление Олега Доманова «Наблюдательная теория типов в семантике естественного языка» на заседании кружка аналитической философии 22 марта 2026 г. Аннотация: Наблюдательная теория типов (Higher Observational Type Theory, HOTT) является третьим из популярных подходов к построению гомотопической теории типов (HoTT) помимо HoTT Book и кубической теории типов. От первой она отличается конструктивностью (унивалентность выполнена по определению), от второй — относительной простотой и «автономностью оснований». Ядром HOTT является определённая теория равенства. Доклад содержит введение в HOTT и некоторые подходы к её использованию для формализации естественного языка (родо-видовые отношения, копредикация). Некоторые источники: 1. Mike Shulman, Higher Observational Type Theory: An autonomous foundation for univalent mathematics (2022) (https://home.sandiego.edu/~shulman/papers/chapman-fall2022.pdf). 2. Mike Shulman, Higher Observational Type Theory (2025) (https://home.sandiego.edu/~shulman/papers/txst-seminar.pdf) 3. Mike Shulman, From HoTT to HOTT: Autonomy in new foundations for mathematics (2024) (https://home.sandiego.edu/~shulman/papers/philsci.pdf). 4. Observational higher dimensions (Narya) (https://narya.readthedocs.io/en/latest/observational.html) 5. nLab: https://ncatlab.org/nlab/show/higher+observational+type+theory (более полный список литературы). 6. Bahramian H.; Nematollahi N.; Sabry A. - Copredication in homotopy type theory (2018).