Context term calculus for rewriting systems
In this paper, a calculus of context-full terms is proposed. Calculus extends the traditional algebraic signatures, used in term rewriting systems, by so-called constructions, that works with context: context constructor, resolving a context value and binding term to context with compatibility check...
Збережено в:
| Дата: | 2018 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2018
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/259 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-259 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/75/54e30aa8e39c68a75d47d3e9847cbf75.pdf |
| spelling |
pp_isofts_kiev_ua-article-2592024-04-28T11:37:22Z Context term calculus for rewriting systems Исчисление контекстных термов для систем переписывания Числення контекстних термів для систем переписування Shevchenko, R.S. software development automation; term rewriting; type systems; programming languages; code analysis; termware UDC 004.4'24 автоматизация разработки программного обеспечения; переписывания термов; системы типов; языки программирования УДК 004.4'24 автоматизація розробки програмного забезпечення; мови програмування; переписування термів; системи типів; алгебра типів; аналіз коду; termware УДК 004.4'24 In this paper, a calculus of context-full terms is proposed. Calculus extends the traditional algebraic signatures, used in term rewriting systems, by so-called constructions, that works with context: context constructor, resolving a context value and binding term to context with compatibility checking. Such extension allows to refining algorithms connected with analysis and transformations of source code in the more natural form, because f the structure of the sense in the modern programming language defined in hierarchical contexts, which can be directly mapped to context-full term in rewriting rule. Type analysis for a programming language can be implemented as checking for context compatibility. In such way, relative simple mechanism, which unites term rewriting and context analysis can be received. The approach is illustrated by defining rules for typing in context-full term formalism.Problems in programming 2018; 2-3: 021-030 В статье предлагается исчисление контекстных термов, которое дополняет традиционный аппарат алгебраических сигнатур, использующихся в системах переписывания термов, конструкциями работы с контекстом: конструирования контекста и операциями определения контекстного значения и связи терма с контекстом с проверкой соответствия. Это позволяет сформулировать задачи, связанные с анализом и трансформацией программного кода в более естественном виде, так как структура исходного кода в современных языках программирования также обладает иерархической контекстной структурой, что может прямо соответствовать структуре терма в переписывающих правилах. Правила вывода типов для языка программирования могут быть отображены в правила соответствия контексту. Таким образом мы получили довольно простой механизм, объединяющий переписывание термов и анализ контекста. Применение подхода описано на примере формулирования с помощью этого механизма распространенных систем типов.Problems in programming 2018; 2-3: 021-030 У статті пропонується числення контекстних термів, що доповнює традиційний апарат алгебраїчних сигнатур, котрі використовуються в системах переписування термів, конструкціями роботи з контекстом: утворення контексту, визначення контекстного значення та зв’язку терму з контекстом із перевіркою відповідності. Це дозволяє сформулювати задачі, пов’язані з аналізом та трансформаціями програмного коду, у більш природньому вигляді, оскільки структура вихідного коду в сучасних мовах програмування також має ієрархічну контекстну структуру, що може прямо відповідати структурі терму в переписувальному правилі. Правила виводу типів для мови програмування можуть бути представлені як правила задовільності контексту. Таким чином можна отримати досить простий механізм, що об’єднує переписування термів з аналізом контексту. Застосування підходу описано на прикладі моделювання системи типів сучасних мов програмування: від обмежень на значення до лінійної типізації.Problems in programming 2018; 2-3: 021-030 Інститут програмних систем НАН України 2018-11-05 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/259 10.15407/pp2018.02.021 PROBLEMS IN PROGRAMMING; No 2-3 (2018); 21-30 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2018); 21-30 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2018); 21-30 1727-4907 10.15407/pp2018.02 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/259/253 Copyright (c) 2018 PROBLEMS OF PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2024-04-28T11:37:22Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
software development automation term rewriting type systems programming languages code analysis termware UDC 004.4'24 |
| spellingShingle |
software development automation term rewriting type systems programming languages code analysis termware UDC 004.4'24 Shevchenko, R.S. Context term calculus for rewriting systems |
| topic_facet |
software development automation term rewriting type systems programming languages code analysis termware UDC 004.4'24 автоматизация разработки программного обеспечения переписывания термов системы типов языки программирования УДК 004.4'24 автоматизація розробки програмного забезпечення мови програмування переписування термів системи типів алгебра типів аналіз коду termware УДК 004.4'24 |
| format |
Article |
| author |
Shevchenko, R.S. |
| author_facet |
Shevchenko, R.S. |
| author_sort |
Shevchenko, R.S. |
| title |
Context term calculus for rewriting systems |
| title_short |
Context term calculus for rewriting systems |
| title_full |
Context term calculus for rewriting systems |
| title_fullStr |
Context term calculus for rewriting systems |
| title_full_unstemmed |
Context term calculus for rewriting systems |
| title_sort |
context term calculus for rewriting systems |
| title_alt |
Исчисление контекстных термов для систем переписывания Числення контекстних термів для систем переписування |
| description |
In this paper, a calculus of context-full terms is proposed. Calculus extends the traditional algebraic signatures, used in term rewriting systems, by so-called constructions, that works with context: context constructor, resolving a context value and binding term to context with compatibility checking. Such extension allows to refining algorithms connected with analysis and transformations of source code in the more natural form, because f the structure of the sense in the modern programming language defined in hierarchical contexts, which can be directly mapped to context-full term in rewriting rule. Type analysis for a programming language can be implemented as checking for context compatibility. In such way, relative simple mechanism, which unites term rewriting and context analysis can be received. The approach is illustrated by defining rules for typing in context-full term formalism.Problems in programming 2018; 2-3: 021-030 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2018 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/259 |
| work_keys_str_mv |
AT shevchenkors contexttermcalculusforrewritingsystems AT shevchenkors isčisleniekontekstnyhtermovdlâsistemperepisyvaniâ AT shevchenkors čislennâkontekstnihtermívdlâsistemperepisuvannâ |
| first_indexed |
2024-09-16T04:08:22Z |
| last_indexed |
2024-09-16T04:08:22Z |
| _version_ |
1818568415891161088 |
| fulltext |
Теоретичні та методологічні основи програмування
© Р.С. Шевченко, 2018
ISSN 1727-4907. Проблеми програмування. 2018. № 2–3. Спеціальний випуск 21
УДК 004.4'24
ЧИСЛЕННЯ КОНТЕКСТНИХ ТЕРМІВ ДЛЯ СИСТЕМ
ПЕРЕПИСУВАННЯ
P.C. Шевченко
У статті пропонується числення контекстних термів, що доповнює традиційний апарат алгебраїчних сигнатур, котрі
використовуються в системах переписування термів, конструкціями роботи з контекстом: утворення контексту, визначення
контекстного значення та зв’язку терму з контекстом із перевіркою відповідності. Це дозволяє сформулювати задачі, пов’язані
з аналізом та трансформаціями програмного коду, у більш природньому вигляді, оскільки структура вихідного коду в сучасних
мовах програмування також має ієрархічну контекстну структуру, що може прямо відповідати структурі терму в
переписувальному правилі. Правила виводу типів для мови програмування можуть бути представлені як правила задовільності
контексту. Таким чином можна отримати досить простий механізм, що об’єднує переписування термів з аналізом контексту.
Застосування підходу описано на прикладі моделювання системи типів сучасних мов програмування: від обмежень на значення
до лінійної типізації.
Ключові слова: автоматизація розробки програмного забезпечення, мови програмування, переписування термів, системи типів,
алгебра типів, аналіз коду, termware.
В статье предлагается исчисление контекстных термов, которое дополняет традиционный аппарат алгебраических сигнатур,
использующихся в системах переписывания термов, конструкциями работы с контекстом: конструирования контекста и
операциями определения контекстного значения и связи терма с контекстом с проверкой соответствия. Это позволяет
сформулировать задачи, связанные с анализом и трансформацией программного кода в более естественном виде, так как
структура исходного кода в современных языках программирования также обладает иерархической контекстной структурой,
что может прямо соответствовать структуре терма в переписывающих правилах. Правила вывода типов для языка
программирования могут быть отображены в правила соответствия контексту. Таким образом мы получили довольно простой
механизм, объединяющий переписывание термов и анализ контекста. Применение подхода описано на примере
формулирования с помощью этого механизма распространенных систем типов.
Ключевые слова: автоматизация разработки программного обеспечения, переписывания термов, системы типов, языки
программирования.
In this paper, a calculus of context-full terms is proposed. Calculus extends the traditional algebraic signatures, used in term rewriting
systems, by so-called constructions, that works with context: context constructor, resolving a context value and binding term to context
with compatibility checking. Such extension allows to refining algorithms connected with analysis and transformations of source code in
the more natural form, because f the structure of the sense in the modern programming language defined in hierarchical contexts, which
can be directly mapped to context-full term in rewriting rule. Type analysis for a programming language can be implemented as checking
for context compatibility. In such way, relative simple mechanism, which unites term rewriting and context analysis can be received.
The approach is illustrated by defining rules for typing in context-full term formalism.
Key words: software development automation, term rewriting, type systems, programming languages, code analysis, termware.
Вступ
Використання переписувальних правил є широко відомою технологією. Існує багато формалізацій,
заснованих на різному підгрунті: від імперативної операційної семантики[1, 2] до екваціональної логіки, 𝜌-
числення [3] та числення зразків (pattern-calculus) [4]. Існує також декілька мов програмування, побудованих
на основі переписування термів.
Одним із типових застосувань подібних систем є опис семантик мов програмування. Класичні системи
переписувальних правил можуть використовуватися для опису трансформацій стану “в малому”, але
необхідність роботи з контекстом сильно обмежує можливості декларативного аналізу. Існують різні
підходи до вирішення цієї проблеми: аналізатори програм, що засновані на termware [5], використовують так
звані ‘збагачені’ терми, що завжди містять додатковий елемент, що дає доступ до запитів інформації з
контексту; Stratego[6] (зараз Spoofax) використовує набори правил, що залежать від контексту.
Ще один підхід – абстрактний синтаксис вищого порядку (high order abstract syntax)[7], де AST з
інформацією про змінні представлено у вигляді лямбда-терму, де зв’язані імена представлені як змінні, що
зв’язані в лямбда-термах.
У цій статті для роботи з контекстом пропонується числення контекстних термів, що доповнює
традиційний апарат алгебраїчних сигнатур конструкціями роботи з контекстом . Підхід полягає у побудові
алгебри контекстних термів, де операції щодо контекстних термів виражені у явному вигляді.
1. Основні конструкції
Нехай 𝐶 – множина константних символів, з виділеною підмножиною атомів 𝐴 ⊂ C та функціональних
термів 𝐹 ⊂ 𝐴, побудуємо на її основі множину контекстних мультитермів 𝐶𝑇(𝑇), що буде включати в себе:
константи 𝐶𝑖;
Теоретичні та методологічні основи програмування
22
функціональні терми 𝑓𝑜(𝑡1… 𝑡𝑛) ∈ 𝐹. Будемо вважати голову терма також термом, обмеженним
видом констант за конструкцією;
перетворення (стрілки) 𝑎 → 𝑏;
контекст context(a,b) або 𝑎@𝑏, що можна читати як a в контексті b, де a та b – будь-які терми.
(Також в формулах будемо іноді використовувати нотацію 𝑎𝑏);
множинні мультитерми (або Or – вирази) {𝑡1 … 𝑡𝑛};
послідовність альтернатив 𝑡1| 𝑡2| … | 𝑡𝑜𝑡ℎ𝑒𝑟;
порожній мультитерм ∅, який можна інтерпретувати як “пустий множинний мультитерм”;
універсальний мультитерм ∗, який можна інтерпретувати як “сумісний з будь-яким мультитермом;
мультитерм протиріччя ⊥.
Основні особливості – замість термів ми оперуємо “мультитермами”, та також відсутні такі об’єкти як
вільні змінні. Ми їх промоделюємо за допомогою контексту: нехай в нас є алфавіт змінних �̃� = { 𝑥1̃, . . 𝑥�̃�} і
перетворимо терм з вільнимі змінними 𝑓(�̃�1, 𝑥�̃�) у контекстний терм 𝑓(𝑥1, 𝑥2)@{ 𝑥1 → ∗ , 𝑥2 →∗ } де 𝑥1, 𝑥2 –
атоми, що не входять в оригінальний терм. Таким чином, ми можемо репрезентувати традиційні системи
переписування, переінтерпритувавши базові операції.
Уніфікація
Почнемо з уніфікації. В нашій інтерпретації вона перетворються в бінарну операцію над термами, що
повертає уніфікатор у контексті підстановок, що перетворюють будь-який аргумент на найбільш конкретний
уніфікатор. Будемо позначати уніфікація a та b як unify(a,b) або скорочено 𝑎 ⋄ 𝑏.
Для констант та мультитермів:
𝑎 ⋄ 𝑎 = 𝑎 , (1)
𝑎 ⋄ 𝑏 = ∅ 𝑖𝑓𝑓 𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶, 𝑎 ≠ 𝑏, (2)
ми можемо замінити при уніфікації символ на його значення в контексті:
(𝑎 ⋄ 𝑣 )@(𝑣 → 𝑥) ⟹ 𝑎 ⋄ 𝑥@(𝑣 → 𝑥) (3)
два значення мають бути сумісними:
(𝑣 ⋄ 𝑤) @{𝑣 → 𝑥,𝑤 → 𝑦} ⟹ 𝑘@{𝑣 → 𝑘,𝑤 → 𝑘, 𝑘 → 𝑥 ⋄ 𝑦 }. (4)
Тепер додамо до розгляду структурні терми:
𝑓(𝑥1, … 𝑥𝑛) ⋄ 𝑔(𝑦1, … 𝑦𝑚) = {
𝑓(𝑣1…𝑣𝑛)@{𝑣1 → 𝑥1 ⋄ 𝑦1, … , 𝑣𝑛 → 𝑥𝑛 ⋄ 𝑦𝑛}
∅. 𝑓 ≠ 𝑔
∅, 𝑛 ≠ 𝑚
. (5)
Множинні терми:
{𝑎, 𝑏} ⋄ 𝑐 = { 𝑎 ⋄ 𝑐, 𝑏 ⋄ 𝑐}, (6)
та симетрично:
𝑎 ⋄ {𝑏, 𝑐} = { 𝑎 ⋄ 𝑏, 𝑎 ⋄ 𝑐}. (7)
Послідовна перевірка:
(𝑎 |𝑏) ⋄ 𝑐 = {
𝑎 ⋄ 𝑐 , 𝑎 ⋄ 𝑐 ≠ ∅
𝑏 ⋄ 𝑐, 𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒
(8)
та симетрично:
Теоретичні та методологічні основи програмування
23
𝑎 ⋄ (𝑏 |𝑐) = {
𝑎 ⋄ 𝑏, 𝑎 ⋄ 𝑏 ≠ ∅
𝑎 ⋄ 𝑐, 𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒
. (9)
Уніфікація загальних та пустих мультитермів
𝑎 ⋄ ∗ ⟹ 𝑎 , (10)
∗ ⋄ 𝑎 ⟹ 𝑎, (11)
𝑎 ⋄ ∅ ⟹ {
∅, 𝑎 ≠⊥
⊥, 𝑎 =⊥
, (12)
𝑎 ⋄⊥=⊥. (13)
Уніфікація значень в контексті :
(𝑎𝑏) ⋄ (𝑐𝑑) = (𝑎 ⋄ 𝑐)𝑏 ∪𝑑. (14)
Де 𝑏 ∪ 𝑑 – операція злиття, яку ми введемо трохи пізніше
(𝑎 → 𝑏) ⋄ (𝑐 → 𝑑) =
{
(𝑎 ⋄ 𝑐 → 𝑏′ ⋄ 𝑑′)@𝑐𝑡𝑥(𝑎 ⋄ 𝑐),
𝑏′ = 𝑠𝑢𝑏𝑠𝑡(𝑏, 𝑐𝑡𝑥(𝑎 ⋄ 𝑐))
𝑑′ = 𝑠𝑢𝑏𝑠𝑡(𝑑, 𝑐𝑡𝑥(𝑎 ⋄ 𝑐))
𝑖𝑓𝑓 𝑎 ⋄ 𝑐 ≠ ∅ , 𝑏′ ⋄ 𝑑′ ≠ ∅
∅, 𝑎 ⋄ 𝑐 = ∅ 𝑜𝑟 𝑏′ ⋄ 𝑑′ = ∅
⊥, (𝑎𝑛𝑦 𝑜𝑓 𝑎𝑟𝑔𝑢𝑚𝑒𝑛𝑡𝑠 =⊥)
. (15)
Де 𝑠𝑢𝑏𝑠𝑡 та ctx – операції підстановки та взяття контексту з очевидним змістом.
Можна прочитати це перетворення наступним чином: при уніфікації двох стрілок ми визначаємо
сумісність лівих та правих частин, та вертаємо лишу суміcну частину. Якщо уніфіковані стрілки дають різний
результат, то визнаємо уніфікацію невдалою.
Множинні терми та операції роботи з контекстом
В прикладі з представленням підстановок, контекст підстановки був представлений у вигляді
множинного мультитерму {𝑎, 𝑏, 𝑐}. У найпростішому випадку, що дає нам перше інтуїтивне бачення,
елементи контексту - це набір стрілок типу атом – значення, проте множинний мультитерм може містити
об’єкти іншого роду: наприклад, стрілки загального типу, тоді об’єднання стрілок – це система правил, або
просто різнорідні об’єкти без протиріч, тоді це просто набір можливостей вибору.
Ми будемо позначати множинний терм як {𝑎, 𝑏, 𝑐}, вважаючи що a, b та c – сумісні між собою.
Створення множини до перевірки сумісності, будемо позначати як 𝑎 ∪ 𝑏. Наприклад, твердження, що одне
й те ж значення у контексті повинно бути визначено сумісно, можно записати як: (𝑥 → 𝑎) ∪ (𝑥 → 𝑏) = 𝑥 →
𝑎 ⋄ 𝑏 .
Множина інваріантна до повторень
𝑎 ∪ 𝑎 = 𝑎; (16)
та комутативна
𝑎 ∪ 𝑏 = 𝑏 ∪ 𝑎. (17)
При об’єднанні атомів,
𝑎 ∪ 𝑏 = { 𝑎, 𝑏} 𝑖𝑓𝑓 (𝑎 ⋄ 𝑏) = ∅. (18)
У більш загальному вигляді, можна сказати, що 𝑎 ∪ 𝑏 = (𝑎 ⋄ 𝑏) ∪ 𝑎 ∪ 𝑏, тобто можна розглядати
об’єднання як фільтр на уніфікацію.
З того, що множина, де є несумісне значення, є протиріччям, випливає:
(𝑎 → ∅) ∪ 𝑏 =⊥. (19)
Теоретичні та методологічні основи програмування
24
Також додамо правила роботи з граничними термами:
𝑎 ∪∗ = ∗, (21)
𝑎 ∪ ∅ = 𝑎; (22)
𝑎 ∪⊥=⊥. (23)
Та мультитермами:
𝑎 ∪ {𝑏, 𝑐} = (𝑎 ∪ 𝑏) ∪ 𝑐, (24)
𝑎 ∪ (𝑏 |𝑐) = (𝑎 ∪ 𝑏)|(𝑎 ∪ 𝑐). (25)
Поширення на структурні терми та стріли практично аналогічні (18):
(𝐹 = 𝑓(𝑥1, … 𝑥𝑛)) ∪ (𝐺 = 𝑔(𝑦1, … 𝑦𝑚)) = { 𝐹 ⋄ 𝐺, 𝐹, 𝐺 }, (26)
та
(𝑎 → 𝑏) ∪ (𝑐 → 𝑑) = { (𝑎 → 𝑏) ⋄ (𝑐 → 𝑑), 𝑎 → 𝑏, 𝑐 → 𝑑)}. (27)
Введемо також стандартні позначення для існування та селекціі у множинних термах, запозичені з теоріі
множин: 𝑥 ∈ { 𝑥1…𝑥𝑛} − скорочення для (𝑥 = 𝑥1) ∨ …∨ (𝑥 = 𝑥𝑛); 𝑣 = {𝑥 ∈ 𝑦| 𝑝(𝑥)} – для ⋃ {
𝑥, 𝑝(𝑥)
∅, ¬𝑝(𝑥)𝑥∈𝑦
множинного терму, що містить лише ті терми, що задовольняють p.
Інше об’єднання термів – послідовний перегляд, можна проінтерпретувати як впорядкований перебіг.
Тобто розглядаючи набір 𝑎 → 𝑏 | 𝑐 → 𝑑, ми спочатку шукаємо спробу уніфікувати a, якщо це не спрацювало –
тоді c. Це дозволяє відтворити ефект “затінювання” імен (shadowing), коли при переміщенні в контекст, нові
імена затінюють старі.
Єдині редукційні правила, що ми можемо додати до послідовного перегляду, – це
елімінація пустого терму:
o ∅| 𝑥 = 𝑥; (28)
o 𝑥|∅ = 𝑥; (29)
ескалація протиріччя
o ⊥ | 𝑥 = ⊥; (30)
o 𝑥 | ⊥= ⊥; (31)
та збереження універсального терму:
∗ | 𝑥 = {
∗, 𝑥 ≠⊥
⊥, 𝑥 =⊥
. (32)
Нарешті можна формулювати правила роботи з контекстом: x@y, що визначає x у контексті y. Почнемо
з співвідношення контексту та граничних термів.
Єдина можлива множина у контексті протиріччя – це пустий мультитерм:
𝑥@ ⊥ = {
⊥ 𝑖𝑓 𝑥 ==⊥
∅
. (33)
Протиріччя у контексті залишається протиріччя (ми хочемо зберегти термінальний об’єкт):
⊥ @ 𝑥 = ⊥ . (34)
Вираз з пустим контекстом еквівалентний виразу без контексту:
𝑥@∅ = 𝑥. (35).
І контекст пустого терма не має змісту: в нас не існує способів його визначити:
Теоретичні та методологічні основи програмування
25
∅@𝑥 = ∅. (36)
Щодо універсального терма: як контекст він не має змісту:
𝑥@ ∗ = ⊥, (37)
але поміщення універсального терму в контекст має зміст – таким чином можна задавати обмеження для
можливого матчінгу. Мультитерми передають контекст своїм компонентам:
{𝑎, 𝑏. . }𝑥 = {𝑎𝑥 , 𝑏𝑥}; (38)
(𝑎|𝑏)𝑥 = 𝑎𝑥|𝑏𝑥. (39)
Залишилась взаємодія між структурними термами та контекстом. Спочатку, наведемо декілька різних
прикладів прагматики застосування:
Нехай у нас є структурний терм у контексті: 𝑓(𝑡1, … 𝑡𝑛)@{𝑎 → 𝑏, 𝑐 → 𝑑,… }. З одного боку, субтерм 𝑡𝑖
має мати доступ до загального контексту (тобто 𝑓(𝑡1, . . 𝑡𝑛)
𝑎 = 𝑓(𝑡1
𝑎… 𝑡𝑛
𝑎)), якщо a – це щось типу доступу до
глобальних елементів; з іншого боку – ми хочемо в контексті зберігати деякі речі, специфічні для 𝑓(… ) в
цілому, скажемо тип 𝑓 або обмеження на вигляд аргументів. Тому контекст структурного терму складається з
двох частин: контекст форми (в коді – head-контекст), що стосується форми 𝑓 та не передається в
аргументи, та контекст змісту (в коді – content-контекст), що передається. Тоді ми зможемо записати
передачу контексту як:
𝑓(𝑡1, … 𝑡𝑛)
𝑎 = 𝑓ℎ𝑒𝑎𝑑(𝑎)(𝑡1
𝑐𝑜𝑛𝑡𝑒𝑛𝑡(𝑎)… 𝑡𝑛
𝑐𝑜𝑛𝑡𝑒𝑛𝑡(𝑎)
). (40)
А head та content можна вибирати з контексту, використовуючи контексти лівих частин. Нехай в нас є
виділений атом, htag, будемо вибирати як head – атоми з ним у лівій частині контексту.
Спочатку визначимо селекцію по тегу:
𝑡𝑎𝑔𝑆𝑒𝑙𝑒𝑐𝑡(𝑎, 𝑡𝑎𝑔) = {
𝑎, 𝑡𝑎𝑔 ∈ 𝑙𝑒𝑓𝑡(ℎ)
∅, 𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒
. (41)
Де
𝑙𝑒𝑓𝑡(ℎ) = {
{𝑙𝑒𝑓𝑡(𝑎1), . . 𝑙𝑒𝑓𝑡(𝑎𝑛)}, ℎ = { 𝑎1, … 𝑎𝑛}
𝑙𝑒𝑓𝑡(𝑎1)|… |𝑙𝑒𝑓𝑡(𝑎𝑛), ℎ = 𝑎1|… |𝑎𝑛
𝑎, 𝑙𝑒𝑓𝑡 = 𝑎 → 𝑏
ℎ, 𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒
, (42)
ℎ𝑒𝑎𝑑(𝑥) = 𝑡𝑎𝑔𝑆𝑒𝑙𝑒𝑐𝑡(𝑥, ℎ𝑡𝑎𝑔), (43)
𝑐𝑜𝑛𝑡𝑒𝑛𝑡(𝑥) = {𝑎 ∈ 𝑥|ℎ𝑒𝑎𝑑(𝑎) == ∅} . (44)
Тепер можна сказати, що (40) визначено однозначно.
Залишилось визначити деталізацію уніфікації для контексту. Контекст зразка може визначати додаткові
обмеження на уніфікації, що, як правило, можуть бути виражені у вигляді набору правил, представлених
мультитермом.
𝑥𝑎 ⋄ 𝑦 = {
(𝑥 ⋄ 𝑦)𝑎, ∃ (𝑐ℎ𝑒𝑐𝑘 → 𝑟) ∈ 𝑎, 𝑎𝑝𝑝𝑙𝑦(𝑟, 𝑥 ⋄ 𝑦) ⇒ 𝑡𝑟𝑢𝑒
∅ , ∃(𝑐ℎ𝑒𝑐𝑘 → 𝑟) ∈ 𝑎, 𝑎𝑝𝑝𝑙𝑦(𝑟, 𝑥 ⋄ 𝑦) ⇏ 𝑡𝑟𝑢𝑒
𝑥 ⋄ 𝑦 , 𝑐ℎ𝑒𝑐𝑘 ∉ 𝑙𝑒𝑓𝑡(𝑎)
. (45)
Оскільки уніфікація симетрична, контекст в y розбирається аналогічно. Можна спростити
конструкцію, якщо перенести перевірку правил сумісності в правила контексту. Тоді контекстне правило
набуде вигляду:
𝑥𝑎 = ∅ 𝑖𝑓𝑓 ∃(𝑐ℎ𝑒𝑐𝑘 → 𝑟) ∈ 𝑎: 𝑎𝑝𝑝𝑙𝑦(𝑟, 𝑥) ⇏ 𝑡𝑟𝑢𝑒. (46)
А уніфікація контексту матимите вигляд: 𝑥𝑎 ⋄ 𝑦 = (𝑥 ⋄ 𝑦)𝑎, або для двох контекстів:
𝑥𝑎 ⋄ 𝑦𝑏 = (𝑥 ⋄ 𝑦)𝑎∪𝑏. (47)
Теоретичні та методологічні основи програмування
26
Це всі основні правила конструкції, тепер ми можемо перейти до визначення дії правил
переписування.
Основне правило залишається точно таким, як і в традиційних системах:
𝑎𝑝𝑝𝑙𝑦(𝑝 → 𝑥, 𝑦) = {
𝑠𝑢𝑏𝑠𝑡(𝑥, 𝑐𝑡𝑥(𝑝 ⋄ 𝑦)), 𝑝 ⋄ 𝑦 ≠ ∅
∅, 𝑝 ⋄ 𝑦 = ∅
. (48)
Множинні терми дозволяють вибирати (паралельно) всі правила, що підходять, а також обробляти
множину правил:
𝑎𝑝𝑝𝑙𝑦(𝑎 ∪ 𝑏, 𝑦) = 𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑦) ∪ 𝑎𝑝𝑝𝑙𝑦(𝑏, 𝑦), (49)
𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑥 ∪ 𝑦) = 𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑥) ∪ 𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑦). (50)
А послідовні перетворення дають нам семантику пріоритетного виконання
𝑎𝑝𝑝𝑙𝑦(𝑎|𝑏, 𝑦) = {
𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑦), 𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑦) ≠ ∅
𝑎𝑝𝑝𝑙𝑦(𝑏, 𝑦), 𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑦) = ∅
, (51)
𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑥|𝑦) = {
𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑥), 𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑥) ≠ ∅
𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑦), 𝑎𝑝𝑝𝑙𝑦(𝑎, 𝑥) = ∅
. (52)
Граничні терми є нижчими елементами решіток (без суперечностей):
𝑎𝑝𝑝𝑙𝑦(𝑎, ∅) = ∅ , 𝑎𝑝𝑝𝑙𝑦(∅, 𝑎) = 𝑎. (53)
Та з суперечністю:
𝑎𝑝𝑝𝑙𝑦(𝑎, ⊥) =⊥, та 𝑎𝑝𝑝𝑙𝑦(⊥, 𝑎) = {
∅, 𝑎 = ∅
⊥, 𝑎 ≠ ∅
, (54)
𝑎𝑝𝑝𝑙𝑦(∗, 𝑥) = ⊥, 𝑎𝑝𝑝𝑙𝑦(𝑥,∗) = ∅. (55)
Залишилось визначити співвідношення перетворення і контекста: тут ми можемо, як у випадку з
уніфікацією, використовувати значення контексту для перевірки:
(𝑎 → 𝑏)𝑐 = 𝑎𝑐 → 𝑏𝑐𝑜𝑛𝑡𝑒𝑛𝑡(𝑣), (56)
𝑎𝑝𝑝𝑙𝑦(𝑎𝑐 → 𝑏, 𝑥) = {
𝑠𝑢𝑏𝑠𝑡(𝑏, 𝑐𝑡𝑥(𝑎 ⋄ 𝑥)𝑐), 𝑎 ⋄ 𝑥 ≠ ∅
∅, 𝑎 ⋄ 𝑥 = ∅
. (57)
Далі, семантику виводу будуємо точно так само, як і у традиційних системах:
Застосування набору правил r до терму t за допомогою стратегіі s, що визначає порядок перебору,
можна визначити наступним чином:
𝑠. 𝑡𝑟𝑎𝑣𝑒𝑟𝑠𝑒(𝑡 → (𝑎𝑝𝑝𝑙𝑦(𝑟, 𝑡)|𝑡)).
Тобто стратегія замінює у термі підтерми на результат apply, або залишає без змін, якщо правила не
можуть бути застосовані бути прикладено (apply повертає ∅ ).
2. Приклад: формулювання типів
Проілюструємо використання систем переписування реалізацією аналізу типів: побудуємо моделі
основних систем типів. Перше питання: як буде виглядати типізована AST у вигляді контекстного терму?
Ми будемо представляти тип контекстом, у якому визначено виділений термін check, що визначає набір
правил.
Тобто, якщо у мові програмування (x:E) означає, що x має тип E – то на рівні термів в нас є контекст E, у
якому є набір правил check. Інтепретація цього набору правил визначає можливість створення терму у цьому
контексті.
Непараметризований список буде визначатись наступним чином:
Теоретичні та методологічні основи програмування
27
List-> {
check-> x-> (
(x <> Nil)
||
(x <> Cons(y,z)){y->*,z->*@List}
)@{ x -> * }@logic
}
}
де logic – якась система, що надає мінімальну інтерпретацію логічних виразів та уніфікації, (будемо називати
її L).
Визначення параметризованого списку виглядає подібним чином:
{List(e) -> {
check-> x-> (
(x <> Nil)
||
(x <> Cons(y,z)){y->*@e,z->*@List(e)}
)@{ x -> * }@logic
}
}}@{e->*}
Тобто List перетворюється на функціональний терм, де e – параметр, що визначається під час уніфікації.
E – звичайний терм, що може бути представлений у termware. Отже, “натуральною моделлю” типів буде
числення залежних типів [8].
Також зазначимо, що поки e – не визначено, відсутня різниця між екзистенціальними та
параметризованими типами. Щоб побудувати модель системи, що підтримує екзистенціальні типи, ми маємо
або збагатити інтерпретатор логіки, додавши аналог квантору існування, або збагатити маппінг термів на типи,
додавши позначення для невизначених термів.
У першому випадку, визначення екзистенціального типу буде виглядати подібно до:
Ex.List -> {
(List e)(e->exists)@logic
}
Дe exists – має бути визначений в логіці як оператор селекції. В залежності від класу логіки, яку ми оберемо,
можна отримати багато варіацій можливої семантики. Це досить цікаве питання для подальшого аналізу, але
виходить за рамки короткого опису системи у цій статті.
У другому – можна отримати нотацію, подібну до сколемівських типів у Scala (невизначених аліасів):
List -> {
check-> x-> (
(x <> Nil)
||
(x <> Cons(y,z)){y->*@element,z->*@(List@{`element->element})}
Теоретичні та методологічні основи програмування
28
)@{ x -> * }@logic,
element -> *
}
Де element – не аргумент функціонального терму, а елемент, що має бути присутнім у конкретному
термі, що використовує контекст List.
Далі, сума та об’єднання типів формулюється очевидним способом (диз’юнкція та кон’юнкція check
клауз); алгебраїчні типи – додаванням до check клаузи ще правила визначення підтипу в залежності від
дискримінатору.
Як бачимо, елементи систем типів, що зустрічаються у найбільш поширених мовах програмування,
прямо моделюються у численні контекстів.
Розглянемо ще менш поширені різновиди – лінійні та афінні типи, що використовуються у мовах з
обліком використання ресурсів (такі як Clean [9], Rust [10], Pony [11]).
Тип називається лінійним, якщо один вираз цього типу може бути використан у програмі лише один
раз. (Приклад – у мові з тракінгом ресурсів, показчик на мутабельну область пам’яті, що може бути
переданий у іншу функцію без копіювання. Функція-отримувач має або передати його далі, або звільнити).
Афінний тип – тип, що може бути використаний у програмі один або нуль раз. Приклад – мутабельна
змінна, що може бути передана до іншого потоку виконання.
Перше питання – як ми взагалі можемо промоделювати програми з лінійними типами: вочевидь, нам
потрібно визначити поняття блоку коду та зв’язати сам тип з входженням у цей блок.
Linear{
check -> (x -> LinearStatements(definedIn@x))@(x->*)
definedIn -> (x -> *@LinearStatements)@(x->*)
}
Тут ми можемо визначити лінейний тип як такий, що визначений у LinearStatements. definedIn ми
повинні визначити при відображенні AST на терми.
LinearStatements можна розглядати як список виразів. А що таке вираз з точки зору нашого аналізу? Це
щось, що може або створювати або використовувати лінійну змінну:
LinearStatement {
usage -> (x -> boolean)@(x->*@Linear),
created -> List *@Linear
}
Тепер, можна визначити типизацію блоку коду:
LinearStatements = {
check -> {x -> checkLinear(Nil, Nil, x)}@(x->*),
checkLinear -> {
(nonUsed, used, statements) ->
{
if (statements = Nil) -> used = Nil and nonUsed=Nil,
if (statements = Cons(statement,rest)@(statement->*@LinearStatement,
rest -> (List *@LinearStatement))
-> checkLinear(
created(statement) + nonUsed.filter(!statement@usage),
Теоретичні та методологічні основи програмування
29
used + nonUsed.filter(statement@usage),
rest
)
and checkNonUsed(nonUsed,statement)
}
},
checkNonUsed -> {
(Nil, statement) -> true
(Cons(x,y),statement) -> !statement@usage(x) and checkNonUsed(y,statement)
}
}
(Тут +, filter – операція додавання списків, що може бути визначена очевидним чином).
Таким чином, маємо таке формулювання: лінійний тип – це такий тип, що вираз цього типу, визначений
у блоці, використовується там лише один раз, декларативно виражено мовою переписуючих систем.
Висновки
Отже, числення контексту дозволяє декларативно промоделювати сучасні системи типів та здійснювати
семантичний аналіз та перетворення програм, залишаючись у рамках декларативної парадигми
переписувальних правил. Поєднуючи різну логічну семантику з відображенням мов програмування, можна
отримати різні версії систем типизації.
Наступні кроки:
верифікація і побудова верифікованої моделі у coq;
імплементація наступної версії termware на основі числення контекстних термів;
імплементація швидкого алгоритму співставлення.
Заначимо, що множинний терм з набором правил можна вважати стандартною моделлю як для
контекста, так і для системи переписуючих правил без пріоритетів. Застосування системи таких правил є
процесом резолвінгу терму в контексті.
Ще однією широкою темою для досліджень є перетворення термів між різними базами контекстів.
Тоді, представляючи контекстом операції середовища виконання, можна переформулювати задачу компіляції
або інтерпретації терму як перенос терму програми в інший контекст. Якщо маркувати черговість елімінації
контексту при перетворенні терму, отримаємо можливість моделювання процесу “постановки”(staging) на
кшталт описаного в [12], де рівень мета-змінних відповідає відповідним міткам контексту.
Задачі оптимізації на основі додаткових знань або результатів профілюючого виконання програм
також можуть бути описані у цьому фреймворку, якщо розглядати метрики ефективності як складові
цільового базового контексту.
Література
1. Jan Willem Klop and Vincent van Oostrom and Femke van Raamsdonk. Combinatory Reduction Systems: introduction and survey. Theoretical
Computer Science. Vol. 121. 1993. P. 279–308.
2. Doroshenko A., Shevchenko R. A rewriting framework for rule-based programming dynamic applications. Fundamenta Informaticae. 2006.
Vol. 72. N 1–3. P. 95–108.
3. Dan Dougherty, Pierre Lescanne, Luigi Liquori, Frédéric Lang. Addressed Term Rewriting Systems: Syntax, Semantics, and Pragmatics.
Electronic Notes in Theoretical Computer Science. Vol. 127, Issue 5, 27 May 2005. P. 57–82.
4. Cirstea, Horatiu and Kirchner, Claude and Liquori, Luigi. Rewriting Calculus with(out) Types. Proceedings of the fourth workshop on rewriting
logic and applications. Electronic Notes in Theoretical Computer Science, Sep. 2002. .
5. C. Barry Jay and Delia Kesner. Pure Pattern Calculus. ACM Trans. Program. Lang. Syst. 2005. P. 263–274.
6. Martin Bravenboer and Karl Trygve Kalleberg and Rob Vermaas and Eelco Visser. {Stratego/XT 0.17}. {A} language and toolset for program
transformation. Science of Computer Programming. Vol. 72. 2008. P. 52–70.
Теоретичні та методологічні основи програмування
30
7. Pfenning, F. and Elliott, C., Higher-order Abstract Syntax. Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language
Design and Implementation. PLDI-88. 1998. P. 199–208.
8. Bove, Ana; Peter Dybjer . Dependent Types at Work. LerNet ALFA Summer School. 2008: P. 57–99.
9. Rinus Plasmeijer and Marko van Eekelen, Keep it Clean: A unique approach to functional programming. ACM Sigplan Notices, June 1999.
10. Eric Reed. Patina: A Formalization of the Rust Programming Language. University of Washington. Technical Report. 2015.
11. Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, Andy McNeil, Deny Capabilities for Safe, Fast Actors. Causality Ltd., Imperial
College London, 2015.
12. Nada Amin and Tiark Rompf. Collapsing Towers of Interpreters. Proc. ACM Program. Lang. 2, POPL, Article 33 (January 2018). 33 p.
References
1. Jan Willem Klop and Vincent van Oostrom and Femke van Raamsdonk. Combinatory Reduction Systems: introduction and survey. Theoretical
Computer Science. Vol. 121. 1993. P. 279–308.
2. Doroshenko A., Shevchenko R. A rewriting framework for rule-based programming dynamic applications. Fundamenta Informaticae. 2006.
Vol. 72. N 1–3. P. 95–108.
3. Dan Dougherty, Pierre Lescanne, Luigi Liquori, Frédéric Lang. Addressed Term Rewriting Systems: Syntax, Semantics, and Pragmatics.
Electronic Notes in Theoretical Computer Science. Vol. 127, Issue 5, 27 May 2005. P. 57–82.
4. Cirstea, Horatiu and Kirchner, Claude and Liquori, Luigi. Rewriting Calculus with(out) Types. Proceedings of the fourth workshop on rewriting
logic and applications. Electronic Notes in Theoretical Computer Science, Sep. 2002. .
5. C. Barry Jay and Delia Kesner. Pure Pattern Calculus. ACM Trans. Program. Lang. Syst. 2005. P. 263–274.
6. Martin Bravenboer and Karl Trygve Kalleberg and Rob Vermaas and Eelco Visser. {Stratego/XT 0.17}. {A} language and toolset for program
transformation. Science of Computer Programming. Vol. 72. 2008. P. 52–70.
7. Pfenning, F. and Elliott, C., Higher-order Abstract Syntax. Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language
Design and Implementation. PLDI-88. 1998. P. 199–208.
8. Bove, Ana; Peter Dybjer . Dependent Types at Work. LerNet ALFA Summer School. 2008: P. 57–99.
9. Rinus Plasmeijer and Marko van Eekelen, Keep it Clean: A unique approach to functional programming. ACM Sigplan Notices, June 1999.
10. Eric Reed. Patina: A Formalization of the Rust Programming Language. University of Washington. Technical Report. 2015.
11. Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, Andy McNeil, Deny Capabilities for Safe, Fast Actors. Causality Ltd., Imperial
College London, 2015.
12. Nada Amin and Tiark Rompf. Collapsing Towers of Interpreters. Proc. ACM Program. Lang. 2, POPL, Article 33 (January 2018). 33 p.
Про автора:
Шевченко Руслан Сергійович,
підприємець.
Кількість наукових публікацій в українських виданнях – 11.
Кількість наукових публікацій в зарубіжних виданнях – 5.
http://orcid.org/0000-0002-1554-2019.
Місце роботи автора:
ПП “Руслан Шевченко”.
E-mail: ruslan@shevchenko.kiev.ua
|