Л.Ю. Исмаилова1, С.В. Косиков2

1 Национальный исследовательский ядерный университет «МИФИ» (Москва, Россия)

2 НАО «ЮрИнфоР» (Москва, Россия)

1 LYIsmailova@mephi.ru, 2 kosikov.s.v@gmail.com

Постановка проблемы. В настоящее время известны два основных способа построения типовых систем ламбда-исчисления: 1) на основе подхода, предложенного Чёрчем; 2) на основе подхода Карри. В системах на основе подхода Чёрча термы являются аннотированными версиями бестиповых термов. Каждый терм имеет тип, который обычно уникален (с точностью до отношения эквивалентности) и который выводится из способа аннотации терма. В типизированном ламбда-исчислении по Карри каждый терм имеет набор возможных типов. Этот набор может быть пустым, одноэлементным или состоять из нескольких (возможно, бесконечно многих) элементов.

Цель. Представить способ построения типовых систем с разным подходом, выделить их достоинства и недостатки, определить возможность их применения для построения предметно-ориентированной системы типов при конструировании практических аппликативных систем.

Результаты. Представлен способ построения типовых систем на основе разных подходов. Даны рекомендации по их применению при построении предметно-ориентированной системы типов.

Практическая значимость. Результаты работы могут быть использованы при выборе или построении инструментальной системы поддержки прикладных аппликативных систем.

Исмаилова Л.Ю., Косиков С.В. Предметно-ориентированные системы типов в формализме Чёрча и Карри // Информационно-измерительные и управляющие системы. 2024. Т. 22. № 5. С. 39−45. DOI: https://doi.org/10.18127/j20700814-202405-05

1. Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. М.: ЮрИнфоР. 2004. 787 с. ISBN 5-89158-100-0.
2. 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.
3. Ismailova L., Wolfengagen V., Kosikov S. Elements of semantic analysis based on lambda-calculus // Proceedings of BICA*AI. 2022.
4. 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.
5. Williams C., Stay M. Native Type Theory // 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
6. Altenkirch T., Kaposi A. A container model of type theory // 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
7. Mc Bride C., Forsberg F.N. Functorial Adapters // 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
8. 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/.
9. Booij A. Exhaustive testing of property testers // 28th International Conference on Types for Proofs and Programs. 2022. https://types22.inria.fr/.
10. 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//.