TermWare-3 – система переписування термів, заснована на контекстному численні
У статті описується конструкція системи переписування термів TermWare-3, що побудована на основі рефлексивного числення контекстних термів, коли структура терму включає до себе, окрім дерева, ще й внутрішній контекст та обмеження на співставлення при застосуванні (зовнішній контекст), що дозволяє за...
Gespeichert in:
| Veröffentlicht in: | Проблеми програмування |
|---|---|
| Datum: | 2019 |
| Hauptverfasser: | , |
| Format: | Artikel |
| Sprache: | Ukrainisch |
| Veröffentlicht: |
Інститут програмних систем НАН України
2019
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/150921 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | TermWare-3 – система переписування термів, заснована на контекстному численні / Р.С. Шевченко, А.Ю. Дорошенко // Проблеми програмування. — 2019. — № 1. — С. 48-56. — Бібліогр.: 11 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862665918094508032 |
|---|---|
| author | Шевченко, Р.С. Дорошенко, А.Ю. |
| author_facet | Шевченко, Р.С. Дорошенко, А.Ю. |
| citation_txt | TermWare-3 – система переписування термів, заснована на контекстному численні / Р.С. Шевченко, А.Ю. Дорошенко // Проблеми програмування. — 2019. — № 1. — С. 48-56. — Бібліогр.: 11 назв. — укр. |
| collection | DSpace DC |
| container_title | Проблеми програмування |
| description | У статті описується конструкція системи переписування термів TermWare-3, що побудована на основі рефлексивного числення контекстних термів, коли структура терму включає до себе, окрім дерева, ще й внутрішній контекст та обмеження на співставлення при застосуванні (зовнішній контекст), що дозволяє занурити операції розв’язування імен в математичну семантику переписувальних правил. Описується метод ефективної диспетчеризації вибору правил, а також автоматичне перетворення виразів між системами на основі алгебраїчних типів мови Scala та контекстними термами.
В статье описывается конструкция системы переписывания термов TermWare-3, построенной на основе рефлексивного исчисления контекстных термов, когда структура терма включает в себя дополнительно к дереву терма еще внутренний контекст и ограничения на сопоставление (внешний контекст). Это позволяет погрузить операции разрешения имен в математическую семантику переписывающих правил. Элементами алгебры являются мультитермы, которые дополняют контекстные термы конструкциями стрелок, универсальным образцом сопоставления и непротиворечивых множеств. Это позволяет эмулировать подстановку типизированных переменных в рамках алгебры мультитермов. Также описывается метод эффективной диспетчеризации выбора правил. Приводится пример применения системы переписывающих правил для анализа смарт-контрактов вместе с автоматическим преобразованием выражения между системами на основе алгебраических типов Scala и контекстными термами.
In this paper, the design of the TermWare-3 rewriting system which is built on the ground of reflective calculus of context term is considered. In the calculus of the context term, term structure contains not only tree, but a reference to an internal context and matching constrains (external context). This allows to embed operation of name resolving into the mathematical semantics of the term rewriting. The elements of algebra are multiterms, which complement context terms by constructions of arrows, universal matching pattern and consistent set. This allows to emulate substitutions of typed variables in the terms of multiterm algebra. Also, the method of effective rule dispatch is described. Example of usage term rewriting system for checking of smart-contract properties, with automatic transformation of expression between representation in terms of Scala algebraic types and TermWare-3 context terms 
is shown.
|
| first_indexed | 2025-12-07T15:18:42Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-150921 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Ukrainian |
| last_indexed | 2025-12-07T15:18:42Z |
| publishDate | 2019 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Шевченко, Р.С. Дорошенко, А.Ю. 2019-04-18T20:39:51Z 2019-04-18T20:39:51Z 2019 TermWare-3 – система переписування термів, заснована на контекстному численні / Р.С. Шевченко, А.Ю. Дорошенко // Проблеми програмування. — 2019. — № 1. — С. 48-56. — Бібліогр.: 11 назв. — укр. 1727-4907 DOI: https://doi.org/10.15407/pp2019.01.048 https://nasplib.isofts.kiev.ua/handle/123456789/150921 004.4'24 У статті описується конструкція системи переписування термів TermWare-3, що побудована на основі рефлексивного числення контекстних термів, коли структура терму включає до себе, окрім дерева, ще й внутрішній контекст та обмеження на співставлення при застосуванні (зовнішній контекст), що дозволяє занурити операції розв’язування імен в математичну семантику переписувальних правил. Описується метод ефективної диспетчеризації вибору правил, а також автоматичне перетворення виразів між системами на основі алгебраїчних типів мови Scala та контекстними термами. В статье описывается конструкция системы переписывания термов TermWare-3, построенной на основе рефлексивного исчисления контекстных термов, когда структура терма включает в себя дополнительно к дереву терма еще внутренний контекст и ограничения на сопоставление (внешний контекст). Это позволяет погрузить операции разрешения имен в математическую семантику переписывающих правил. Элементами алгебры являются мультитермы, которые дополняют контекстные термы конструкциями стрелок, универсальным образцом сопоставления и непротиворечивых множеств. Это позволяет эмулировать подстановку типизированных переменных в рамках алгебры мультитермов. Также описывается метод эффективной диспетчеризации выбора правил. Приводится пример применения системы переписывающих правил для анализа смарт-контрактов вместе с автоматическим преобразованием выражения между системами на основе алгебраических типов Scala и контекстными термами. In this paper, the design of the TermWare-3 rewriting system which is built on the ground of reflective calculus of context term is considered. In the calculus of the context term, term structure contains not only tree, but a reference to an internal context and matching constrains (external context). This allows to embed operation of name resolving into the mathematical semantics of the term rewriting. The elements of algebra are multiterms, which complement context terms by constructions of arrows, universal matching pattern and consistent set. This allows to emulate substitutions of typed variables in the terms of multiterm algebra. Also, the method of effective rule dispatch is described. Example of usage term rewriting system for checking of smart-contract properties, with automatic transformation of expression between representation in terms of Scala algebraic types and TermWare-3 context terms 
 is shown. uk Інститут програмних систем НАН України Проблеми програмування Інструментальні засоби і середовища програмування TermWare-3 – система переписування термів, заснована на контекстному численні TermWare-3 – система переписывания термов, основанная на исчислении контекстов TermWare-3 – term rewriting system, based on context-term calculus Article published earlier |
