<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.3 20210610//EN" "JATS-journalpublishing1-3.dtd">
<article article-type="research-article" dtd-version="1.3" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xml:lang="ru"><front><journal-meta><journal-id journal-id-type="publisher-id">mais</journal-id><journal-title-group><journal-title xml:lang="ru">Моделирование и анализ информационных систем</journal-title><trans-title-group xml:lang="en"><trans-title>Modeling and Analysis of Information Systems</trans-title></trans-title-group></journal-title-group><issn pub-type="ppub">1818-1015</issn><issn pub-type="epub">2313-5417</issn><publisher><publisher-name>Yaroslavl State University</publisher-name></publisher></journal-meta><article-meta><article-id pub-id-type="doi">10.18255/1818-1015-2021-4-414-433</article-id><article-id custom-type="elpub" pub-id-type="custom">mais-1568</article-id><article-categories><subj-group subj-group-type="heading"><subject>Research Article</subject></subj-group><subj-group subj-group-type="section-heading" xml:lang="ru"><subject>Theory of Computing</subject></subj-group></article-categories><title-group><article-title>Рекурсивная проверка включения для рекурсивно определенных подтипов</article-title><trans-title-group xml:lang="en"><trans-title>A Recursive Inclusion Checker for Recursively Defined Subtypes</trans-title></trans-title-group></title-group><contrib-group><contrib contrib-type="author" corresp="yes"><contrib-id contrib-id-type="orcid">https://orcid.org/0000-0001-9343-6679</contrib-id><name-alternatives><name name-style="eastern" xml:lang="ru"><surname>Де Нивелле</surname><given-names>Ханс</given-names></name><name name-style="western" xml:lang="en"><surname>De Nivelle</surname><given-names>Hans</given-names></name></name-alternatives><email xlink:type="simple">hans.denivelle@nu.edu.kz</email><xref ref-type="aff" rid="aff-1"/></contrib></contrib-group><aff-alternatives id="aff-1"><aff xml:lang="ru"><institution>Назарбаев Университет</institution><country>Казахстан</country></aff><aff xml:lang="en"><institution>Nazarbayev University</institution><country>Kazakhstan</country></aff></aff-alternatives><pub-date pub-type="collection"><year>2021</year></pub-date><pub-date pub-type="epub"><day>18</day><month>12</month><year>2021</year></pub-date><volume>28</volume><issue>4</issue><fpage>414</fpage><lpage>433</lpage><permissions><copyright-statement>Copyright &amp;#x00A9; Де Нивелле Х., 2021</copyright-statement><copyright-year>2021</copyright-year><copyright-holder xml:lang="ru">Де Нивелле Х.</copyright-holder><copyright-holder xml:lang="en">De Nivelle H.</copyright-holder><license xml:lang="ru" license-type="creative-commons-attribution" xlink:href="https://creativecommons.org/licenses/by/4.0/" xlink:type="simple"><license-p>Данная работа распространяется под лицензией Creative Commons Attribution 4.0.</license-p></license><license xml:lang="en" license-type="creative-commons-attribution" xlink:href="https://creativecommons.org/licenses/by/4.0/" xlink:type="simple"><license-p>This work is licensed under a Creative Commons Attribution 4.0 License.</license-p></license></permissions><self-uri xlink:href="https://www.mais-journal.ru/jour/article/view/1568">https://www.mais-journal.ru/jour/article/view/1568</self-uri><abstract><p>Мы представляем табличную процедуру, которая проверяет логические отношения между рекурсивно определенными подтипами рекурсивно определенных типов, и применяем эту процедуру к проблеме разрешения неоднозначных имен в языке программирования. Эта работа является частью проекта по разработке нового языка программирования, подходящего для эффективной реализации логики. Логические формулы представляют собой древовидные структуры со множеством конструкторов, имеющих различные свойства и типы аргументов. Алгоритмы, использующие эти структуры, должны выполнять анализ вариантов для конструкторов и получать доступ к поддеревьям, тип и существование которых зависят от используемого конструктора. Во многих языках программирования анализ прецедентов обрабатывается путем сопоставления, но мы хотим использовать другой подход, основанный на рекурсивно определенных подтипах. Вместо сопоставления дерева с различными конструкторами мы будем классифицировать его с помощью набора непересекающихся подтипов. Подтипы являются более общими, чем структурные формы, основанные на конструкторах, мы ожидаем, что они могут быть реализованы более эффективно и, кроме того, могут использоваться при статической проверке типов. Это позволяет использовать рекурсивно определенные подтипы в качестве предварительных условий или постусловий функций. Мы определяем типы и подтипы (которые мы будем называть прилагательными), определяем их семантику и даем проверку включения прилагательных на основе таблиц. Мы показываем, как использовать эту проверку включения для разрешения неоднозначных ссылок на поля в объявлениях прилагательных. Та же процедура может быть использована для разрешения неоднозначных вызовов функций.</p></abstract><trans-abstract xml:lang="en"><p>We present a tableaux procedure that checks logical relations between recursively defined subtypes of recursively defined types and apply this procedure to the problem of resolving ambiguous names in a programming language. This work is part of a project to design a new programming language suitable for efficient implementation of logic. Logical formulas are tree-like structures with many constructors having different arities and argument types. Algorithms that use these structures must perform case analysis on the constructors, and access subtrees whose type and existence depend on the constructor used. In many programming languages, case analysis is handled by matching, but we want to take a different approach, based on recursively defined subtypes. Instead of matching a tree against different constructors, we will classify it by using a set of disjoint subtypes. Subtypes are more general than structural forms based on constructors, we expect that they can be implemented more efficiently, and in addition can be used in static type checking. This makes it possible to use recursively defined subtypes as preconditions or postconditions of functions. We define the types and the subtypes (which we will call adjectives), define their semantics, and give a tableaux-based inclusion checker for adjectives. We show how to use this inclusion checker for resolving ambiguous field references in declarations of adjectives. The same procedure can be used for resolving ambiguous function calls.</p></trans-abstract><kwd-group xml:lang="ru"><kwd>проектирование языков программирования</kwd><kwd>системы типов</kwd><kwd>доказательство теорем</kwd><kwd>построение компилятора</kwd></kwd-group><kwd-group xml:lang="en"><kwd>programming language design</kwd><kwd>type systems</kwd><kwd>theorem proving</kwd><kwd>compiler construction</kwd></kwd-group></article-meta></front><back><ref-list><title>References</title><ref id="cit1"><label>1</label><citation-alternatives><mixed-citation xml:lang="ru">Y. Minsky, A. Madhavapeddy, and J. Hickey, Real World OCaml (functional programming for the masses). O'Reilly, 2013.</mixed-citation><mixed-citation xml:lang="en">Y. Minsky, A. Madhavapeddy, and J. Hickey, Real World OCaml (functional programming for the masses). O'Reilly, 2013.</mixed-citation></citation-alternatives></ref><ref id="cit2"><label>2</label><citation-alternatives><mixed-citation xml:lang="ru">G. Hutton, Programming in Haskell (second edition). Cambridge University Press, 2016.</mixed-citation><mixed-citation xml:lang="en">G. Hutton, Programming in Haskell (second edition). Cambridge University Press, 2016.</mixed-citation></citation-alternatives></ref><ref id="cit3"><label>3</label><citation-alternatives><mixed-citation xml:lang="ru">M. Odersky, L. Spoon, and B. Venners, Programming in Scala Third Edition. Artima Press, 2007-2016.</mixed-citation><mixed-citation xml:lang="en">M. Odersky, L. Spoon, and B. Venners, Programming in Scala Third Edition. Artima Press, 2007-2016.</mixed-citation></citation-alternatives></ref><ref id="cit4"><label>4</label><citation-alternatives><mixed-citation xml:lang="ru">P. Rondon, M. Kawaguchi, and R. Jhala, “Liquid Types,” in Programming Language Design and Implementation (PLDI), 2009, pp. 159-169.</mixed-citation><mixed-citation xml:lang="en">P. Rondon, M. Kawaguchi, and R. Jhala, “Liquid Types,” in Programming Language Design and Implementation (PLDI), 2009, pp. 159-169.</mixed-citation></citation-alternatives></ref><ref id="cit5"><label>5</label><citation-alternatives><mixed-citation xml:lang="ru">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.</mixed-citation><mixed-citation xml:lang="en">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.</mixed-citation></citation-alternatives></ref><ref id="cit6"><label>6</label><citation-alternatives><mixed-citation xml:lang="ru">S. Klabnik and C. Nichols, The Rust Programming Language. No Starch Press, 2019.</mixed-citation><mixed-citation xml:lang="en">S. Klabnik and C. Nichols, The Rust Programming Language. No Starch Press, 2019.</mixed-citation></citation-alternatives></ref><ref id="cit7"><label>7</label><citation-alternatives><mixed-citation xml:lang="ru">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.</mixed-citation><mixed-citation xml:lang="en">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.</mixed-citation></citation-alternatives></ref><ref id="cit8"><label>8</label><citation-alternatives><mixed-citation xml:lang="ru">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.</mixed-citation><mixed-citation xml:lang="en">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.</mixed-citation></citation-alternatives></ref></ref-list><fn-group><fn fn-type="conflict"><p>The authors declare that there are no conflicts of interest present.</p></fn></fn-group></back></article>
