Предметно-ориентированные системы типов в формализме Чёрча и Карри
- 1 Национальный исследовательский ядерный университет «МИФИ» (Москва, Россия)
- 2 НАО «ЮрИнфоР» (Москва, Россия)
Аннотация
Постановка проблемы. В настоящее время известны два основных способа построения типовых систем ламбда-исчисления: 1) на основе подхода, предложенного Чёрчем; 2) на основе подхода Карри. В системах на основе подхода Чёрча термы являются аннотированными версиями бестиповых термов. Каждый терм имеет тип, который обычно уникален (с точностью до отношения эквивалентности) и который выводится из способа аннотации терма. В типизированном ламбда-исчислении по Карри каждый терм имеет набор возможных типов. Этот набор может быть пустым, одноэлементным или состоять из нескольких (возможно, бесконечно многих) элементов.
Цель. Представить способ построения типовых систем с разным подходом, выделить их достоинства и недостатки, определить возможность их применения для построения предметно-ориентированной системы типов при конструировании практических аппликативных систем.
Результаты. Представлен способ построения типовых систем на основе разных подходов. Даны рекомендации по их применению при построении предметно-ориентированной системы типов.
Практическая значимость. Результаты работы могут быть использованы при выборе или построении инструментальной системы поддержки прикладных аппликативных систем.
- Поступила
- 30.08.2024
- Одобрена
- 13.09.2024
- Принята
- 27.09.2024
Для цитирования
Исмаилова Л.Ю., Косиков С.В. Предметно-ориентированные системы типов в формализме Чёрча и Карри // Информационно-измерительные и управляющие системы. 2024. Т. 22. № 5. С. 39−45. DOI: https://doi.org/10.18127/j20700814-202405-05
Список источников
- Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. М.: ЮрИнфоР. 2004. 787 с. ISBN 5-89158-100-0.
- Wolfengagen V., Ismailova L., Kosikov S. When and Where Conceptual Maths Equals to Conceptual Modeling: Reasons for Using in Cognitive Modeling // Proceedings of BICA*AI. 2023.
- Ismailova L., Wolfengagen V., Kosikov S. Elements of semantic analysis based on lambda-calculus // Proceedings of BICA*AI. 2022.
- Slieptsov I., Ismailova L., Kosikov S. Analysis and comparison of generators of words of context-sensitive language on example of typed λ-calculus // Proceedings of BICA*AI. 2022.
- Williams C., Stay M. Native Type Theory // 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
- Altenkirch T., Kaposi A. A container model of type theory // 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
- Mc Bride C., Forsberg F.N. Functorial Adapters // 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
- Dybjer P., Setzer A. Implementing Martin-Löf’s Meaning Explanations for Intuitionistic Type Theory in Agda // 28th International Conference on Types for Proofs and Programs. 2022. https://types22.inria.fr/.
- Booij A. Exhaustive testing of property testers // 28th International Conference on Types for Proofs and Programs. 2022. https://types22.inria.fr/.
- Shulman M. The unifying power of modal type theory // The Second International Conference on Homotopy Type Theory (HoTT). 2023. https://hott.github.io/HoTT-2023//.