Рекурсивная проверка включения для рекурсивно определенных подтипов
https://doi.org/10.18255/1818-1015-2021-4-414-433
Аннотация
Мы представляем табличную процедуру, которая проверяет логические отношения между рекурсивно определенными подтипами рекурсивно определенных типов, и применяем эту процедуру к проблеме разрешения неоднозначных имен в языке программирования. Эта работа является частью проекта по разработке нового языка программирования, подходящего для эффективной реализации логики. Логические формулы представляют собой древовидные структуры со множеством конструкторов, имеющих различные свойства и типы аргументов. Алгоритмы, использующие эти структуры, должны выполнять анализ вариантов для конструкторов и получать доступ к поддеревьям, тип и существование которых зависят от используемого конструктора. Во многих языках программирования анализ прецедентов обрабатывается путем сопоставления, но мы хотим использовать другой подход, основанный на рекурсивно определенных подтипах. Вместо сопоставления дерева с различными конструкторами мы будем классифицировать его с помощью набора непересекающихся подтипов. Подтипы являются более общими, чем структурные формы, основанные на конструкторах, мы ожидаем, что они могут быть реализованы более эффективно и, кроме того, могут использоваться при статической проверке типов. Это позволяет использовать рекурсивно определенные подтипы в качестве предварительных условий или постусловий функций. Мы определяем типы и подтипы (которые мы будем называть прилагательными), определяем их семантику и даем проверку включения прилагательных на основе таблиц. Мы показываем, как использовать эту проверку включения для разрешения неоднозначных ссылок на поля в объявлениях прилагательных. Та же процедура может быть использована для разрешения неоднозначных вызовов функций.
Ключевые слова
MSC2020: 68Q99, 03B70
Список литературы
1. Y. Minsky, A. Madhavapeddy, and J. Hickey, Real World OCaml (functional programming for the masses). O'Reilly, 2013.
2. G. Hutton, Programming in Haskell (second edition). Cambridge University Press, 2016.
3. M. Odersky, L. Spoon, and B. Venners, Programming in Scala Third Edition. Artima Press, 2007-2016.
4. P. Rondon, M. Kawaguchi, and R. Jhala, “Liquid Types,” in Programming Language Design and Implementation (PLDI), 2009, pp. 159-169.
5. R. Jhala and N. Vazou, “Refinement Types: A Tutorial,” Foundations and Trends in Programming Languages, vol. 6, no. 3-4, pp. 159-317, 2021, doi: 10.1561/2500000032.
6. S. Klabnik and C. Nichols, The Rust Programming Language. No Starch Press, 2019.
7. Michael Gelfond and Vladimar Lifschitz, “The Stable Model Semantics for Logic Programming,” in Fifth International Conference and Symposium on Logic Programming, 1988, pp. 1070-1080.
8. G. S. Tseytin, “On the complexity of Derivation in the Propositional Calculus,” in Studies in Constructive Mathematics and Mathematical Logic, Part II, 1970, pp. 115-125.
Рецензия
Для цитирования:
Де Нивелле Х. Рекурсивная проверка включения для рекурсивно определенных подтипов. Моделирование и анализ информационных систем. 2021;28(4):414-433. https://doi.org/10.18255/1818-1015-2021-4-414-433
For citation:
De Nivelle H. A Recursive Inclusion Checker for Recursively Defined Subtypes. Modeling and Analysis of Information Systems. 2021;28(4):414-433. (In Russ.) https://doi.org/10.18255/1818-1015-2021-4-414-433