У статті пропонується числення контекстних термів, що доповнює традиційний апарат алгебраїчних сигнатур, котрі використовуються в системах переписування термів, конструкціями роботи з контекстом: утворення контексту, визначення контекстного значення та зв'язку терму з контекстом із перевіркою відповідності. Це дозволяє сформулювати задачі, пов'язані з аналізом та трансформаціями програмного коду, у більш природньому вигляді, оскільки структура вихідного коду в сучасних мовах програмування також має ієрархічну контекстну структуру, що може прямо відповідати структурі терму в переписувальному правилі. Правила виводу типів для мови програмування можуть бути представлені як правила задовільності контексту. Таким чином можна отримати досить простий механізм, що об'єднує переписування термів з аналізом контексту. Застосування підходу описано на прикладі моделювання системи типів сучасних мов програмування: від обмежень на значення до лінійної типізації. Ключові слова: автоматизація розробки програмного забезпечення, мови програмування, переписування термів, системи типів, алгебра типів, аналіз коду, 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.
1. Основні конструкції
. Будемо вважати голову терма також термом, обмеженним функціональні терми видом констант за конструкцією; перетворення (стрілки)
;
Основні особливості – замість термів ми оперуємо “мультитермами”, та також відсутні такі об’єкти як вільні змінні. Ми їх промоделюємо за допомогою контексту: нехай в нас є алфавіт змінних і перетворимо терм з вільнимі змінними у контекстний терм де – атоми, що не входять в оригінальний терм. Таким чином, ми можемо репрезентувати традиційні системи переписування, переінтерпритувавши базові операції. (8) Уніфікація загальних та пустих мультитермів Уніфікація значень в контексті : – операція злиття, яку ми введемо трохи пізніше Де та ctx – операції підстановки та взяття контексту з очевидним змістом.
Можна прочитати це перетворення наступним чином: при уніфікації двох стрілок ми визначаємо сумісність лівих та правих частин, та вертаємо лишу суміcну частину. Якщо уніфіковані стрілки дають різний результат, то визнаємо уніфікацію невдалою. Множинні терми та операції роботи з контекстом
В прикладі з представленням підстановок, контекст підстановки був представлений у вигляді множинного мультитерму . У найпростішому випадку, що дає нам перше інтуїтивне бачення, елементи контексту - це набір стрілок типу атом – значення, проте множинний мультитерм може містити об’єкти іншого роду: наприклад, стрілки загального типу, тоді об’єднання стрілок – це система правил, або просто різнорідні об’єкти без протиріч, тоді це просто набір можливостей вибору.
Ми будемо позначати множинний терм як , вважаючи що a, b та c – сумісні між собою. Створення множини до перевірки сумісності, будемо позначати як . Наприклад, твердження, що одне й те ж значення у контексті повинно бути визначено сумісно, можно записати як: .
Множина інваріантна до повторень та комутативна При об’єднанні атомів, У більш загальному вигляді, можна сказати, що об’єднання як фільтр на уніфікацію. , тобто можна розглядати З того, що множина, де є несумісне значення, є протиріччям, випливає: (9) (10) (11) (12) (13) (14) (19) Поширення на структурні терми та стріли практично аналогічні (18): та множин: (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32) (33) (34) (35).
Введемо також стандартні позначення для існування та селекціі у множинних термах, запозичені з теоріі множинного терму, що містить лише ті терми, що задовольняють p.
Інше об’єднання термів – послідовний перегляд, можна проінтерпретувати як впорядкований перебіг. Тобто розглядаючи набір , ми спочатку шукаємо спробу уніфікувати a, якщо це не спрацювало – тоді c. Це дозволяє відтворити ефект “затінювання” імен (shadowing), коли при переміщенні в контекст, нові імена затінюють старі.
Єдині редукційні правила, що ми можемо додати до послідовного перегляду, – це елімінація пустого терму: ескалація протиріччя та збереження універсального терму: o o o o Нарешті можна формулювати правила роботи з контекстом: x@y, що визначає x у контексті y. Почнемо з співвідношення контексту та граничних термів.
Єдина можлива множина у контексті протиріччя – це пустий мультитерм: Протиріччя у контексті залишається протиріччя (ми хочемо зберегти термінальний об’єкт): Вираз з пустим контекстом еквівалентний виразу без контексту: І контекст пустого терма не має змісту: в нас не існує способів його визначити: Щодо універсального терма: як контекст він не має змісту: але поміщення універсального терму в контекст має зміст – таким чином можна задавати обмеження для можливого матчінгу. Мультитерми передають контекст своїм компонентам: А head та content можна вибирати з контексту, використовуючи контексти лівих частин. Нехай в нас є виділений атом, htag, будемо вибирати як head – атоми з ним у лівій частині контексту. Спочатку визначимо селекцію по тегу: Тепер можна сказати, що (40) визначено однозначно.
Залишилось визначити деталізацію уніфікації для контексту. Контекст зразка може визначати додаткові обмеження на уніфікації, що, як правило, можуть бути виражені у вигляді набору правил, представлених мультитермом.
Оскільки уніфікація симетрична, контекст в y розбирається аналогічно. Можна спростити конструкцію, якщо перенести перевірку правил сумісності в правила контексту. Тоді контекстне правило набуде вигляду:
Проілюструємо використання систем переписування реалізацією аналізу типів: побудуємо моделі основних систем типів. Перше питання: як буде виглядати типізована AST у вигляді контекстного терму? Ми будемо представляти тип контекстом, у якому визначено виділений термін check, що визначає набір правил.
Тобто, якщо у мові програмування (x:E) означає, що x має тип E – то на рівні термів в нас є контекст E, у якому є набір правил check. Інтепретація цього набору правил визначає можливість створення терму у цьому контексті.
Непараметризований список буде визначатись наступним чином: List-> { check-> x-> ( (x <> Nil) || (x <> Cons(y,z)){y->*,z->*@List} )@{ x -> * }@logic де logic – якась система, що надає мінімальну інтерпретацію логічних виразів та уніфікації, (будемо називати її L).
Визначення параметризованого списку виглядає подібним чином:
}
}
Тобто List перетворюється на функціональний терм, де e – параметр, що визначається під час уніфікації.
E – звичайний терм, що може бути представлений у termware. Отже, “натуральною моделлю” типів буде
числення залежних типів [
Також зазначимо, що поки e – не визначено, відсутня різниця між екзистенціальними та параметризованими типами. Щоб побудувати модель системи, що підтримує екзистенціальні типи, ми маємо або збагатити інтерпретатор логіки, додавши аналог квантору існування, або збагатити маппінг термів на типи, додавши позначення для невизначених термів.
У першому випадку, визначення екзистенціального типу буде виглядати подібно до: } Дe exists – має бути визначений в логіці як оператор селекції. В залежності від класу логіки, яку ми оберемо, можна отримати багато варіацій можливої семантики. Це досить цікаве питання для подальшого аналізу, але виходить за рамки короткого опису системи у цій статті.
У другому – можна отримати нотацію, подібну до сколемівських типів у Scala (невизначених аліасів): }
Де element – не аргумент функціонального терму, а елемент, що має бути присутнім у конкретному термі, що використовує контекст List.
Далі, сума та об’єднання типів формулюється очевидним способом (диз’юнкція та кон’юнкція check клауз); алгебраїчні типи – додаванням до check клаузи ще правила визначення підтипу в залежності від дискримінатору.
Як бачимо, елементи систем типів, що зустрічаються у найбільш поширених мовах програмування, прямо моделюються у численні контекстів.
Розглянемо ще менш поширені різновиди – лінійні та афінні типи, що використовуються у мовах з
обліком використання ресурсів (такі як Clean [
Афінний тип – тип, що може бути використаний у програмі один або нуль раз. Приклад – мутабельна змінна, що може бути передана до іншого потоку виконання.
Перше питання – як ми взагалі можемо промоделювати програми з лінійними типами: вочевидь, нам потрібно визначити поняття блоку коду та зв’язати сам тип з входженням у цей блок.
Тут ми можемо визначити лінейний тип як такий, що визначений у LinearStatements. definedIn ми повинні визначити при відображенні AST на терми.
LinearStatements можна розглядати як список виразів. А що таке вираз з точки зору нашого аналізу? Це щось, що може або створювати або використовувати лінійну змінну: } Тепер, можна визначити типизацію блоку коду: 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), 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) на
кшталт описаного в [
Задачі оптимізації на основі додаткових знань або результатів профілюючого виконання програм також можуть бути описані у цьому фреймворку, якщо розглядати метрики ефективності як складові цільового базового контексту. Література Про автора: Шевченко Руслан Сергійович, підприємець. Кількість наукових публікацій в українських виданнях – 11. Кількість наукових публікацій в зарубіжних виданнях – 5.