| spellingShingle | TermWare-3 – система переписування термів, заснована на контекстному численні Шевченко, Р.С. Дорошенко, А.Ю. Інструментальні засоби і середовища програмування |
| title | TermWare-3 – система переписування термів, заснована на контекстному численні |
| title_alt | TermWare-3 – система переписывания термов, основанная на исчислении контекстов TermWare-3 – term rewriting system, based on context-term calculus |
| title_full | TermWare-3 – система переписування термів, заснована на контекстному численні |
| title_fullStr | TermWare-3 – система переписування термів, заснована на контекстному численні |
| title_full_unstemmed | TermWare-3 – система переписування термів, заснована на контекстному численні |
| title_short | TermWare-3 – система переписування термів, заснована на контекстному численні |
| title_sort | termware-3 – система переписування термів, заснована на контекстному численні |
| topic | Інструментальні засоби і середовища програмування |
| topic_facet | Інструментальні засоби і середовища програмування |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/150921 |
| work_keys_str_mv | AT ševčenkors termware3sistemaperepisuvannâtermívzasnovananakontekstnomučislenní AT dorošenkoaû termware3sistemaperepisuvannâtermívzasnovananakontekstnomučislenní AT ševčenkors termware3sistemaperepisyvaniâtermovosnovannaânaisčisleniikontekstov AT dorošenkoaû termware3sistemaperepisyvaniâtermovosnovannaânaisčisleniikontekstov AT ševčenkors termware3termrewritingsystembasedoncontexttermcalculus AT dorošenkoaû termware3termrewritingsystembasedoncontexttermcalculus |