-calculus as a realistic formalization of a class of rewriting systems

A new formalism of typed -calculus is offered as theoretical foundation for the construction of the special classes of programming systems based on rewriting rules. The formalism utilizes the ordered non-confluent sets of rewriting rules and interaction with programming environment that allows to e...

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2025
Hauptverfasser:	Shevchenko, R.S., Doroshenko, A.Yu.
Format:	Artikel
Sprache:	Russian
Veröffentlicht:	PROBLEMS IN PROGRAMMING 2025
Schlagworte:	UDC 681.3
Online Zugang:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/803
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Problems in programming
Завантажити файл:

Institution

Problems in programming

id	pp_isofts_kiev_ua-article-803
record_format	ojs
resource_txt_mv	ppisoftskievua/fd/a5db1171d653d87f8f054f9142f037fd.pdf
spelling	pp_isofts_kiev_ua-article-8032025-08-28T20:52:26Z -calculus as a realistic formalization of a class of rewriting systems n- исчисление – реалистичная формализация класса переписывающих систем -числення – реалістична формалізація класу переписувальних систем Shevchenko, R.S. Doroshenko, A.Yu. UDC 681.3 УДК 51:681.3 УДК 51:681.3 A new formalism of typed -calculus is offered as theoretical foundation for the construction of the special classes of programming systems based on rewriting rules. The formalism utilizes the ordered non-confluent sets of rewriting rules and interaction with programming environment that allows to extend possibilities of programming dynamic applications.Problems in programming 2011; 2: 3-11 Предложен новый формализм типизированного η-исчисления в качестве теоретической основы для по-строения специальных классов систем программирования на основе переписывающих правил. Форма-лизм использует упорядоченные неконфлюэнтные множества правил переписывания и взаимодействие с программным окружением, что позволяет расширить возможности программирования динамических приложений.Problems in programming 2011; 2: 3-11 Запропоновано новий формалізм типізованого -числення як теоретичної бази для побудови спеціальних класів систем програмування на основі переписувальних правил. Формалізм використовує впорядковані неконфлюентні множини правила переписування і взаємодію з програмним оточенням, що дозволяє розширити можливості програмування динамічних застосувань.Problems in programming 2011; 2: 3-11 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-08-28 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/803 PROBLEMS IN PROGRAMMING; No 2 (2011); 3-11 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2 (2011); 3-11 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2 (2011); 3-11 1727-4907 ru https://pp.isofts.kiev.ua/index.php/ojs1/article/view/803/855 Copyright (c) 2025 PROBLEMS IN PROGRAMMING
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2025-08-28T20:52:26Z
collection	OJS
language	Russian
topic	UDC 681.3
spellingShingle	UDC 681.3 Shevchenko, R.S. Doroshenko, A.Yu. -calculus as a realistic formalization of a class of rewriting systems
topic_facet	UDC 681.3 УДК 51:681.3 УДК 51:681.3
format	Article
author	Shevchenko, R.S. Doroshenko, A.Yu.
author_facet	Shevchenko, R.S. Doroshenko, A.Yu.
author_sort	Shevchenko, R.S.
title	-calculus as a realistic formalization of a class of rewriting systems
title_short	-calculus as a realistic formalization of a class of rewriting systems
title_full	-calculus as a realistic formalization of a class of rewriting systems
title_fullStr	-calculus as a realistic formalization of a class of rewriting systems
title_full_unstemmed	-calculus as a realistic formalization of a class of rewriting systems
title_sort	-calculus as a realistic formalization of a class of rewriting systems
title_alt	n- исчисление – реалистичная формализация класса переписывающих систем -числення – реалістична формалізація класу переписувальних систем
description	A new formalism of typed -calculus is offered as theoretical foundation for the construction of the special classes of programming systems based on rewriting rules. The formalism utilizes the ordered non-confluent sets of rewriting rules and interaction with programming environment that allows to extend possibilities of programming dynamic applications.Problems in programming 2011; 2: 3-11
publisher	PROBLEMS IN PROGRAMMING
publishDate	2025
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/803
work_keys_str_mv	AT shevchenkors calculusasarealisticformalizationofaclassofrewritingsystems AT doroshenkoayu calculusasarealisticformalizationofaclassofrewritingsystems AT shevchenkors nisčislenierealističnaâformalizaciâklassaperepisyvaûŝihsistem AT doroshenkoayu nisčislenierealističnaâformalizaciâklassaperepisyvaûŝihsistem AT shevchenkors čislennârealístičnaformalízacíâklasuperepisuvalʹnihsistem AT doroshenkoayu čislennârealístičnaformalízacíâklasuperepisuvalʹnihsistem
first_indexed	2025-09-17T09:23:24Z
last_indexed	2025-09-17T09:23:24Z
_version_	1850413023586418688
fulltext	Теоретичні та методологічні основи програмування УДК 51:681.3 Р.С. Шевченко, А.Е. Дорошенко η-ИСЧИСЛЕНИЕ – РЕАЛИСТИЧНАЯ ФОРМАЛИЗАЦИЯ КЛАССА ПЕРЕПИСЫВАЮЩИХ СИСТЕМ Предложен новый формализм типизированного η-исчисления в качестве теоретической основы для по- строения специальных классов систем программирования на основе переписывающих правил. Форма- лизм использует упорядоченные неконфлюэнтные множества правил переписывания и взаимодействие с программным окружением, что позволяет расширить возможности программирования динамических приложений. Введение Техника символьных преобразова- ний, основанная на правилах переписыва- ния термов, является мощным средством разработки программных систем. Системы переписывания известны давно и сущест- вует довольно много формализмов для их описания, такие как эквациональная логи- ка [1], ρ-исчисление [2] или λ-исчисление с образцом [3, 4], снабженные разнообраз- ной системой типов [5]. Однако при разра- ботке и использовании систем переписы- вания становится очевидной неполнота описания математическими моделями су- ществующей практики техники переписы- вания и соответствующие ограничения, а именно: • математические модели в боль- шинстве своем описывают семантику не- упорядоченных конфлюэнтных систем правил без приоритетов, хотя достаточно удобными оказываются системы с исполь- зованием упорядоченного набора правил, где порядок применения определяется ли- бо отношением конкретизации, либо при- оритетом, а наборы правил формально не- конфлюэнтны; • в качестве ввода и вывода обычно используется множества термов, при этом существуют применения для системы с интерактивным взаимодействием; • кроме действий по сопоставлению с определенным образцом, также исполь- зуются действия по неудачному сопостав- лению; обычно это сопровождается рас- ширением существующих моделей, доста- точно сильно меняющим первоначальную семантику [6]. В данной работе строится форма- лизм типового исчисления, названный η- исчислением, как возможное теоретиче- ское обоснование для класса систем пере- писывания с упорядоченными правилами и взаимодействием со внешней средой, пре- доставляющих разработчику полный на- бор возможностей по определению средств проектирования приложений. В частности, рассмотрен способ встраивания средств ввода/вывода в структуру типов языка, чтобы анализ типов мог включать в себя анализ взаимодействия с окружающей средой, что может быть полезно с точки зрения оптимизации программ. η- исчисление строится на замкнутых термах без использования свободных переменных, что дает некоторый новый взгляд на спектр возможностей программной реали- зации. Реализацию η-исчисления с систе- мой типов и анализом взаимодействий планируется встроить в следующую вер- сию авторской системы Termware [7, 8]. 1. Модель переписывающих систем 1.1. Основные обозначения. Рас- смотрим некоторое множество термов T над алфавитом A с помощью некоторой индуктивной схемы, содержащей множе- ство переменных X. Для термов обозначение g◄h означает, что g содержится в h. Мно- Thg ∈, ISSN 1727-4907. Проблеми програмування. 2011. № 2 © Шевченко Р.С., Дорошенко А.Е., 2011 3 Теоретичні та методологічні основи програмування жество свободных переменных терма t обозначается fv(t). Подстановка – это мно- жество пар, состоящих из свободных пе- ременных и термов. Результат применения подстановки S к терму t будем обозначать как t[S]. Синтаксическую эквивалентность термов будем обозначать t1=t2, а эквива- лентность экземпляров — t1≡t2 . Для мно- жеств будем использовать декартово про- изведение X×Y и проекции X⎪i, а именно: X×Y – это множество пар (x,y) таких, что x∈X, y∈Y; (x,y)⎪1 = x, (x,y)⎪2 = y. Для мно- жества пар S определим S⎪i = {s\|i: s∈S}. Последовательность элементов seq(x1,…, …,xn) будет иногда обозначаться как (x1,…,xn). Проекция (x1,…,xn)⎪i также мо- жет быть применена к последовательности и обозначает i-й элемент этой последова- тельности. 1.2. Нетипизированное η-исчис- ление. Пусть наш алфавит состоит из кон- стант ci∈C, функциональных символов fi∈F и пропозициональных переменных xi ∈ X. Теперь множество неограниченных η- термов Tη S может быть построено индук- тивно: • константы С: если ci∈C, то ci∈ Tη S. Также будем предполагать, что C содержит выделенную константу для ошибки, которую будем обозначать как ⊥, и булевские значения true и false; • переменные Х: если xi ∈ X, то xi ∈ Tη S; • функции 1-го порядка F: если fi∈F, t1,...,tn∈Tη S, то f(t1,...,tn)∈Tη S; предпо- лагается, что множество функциональных символов включает, по крайней мере, кон- структор последовательности seq(x1,...,xn), проекции proji, условное выражение cond(x,y,z) и тождественное преобразова- ние id; • композиции функций высших по- рядков: если t ∈, t1,...,tn ∈ Tη S, то t(t1,...,tn) ∈ Tη S; • η-термы: если v={x1....xn: xi∈X}, f,g,h∈Tη S, то (ηv.f → g\|h)∈ Tη S; также будет использоваться написание η v.f → g как сокращение для η v.f → g\|id; • let-конструкция: let x ← f.g (ино- гда будем использовать альтернативный синтаксис g where x ←f ). Пусть r = (η v.f → g\|h) ∈ Tη S. Назо- вем X(t) множество переменных, связан- ных с cамым верхним η-термом (т. е. v); P(t), T(t) и F(t) обозначим, соответственно, образец, результат в случае успеха в со- поставлении и в случае неуспеха (т. е. f, g, h, соответственно). Теперь выберем из Tη S подмножест- во Tη с полностью связанными перемен- ными, включающее: • константы: если ci ∈ C, то ci ∈ Tη; • функции первого порядка: если f∈F, t1,...,tn ∈Tη, то f(t1,...,tn)∈ Tη; • композиции функций высших по- рядков: если t∈Tη, t1,...,tn∈Tη, то t(t1,...,tn)∈Tη; • полностью связанные η-термы: если v={x1,...,xn: xi ∈X}, f,g,h∈Tη, и t=(ηv.f→ g\|h), то t∈Tη при одновременном выполнении следующих условий: 1) ∀ x ∈ X : x ◄ f ⇒ x ∈ X(t) или x◄η z1... zn .fz→ gz\|hz ◄ g; 2) ∀ x ∈ X: x ◄ g ⇒ x∈X(t)∧ x ◄ f или x ◄ η z1...zn .fz→ gz\|hz ◄ g; 3) ∀ x ∈ X: x ◄ h ⇒ x∈X(t) ∧ x◄f или x ◄ η z1...zn .fz→ gz\|hz ◄ h. Иными словами, все η-термы закрыты, любая переменная из g находится в какой- либо η-конструкции (либо самой верхней, либо внутри g); то же относится и к пере- менными из h. Для каждой переменной х можно определить η-конструкцию, в кото- рой она определена. Будем обозначать эту конструкцию как ηt(x). 1.3. Операционная семантика. Ос- новная операция семантической модели – это редукция η-правила: ⎪⎩ ⎪ ⎨ ⎧ ¬ == =→ ).,( если, ;\|),( и \|),( если],[ )\|.(η 2 1 qfmatchhq qfmatchS qfmatchSg qhgfv 4 Теоретичні та методологічні основи програмування Таким образом, успех правила пе- реписывания зависит от успеха сопостав- ления образца в левой части правила с ар- гументом. Будем преобразовывать η- выражения в условные выражения: (ηv .f → g\|h) q = let m ← ← match(f,q).cond(m\|1,q[m\|2],h q) (η:match). Условные выражения могут быть редуцированы, когда первый аргумент принимает значение true или false, а имен- но: cond(true,f,g)=f; cond(false,f,g)=g. Let- выражения используются в основном для совместного использования подтермов и могут быть полностью элиминированы: let x ← y.z = z [{(x,y)}]. Собственно, суть формализации со- стоит в разрешении проблемы сопоставле- ния. Результатом сопоставления будет па- ра из булевского значения и подстановки: два терма x и y совместимы, если сущест- вует подстановка S, такая что x[S]=y. Оп- ределим процесс сопоставления таким об- разом, что поведение сопоставления зави- сит от уровня вложенности переменных. При сопоставлении переменных, опреде- ленных в разных η-выражениях, соответ- ствующая пара добавляется в результи- рующую подстановку. Но если сравнива- ются две переменные, определенные в од- ном η-выражении, то они должны быть синтаксически эквивалентны. Пусть теперь x,y ∈ X. Тогда: var).:( )(η)(ηесли ),,( )(η)(η если )),(,( ),( match ytxt yx ytxt yx yxmatch ⎪ ⎪ ⎩ ⎪⎪ ⎨ ⎧ ⎪ ⎪ ⎭ ⎪⎪ ⎬ ⎫ ≡ ∅= ≡¬ ← = = true Если x∈X и y ∉ X, то просто добав- ляем пару в подстановку: match(x,y) = = (true, (x←y)) (match:var). Сопоставление структурных термов можно определить, как обычно, по индук- ции. Пусть x и y – функциональные термы, x=x0(x1,...,xn), y=y0(y1,...,ym). Тогда: fun),:( если ),,( если ,),( ),( 0 match nm nm yxmatch yxmatch n i ii ⎪ ⎪ ⎪ ⎩ ⎪⎪ ⎪ ⎨ ⎧ ⎪ ⎪ ⎪ ⎭ ⎪⎪ ⎪ ⎬ ⎫ ≠ ∅ == = ∏ = false где произведение на парах определено следующим образом: ⎪ ⎪ ⎩ ⎪⎪ ⎨ ⎧ ∅= ⊕∪∪∧ = =∧ мы,несовместиони если ),,( совместимы и если )),(,( ),(),( 21 212121 2211 yx ss ssssbb sbsb а два множества совместимы, если выпол- няются условия ∀ x,y,z: (x,y)∈s1 ∧ (x,z)∈s2 ⇒ ⇒ match(y,z) и (s1⊕ s2) = , U p ),( zy p ={x,y,z:(x,y) ∈ s1, (x,z) ∈ s2}. Заметим, что сопоставление кон- стант получается тривиальным образом: ).( если ),,( если ),,( ),( 21 21 21 match:c cc cc ccmatch ⎪ ⎪ ⎩ ⎪⎪ ⎨ ⎧ ⎪ ⎪ ⎭ ⎪⎪ ⎬ ⎫ ≠ ∅ = ∅ = = false true При этом термы с разными заглав- ными конструкциями не могут быть сопо- ставлены и, соответственно, сравнимы. Вышеописанные правила некон- флюэнтны, если образец содержит выра- жения из Tη. К примеру, терм match(cond(true,1,2),1) будет редуциро- 5 Теоретичні та методологічні основи програмування ваться к true или false в зависимости от того, будет ли вначале вычисляться внеш- ний или внутренний подтерм. Обычно во избежание подобной не- однозначности в формализмах фиксирует- ся порядок редукций. Предложим не- сколько другой подход, основанный на том, что выявление неоднозначности мо- жет иметь определенный смысл с точки зрения программирования и с точки зрения прагматики лучше выявить и локализовать противоречие в системе правил, а не при- давать четко фиксированный результат неоднозначной системе. Более подробно предотвращение неоднозначности будет рассмотрено в разделе 3. 2. Интенсиональное равенство как замена переименования переменных Построенное исчисление переписы- вающих правил высшего порядка основано на замкнутых термах, где пропозицио- нальные переменные действуют в разных областях разных η-выражений. Основан- ные на этой семантике процессы вычисле- ний могут избегать переименования пере- менных во время применения правил пе- реписывания, так как переменные должны быть разными только внутри одного η- терма. Однако вместо такого определения области действия можно использовать две операции, не входящие в традиционную операционную семантику языков и ис- пользующие: • возможность по переменной определить η-терм, в котором эта пере- менная определена; • интенсиональное равенство t1≡t2, если t1 и t2 – это один и тот же терм (под- разумевая, что реализация не использует неявно различаемые подтермы). 6 Таким образом, необходимость и “магия” переименования переменных ком- пенсируется необходимостью разрыва идентичности η-термов при копировании. Естественной интерпретацией равенства ≡ может быть сравнение машинных адресов (с тем ограничением, что система должна заменять адрес во время η-переписыва- ния). Можно переопределить η-исчис- ление и без интенсионального равенства, используя модель “термов с метками”. Пусть для каждого терма t у нас определе- на его метка L(t) такая, что: • разные термы помечены разными метками: t1 ≠ t2 ⇒ L(t1) ≠ L(t2); • во время создании η-терма при переписывании метка новой копии должна не совпадать с уже существующими. Достаточно теперь определить мет- ки как явные компоненты η-термов и про- позициональных переменных и изменить определение структурной эквивалентности так, чтобы не принимать метки во внима- ние при сравнении η -термов. Пусть η-терм выглядит, как <L1, L2> η X.f → g\|h, а связанные переменные, как <L1, L2>vi. Метка состоит из двух час- тей: L1 – уникальный идентификатор для начального η-терма, который выделяется при создании начального множества тер- мов и L2 – переменная часть, которая из- меняется во время каждой подстановки. Тогда все, что нужно сделать для пере- формулирования η-исчисления – это изме- нить правило (ρ:match) так, что бы при подстановке инкрементировалась пере- менная часть меток переменных: ⎪ ⎪ ⎪ ⎩ ⎪⎪ ⎪ ⎨ ⎧ ¬ == =→ ),,(если ),( ;\|),(и \|),(если ]),[( )\|.(( 2 1 hfmatch hqapply hfmatchS hfmatch SqincrL qhgfvapply η где incrL каким-то образом изменяет метки переменных. Можно сказать, что использование ин- тенсионального равенства и уникального машинного представления эквивалентно явному процессу переименования пере- Теоретичні та методологічні основи програмування 7 менных. Использование меток для эмули- рования интенсионального равенства мо- жет быть использовано при реализации системы на платформах без доступа к вы- числению адресов (таким, например, как виртуальная машина JVM). 3. Комбинирование правил в упорядоченные множества правил Еще одним упрощением в языках, основанных на переписывающих прави- лах, является предположение, что вычис- лительный процесс не должен зависеть от порядка применения набора правил. Одна- ко в типичной программисткой практике чаще встречается другой тип рассуждений, сводящийся к выбору между частными случаями какого-то общего образца. Определим частичное упорядочи- вание на множестве правил по “степени конкретности” входящих образцов. То есть будем говорить, что t1<< t2, если t1 явля- ется “более конкретным”, чем t2. Для на- шего случая можем определить, что f << g, если ∀h.match(g,h)\|1 ⇒ match(f,h)\|1. Теперь пусть p = (fp → gp) и s = (fs → → gs) – два правила с пересекающимися образцами и fp << fs. Как правило, наличие в системе двух таких правил говорит о на- мерении сначала провести более частную проверку, а потом более общую. Тогда можно ввести правило вида fp → gp \| (fs → → gs\|id) (в традиционной интерпретации такие правила образуют неконфлюэнтную критическую пару [9]). Соответственно, комбинирование множества правил пере- писывания {p1,...,pN} сводится к разбиению этого множества правил на последователь- ность упорядоченных правил со взаимно- непересекающиеся образцами и построе- нию упорядоченного локально-конфлю- энтного терма внутри таких сегментов. Ес- тественно, построить отношения << не всегда возможно, что иллюстрируется сле- дующим примером: 1) η x,y: f(x,a(y)) → 1 2) η x,y: f(a(x),y) → 2 3) η x,y: f(x,y) → 3. Здесь невозможно построить упорядоче- ние образцов, так как редукция терма f(a(x),a(x)) неоднозначна и зависит от стра- тегии (или порядка) применения правил переписывания. Заметим, что неконфлюэнтность системы с упорядоченным множеством правил всегда может быть разрешена до- бавлением дополнительных разрешающих правил. То есть, если у нас есть система переписывающих правил r1,…,rN, дающая неоднозначный результат при переписы- вании, упорядоченном по степени конкре- тности, то мы можем построить систему правил r1,…,rN, rN+1,...,rN+K, включающую в себя первоначальную и в свою очередь конфлюэнтную. Действительно, если сис- тема неконфлюэнтна, значит найдутся два правила ri и rj, образующую критическую пару. Это означает, что ri и rj имеют об- щий унификатор образцов (пусть это бу- дет l: l << left(ri) и l << left(rj). Тогда мо- жем ввести новое правило rN+1= l→ x, ко- торое при упорядоченно-частном приме- нении будет всегда применяться перед ri или rj для образцов, образующих критиче- скую точку в r1,…,rN. Для того, чтобы x не вводил новых критических точек, доста- точно выбрать его совпадающим с каким- либо из уже существующих результатов подстановок правых частей ri или rj. Итого, получим новую систему, где ri и rj не яв- ляются более критической парой. Продол- жая этот процесс до полного исчерпания критических пар получаем конфлюэнтную систему. Так, вышеприведенном примере критическую пару составляют правила 1) и 2), общий унификатор образцов − η x,y: :f(a(x),a(y)). Следовательно, систему мож- но превратить в конфлюэнтную по отно- шению к упорядоченному переписыванию, добавив правило: η x,y: f(a(x),a(y)) → 1. Такое построение работает для сис- тем переписывания первого порядка. Для систем высших порядков дело обстоит не- сколько сложнее, так как редукция может образовывать критическую пару с собст- венной подстановкой, процесс определе- ния дополнительных правил тогда стано- вится бесконечным и фактически сводит- Теоретичні та методологічні основи програмування ся к определению порядка вычисления. Стандартный пример, который обычно ил- люстрирует неконфлюэнтность правил пе- реписывания второго порядка [2], в η- исчислении можно переписать как (η x.x a→ x) ((η y.y → y) a), или, в полной форме: apply(η x.apply(x,a) → x, apply((η y.y → y), a)). В работе [10] рассмотрены примеры ограничений вывода для получения ло- кальной конфлюэнтности систем высшего порядка, основанных на λ-исчислении (та- кие как линейность образцов). 4. Взаимодействие с внешней средой – получение и посыл- ка сигналов Теперь дополним конструкции по- строенного языка операциями взаимодей- ствия с внешней средой. В предыдущей версии системы Termware [7, 8] обмен ин- формацией с внешним миром осуществ- лялся с помощью установки значения сво- бодной переменной из процедурной части базы данных (БД) фактов. В настоящем подходе с использованием связующих пе- ременных естественно ввести специальные конструкции для получения и передачи информации. Будем представлять БД фак- тов как пару: • множество входных событий, ко- торое может быть представлено множест- вом функциональных символов или ато- мов Tin; • множество выходных действий Tout, также представленных функциональ- ными символами или атомами. Для учета передачи информации дополним наш язык θ-конструкциями, по- лучив множество термов Tηθ c помощью следующего рекурсивного определения. Выделим подмножества Tθin и Tθout сле- дующим образом: • любой η-терм входит в дополнен- ный язык: t∈Tη ⇒ t∈Tθin и t ∈ Tθout; • можно комплектовать входные и выходные функциональные термы: fin ∈ Tin, t1...tN ∈ Tθin ⇒ fin(t1,..tN) ∈ Tθin, fout ∈ Tout, t1...tN ∈ Tθout ⇒ fout(t1,..tN) ∈ Tθout; • можно связывать входные пере- менные с помощью θ-конструкций ввода: f∈Tθin, g∈TηS ∧ fv(g)={x} ⇒ θx←in f.g∈Tθin; • можно передавать информацию с помощью θ-конструкций вывода: f ∈ Tθout, g, h ∈ Tη ⇒ θg.f ←out h ∈ Tθout; • правило взаимодействия коррект- но, если в левой части находятся конст- рукции ввода, а в правой – конструкции вывода: f ∈ Tθin, g,h∈ Tθout ⇒ η(f → g\|h) ∈ ∈Tηθ. Операционная семантика таких правил может быть определена как прове- дение операций ввода при сопоставлении и вывода при подстановке. 5. Типизация η-исчисления Типизация построенного η-исчис- ления имеет целью улучшить свойства анализируемости формул исчисления и эффективности его реализации. Определе- ние правил вывода типов для η- конструкций, θ-конструкций и правил взаимодействия начинается с принятия сигнатуры типов для констант и функцио- нальных символов. Начнем со случая без взаимодействий: пусть имеем некоторую упорядоченно сортную сигнатуру (T, <, ∑) и требуется обогатить ее возможностью построения η-термов. Можно построить рекурсивно полиморфную структуру ти- пов, в точности следуя подходу, принято- му в [5], т. е. построив систему типов V=T+(V→V)+(V+V)+(V×V)+W путем пря- мой трансляции конструкций λ2μ∪ в кон- текст η-исчисления. Единственное изме- нение, которое надо будет внести в собст- венно исчисление – это типизация связан- ных переменных. Правила вывода тогда будут иметь следующий вид, где символ означает свойство выводимости: > 1) δ: δ: x x >Γ Γ∈ − начало; 8 Теоретичні та методологічні основи програмування 2) δ:),( :,δ: NMapply NM > >> Γ ϕΓ→ϕΓ − элиминация стрелки; 3) τδ→ϕ→ηΓ τΓϕΓϕΓ \|:\| :,:,: QNM QNM > >>> − внесение стрелки; 4) δΓϕΓ δ∩ϕΓ :,: : MM M >> > − элиминация ∩; 5) δ∩ϕΓ δΓϕΓ : :,: M MM > >> − внесение ∩; 6) δΓϕΓ δ×ϕΓ :)(,:)( : 21 MprojMproj M >> > − эли- минация ×; 7) δ×ϕΓ δΓϕΓ :),( :,: NMpair NM > >> − внесение ×. Теперь добавим к рассмотрению θ- конструкции, определив на них типиза- цию. Добавим указание типа к перемен- ным ввода и пусть для каждого входного события fin, совместимого со входной пе- ременной типа τ, имеется определенный идентификатор события Id(f). Будем обоз- начать такой факт как Id(f):τ. Введем специальный тип θin({Idi:ϕi},δ), содержащий в себе множе- ство входных событий и результирующий тип, с интерпретацией правила, которое воспринимает на входе событие с такими Id и выдает на выход результирующий терм типа δ. Также можем определить, что θin (∅,δ)=δ. Соответствующие правила конст- руирования и правила элиминации имеют вид: 1) )},:)(({:)( :)(,: ϕδθ←θΓ δΓϕΓ fIdMfx fIdM inin> >> − внесение θin; 2) )},:)(},:)(({: )),:)((,:)((: ϕτδθΓ ϕτθδθΓ gIdfIdM gIdfIdM in inin > > − секвенция θin; 3) ),(: : ϕ∅θΓ ϕΓ inM M > > − пустой сигнал; 4) ϕΓ ϕδθΓ : ),(: M M in > > − ослабление зависимо- сти; 5) ):)(,:,)(., ),:)((: δΓϕΓ←θ=∃ ϕδθΓ fIdNNfxMfN fIdM in in >> > − элиминация θin; 6) ))},:)((},:)((: ),:)(,:)((: ϕτθδθΓ ϕτδθΓ gIdfIdM gIdfIdM inin in > > − десеквенция θin. Точно также можно определить θout({Idi:ϕi},δ), содержащий в себе набор идентификаторов выходных событий и ввести аналогичные правила конструиро- вания. Например, правило вывода для вне- сения в формулу θout будет иметь вид: ),:)((:)( :)(,:,: ϕδθ←θΓ δΓδΓϕΓ fIdNfM fIdNM outout> >>> (ос- тальные правила полностью аналогичны соответствующим правилам для θin, по- этому здесь не приводятся). Отношение между θin-типами и ос- тальными можно записать покомпонентно (правила для θout – аналогичны): θin(A,ϕ) ∪ θin (B,τ) = θin (A∪B, ϕ ∪τ) θin (A, ϕ) ∩ θin (B, τ) = θin (A∩B, ϕ ∩τ) θin (A, ϕ) × θin (B, τ) = θin (A∪B, ϕ × τ) θin (A, ϕ→ τ) → θin (B, τ) = θin (A∪B, τ). Анализ типов взаимодействий мо- жет использоваться системой выполнения правил для определения корректности оп- тимизационных преобразований. Напри- мер, если система правил не включает в себя взаимодействия, то применение кэ- ширования промежуточных результатов 9 Теоретичні та методологічні основи програмування 10 (memoizing) не изменит семантику вычис- лений и может быть применено. Выводы Построенное исчисление описывает применения правил переписывания, при- годных к широкому спектру задач. Cопоставление η-исчисления и ρ- исчисления позволяет сделать вывод как об области применения, так и об архитек- туре разрабатываемых систем. Если в η- исчислении мы работаем с одним термом, который сопоставляется с правилами на основе выбранного порядка применение, то в ρ-исчислении система имеет дело сра- зу со множеством термов. И, таким обра- зом, структурный оператор ρ-исчисления позволяют применить сразу множество правил, при этом как в η-исчислении все время выбирается одно правило, на основе порядка и стратегии. Недетерминирован- ный выбор и спецификация результата в случае отказа изначально не были преду- смотрены в ρ-исчислении, но для этой це- ли существуют его расширения [4, 6]. Ин- тересно, что реализация обработки отказа также потребовала фиксации стратегии редукции методом call-by-value. Намного ближе в этом отношении находятся вариа- ции λ-исчисления с образцами [3, 9] и ис- числениями образцов [4]. В перспективе возможно построе- ние объединяющего формализма, включа- ющего в себя редукцию как одиночных термов, так и множеств так, что бы подо- бное исчисление в программировании, ос- нованном на правилах переписывания термов, заняло роль, подобную роли System F [11] в функциональном програм- мировании. Типизация правил взаимодействия в принципе не зависит от собственно η- исчисления и может быть применена к любому типизированному декларативному языку с побочными эффектами. В будущем планируется исследо- вать возможности ослабления требований к стратегии редукций [12] в отдельных об- ластях и встроить типизированное η- исчисление в следующую версию системы TermWare [13]. Дальнейшие исследования в данном направлении предполагают формулирова- ние дополнительных условий, обеспечи- вающих корректность преобразований, а также реализацию переписывающих пра- вил для проверки данных условий. Также возможна интеграция с системами для ав- томатического доказательства теорем, с целью более полной автоматизации про- цесса доказательства корректности. 1. C. de Oliveira Braga. Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics. Pontificia Universi- dade Catolica do Rio de Janeiro. 2001. 2. Cirstea H., Liquori L., Wack B. Rewriting calculus with fixpoints: Untyped and first- order systems. Vol. 3085, Springer, 2003. 3. Oostrom V. van. Lambda Calculus with Pat- terns. 1990. 4. Jay C.B. The pattern calculus. ACM Trans. Program. Lang. Syst. 2005.–Vol. 26, N 6. P. 911 – 937. 5. Abadi M., Pierce B., Plotkin G. Faithful Ideal Models for Recursive Polymorphic Types // International J. of Foundations of Computer Science. –1989. – Vol. 2. –P. 1 – 21. 6. Faure G., Kirchner C. Exceptions in the re- writing calculus / Proceedings of the RTA conference, Copenhagen, July 2002. – Lect. Notes in Comp. Sci. – Vol. 2378. – P. 66 – 82. 7. Doroshenko A., Shevchenko R. TermWare: A Rewriting Framework for Rule-Based Pro- gramming Dynamic Applications // Funda- menta Informaticae. – 2006. –Vol. 72, Issue 1-3. – P. 95 – 108. 8. Дорошенко А.Е., Шевченко Р.С. Система символьных вычислений для программи- рования динамических приложений // Проблеми програмування. – 2005. – №4. – С. 23 – 33. 9. Baader F. and Nipkow T. Term Rewriting and All That. Cambridge, England: Cambridge University Press, 1999. – 316 p. 10. Mayr R., Nipkow T. High Order Rewrite Sys- tems and their confluence. Theoretical Com- http://www.amazon.com/exec/obidos/ASIN/0521779200/ref=nosim/weisstein-20 http://www.amazon.com/exec/obidos/ASIN/0521779200/ref=nosim/weisstein-20 Теоретичні та методологічні основи програмування 11 puter Science. – 1998. – Vol. 192, Issue 1. – P. 3 – 29. 11. Girard J.-Y., Taylor P., Lafont Y. Proofs and Types, Cambridge University Press, 1989. – 183 p. 12. Visser E., A survey of rewriting strategies in program transformation systems, Proceedings of the Workshop on Reduction Strategies in Rewriting and Programming (B. Gram- lichand, S.L.Alba, eds.), 2001. 13. TermWare: http://www.gradsoft.ua Получено 03.03.2011 Об авторах: Шевченко Руслан Сергеевич, архитектор ПО, Дорошенко Анатолий Ефимович, доктор физико-математических наук, профессор, заведующий отделом теории компьютерных вычислений Института программных систем НАН Украины. Место работы авторов: ООО Gradsoft, e-mail: ruslan@shevchenko.kiev.ua Институт программных систем НАН Украины, 03680, Киев-187, Проспект Академика Глушкова, 40. тел.: (044) 526 3559. e-mail: dor@isofts.kiev.ua http://www.gradsoft.ua/ mailto:ruslan@shevchenko.kiev.ua mailto:dor@isofts.kiev.ua (-ИСЧИСЛЕНИЕ – РЕАЛИСТИЧНАЯ ФОРМАЛИЗАЦИЯ КЛАССА ПЕРЕПИСЫВАЮЩИХ СИСТЕМ Введение 1. Модель переписывающих систем 2. Интенсиональное равенство как замена переименования переменных 4. Взаимодействие с внешней средой – получение и посылка сигналов 5. Типизация (-исчисления Выводы

-calculus as a realistic formalization of a class of rewriting systems

Institution

Ähnliche Einträge