Axiomatic models and methods used to design of language translators

Application of logical methods and formal system theory methods used to design of language translators are considered. An analogue of a resolution method for elementary systems is proposed.

Збережено в:

Бібліографічні деталі
Дата:	2015
Автори:	Parasyuk, I.N., Provotar, O.I., Kondratenko, V.A.
Формат:	Стаття
Мова:	Ukrainian
Опубліковано:	PROBLEMS IN PROGRAMMING 2015
Теми:	UDC 681.3
Онлайн доступ:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/16
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Problems in programming
Завантажити файл:

Репозитарії

Problems in programming

id	pp_isofts_kiev_ua-article-16
record_format	ojs
resource_txt_mv	ppisoftskievua/b7/ca7caa0320d40580e84d19e64c25dfb7.pdf
spelling	pp_isofts_kiev_ua-article-162018-10-02T20:47:22Z Axiomatic models and methods used to design of language translators Аксиоматические модели и методы проектирования языковых трансляторов Аксіоматичні моделі та методи проектування мовних трансляторів Parasyuk, I.N. Provotar, O.I. Kondratenko, V.A. UDC 681.3 Application of logical methods and formal system theory methods used to design of language translators are considered. An analogue of a resolution method for elementary systems is proposed. Рассматриваются вопросы применения логических методов и методов теории формальных систем для построения языковых трансляторов. Предложен аналог метода резолюций для элементарных формальных систем. Розглядаються питання застосування логічних методів та методів формальних систем для побудови мовних трансляторів. Запропонований аналог методу резолюцій для елементарних формальних систем. PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2015-07-01 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/16 PROBLEMS IN PROGRAMMING; No 3 (2003) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 3 (2003) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 3 (2003) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/16/20 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2018-10-02T20:47:22Z
collection	OJS
language	Ukrainian
topic	UDC 681.3
spellingShingle	UDC 681.3 Parasyuk, I.N. Provotar, O.I. Kondratenko, V.A. Axiomatic models and methods used to design of language translators
topic_facet	UDC 681.3
format	Article
author	Parasyuk, I.N. Provotar, O.I. Kondratenko, V.A.
author_facet	Parasyuk, I.N. Provotar, O.I. Kondratenko, V.A.
author_sort	Parasyuk, I.N.
title	Axiomatic models and methods used to design of language translators
title_short	Axiomatic models and methods used to design of language translators
title_full	Axiomatic models and methods used to design of language translators
title_fullStr	Axiomatic models and methods used to design of language translators
title_full_unstemmed	Axiomatic models and methods used to design of language translators
title_sort	axiomatic models and methods used to design of language translators
title_alt	Аксиоматические модели и методы проектирования языковых трансляторов Аксіоматичні моделі та методи проектування мовних трансляторів
description	Application of logical methods and formal system theory methods used to design of language translators are considered. An analogue of a resolution method for elementary systems is proposed.
publisher	PROBLEMS IN PROGRAMMING
publishDate	2015
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/16
work_keys_str_mv	AT parasyukin axiomaticmodelsandmethodsusedtodesignoflanguagetranslators AT provotaroi axiomaticmodelsandmethodsusedtodesignoflanguagetranslators AT kondratenkova axiomaticmodelsandmethodsusedtodesignoflanguagetranslators AT parasyukin aksiomatičeskiemodeliimetodyproektirovaniââzykovyhtranslâtorov AT provotaroi aksiomatičeskiemodeliimetodyproektirovaniââzykovyhtranslâtorov AT kondratenkova aksiomatičeskiemodeliimetodyproektirovaniââzykovyhtranslâtorov AT parasyukin aksíomatičnímodelítametodiproektuvannâmovnihtranslâtorív AT provotaroi aksíomatičnímodelítametodiproektuvannâmovnihtranslâtorív AT kondratenkova aksíomatičnímodelítametodiproektuvannâmovnihtranslâtorív
first_indexed	2025-07-17T09:38:32Z
last_indexed	2025-07-17T09:38:32Z
_version_	1850409683560431616
fulltext	Теоретические и методологические основы программирования © И.Н. Парасюк, А.И. Провотар, В.А. Кондратенко, 2003 22 ISSN 1727-4907. Проблемы программирования. 2003. № 3 УДК 681.3 И.Н. Парасюк, А.И. Провотар, В.А. Кондратенко АКСИОМАТИЧЕСКИЕ МОДЕЛИ И МЕТОДЫ ПРОЕКТИРОВАНИЯ ЯЗЫКОВЫХ ТРАНСЛЯТОРОВ Рассматриваются вопросы применения логических методов и методов теории формальных систем для построения языковых трансляторов. Предложен аналог мето- да резолюций для элементарных формальных систем. Введение Теория языковых трансляторов на сегодняшний день хорошо развита и нашла свое применение в многочис- ленных приложениях. Стержневой идеей ставших классическими методов построения трансляторов является описание языковых конструкций фор- мальными грамматиками или автома- тами различной сложности для реше- ния проблем синтаксического анализа, перевода и компиляции. При этом со- ответствующие методы для каждой па- ры языков, вообще говоря, не будут универсальными, что делает их техно- логически трудоемкими (за исключе- нием, быть может, случаев синтаксиче- ски управляемых трансляций). Актуальность проблемы разра- ботки технологически и функциональ- но эффективных методов автоматиза- ции программирования В.М. Глушков убедительно продемонстрировал еще в 1959 г. [1] при обсуждении новых принципов построения программирую- щих программ. Уместно отметить, что результаты этой работы были успешно применены в ряде проектов, в частно- сти при построении семейства семан- тически управляемых автоматизиро- ванных систем обработки данных [2]. В настоящей статье предлагается подход к проектированию языковых трансляторов, который основан на ло- гическом описании языков [3] и исполь- зовании универсальной составляющей различных этапов трансляции – методе резолюций [4]. В частности, представ- лен метод построения вывода из акси- ом элементарных формальных систем (ЭФС) – аналог метода резолюций, формулами ЭФС описаны этапы син- таксического анализа и перевода. Применение подхода иллюстрируется на различных типах грамматик и син- таксически управляемых переводов, описанных формулами логики преди- катов первого порядка [5]. Транслирующие грамматики Транслирующей грамматикой или грамматикой перевода, как извест- но, называется контекстно-свободная грамматика, множество терминальных символов которой разбито на множе- ство входных символов и множество символов действия. А цепочки языка, определяемого транслирующей грам- матикой, называются последовательно- стями актов. Процесс получения трансли- рующей грамматики продемонстриру- ем на простом модельном примере. Допустим, нужно построить про- цессор, получающий в качестве входа инфиксное выражение и печатающий на выходе эквивалентное выражение в постфиксной польской записи. Кроме того, мы хотим, чтобы проектирование этого процессора основывалось на распознавателе, который каждый раз, когда распознан символ, вызывал про- цедуру печати и инициировал ее. Грамматика G0 для инфиксных выражений с начальным нетерминаль- ным символом <E> будет иметь сле- дующий вид: 1. <E> => <E> + <T>. 2. <E> => <T>. 3. <T> => <T><P>. 4. <T> => <P>. 5. <P> => (<E>). 6. <P> => a. 7. <P> => b. 8. <P> => c. Теоретические и методологические основы программирования 23 Для удобства изложенная грам- матика содержит 3 конкретных имени констант a, b, c. Чтобы построить грамматику для последовательностей актов, опишем действия, соответст- вующие каждой правой части правил грамматики. Например, чтобы напеча- тать a после того, как оно прочитано, правило 6 заменяется на P => a{a}. Чтобы напечатать знак + после того, как напечатаны оба его операнда, пра- вило 1 заменяется на <E> => <E> + + <T>{+}. Новое правило 1 содержа- тельно состоит в следующем: обработ- ка нетерминала <E> включает обра- ботку нетерминала <E>, чтение опера- ции +, обработку нетерминала <T> и печать операции +. После аналогичных изменений в других правилах, новая грамматика примет следующий вид: 1. <E> => <E> + <T>{+}. 2. <E> => <T>. 3. <T> => <T><P>{}. 4. <T> => <P>. 5. <P> => (<E>). 6. <P> => a{a}. 7. <P> => b{b}. 8. <P> => c{c}. Полученная новая грамматика и будет транслирующей грамматикой или грамматикой перевода. Синтаксически управляемые переводы Грамматику, транслирующую в цепочки, можно интерпретировать как способ описания перевода со входного языка на выходной. По сути, такие пе- реводы управляются грамматикой и называются синтаксически управляе- мыми переводами (СУ-переводами) [6]. Пусть Σ и ∆ – два алфавита и T ⊆ Σ × ∆* – произвольное отношение на паре языков L ⊆ Σ, l ⊆ ∆ ( L – об- ласть определения, а l – множество значений отношения). Отношение T ⊆ Σ* × ∆* называет- ся отношением СУ-перевода, если оно формально представимо [7]. Формально представимое отно- шение T ⊆ Σ×∆ на паре языков L ⊆ Σ, l ⊆ ∆ называется отношением транс- ляции, если область определения его разрешима. Рассмотрим схему перевода, ото- бражающую арифметические выраже- ния языка L(G0) в постфиксные поль- ские записи. Такая схема представля- ется правилами грамматики G0 и соот- ветствующими элементами перевода G1 как показано ниже: 1. <E> => <E> + <T>; <E> => <E><T>+. 2. <E> => <T>; <E> => <T>. 3. <T> => <T><P>; <T> => <T><P>. 4. <T> => <P>; <T> => <P>. 5. <P> => (<E>); <P> => <E>. 6. <P> => a; <P> => a. 7. <P> => b; <P> => b. 8. <P> => c; <P> => c. Схемы определяют отношения между цепочками, порождаемыми грам- матиками G0 и G1 соответственно. Для этого необходимо найти вывод цепочки в грамматике G0 и сопоставить его с вы- водом в грамматике перевода G1. На- пример, цепочке a+bc будет соответст- вовать цепочка abc+, так как сущест- вует вывод пары (a+bc, abc+) вида (<E>, <E>) ⇒ (<E>+<T>, <E><T>+) ⇒ ⇒ (<T>+<T>, <T><T>+) ⇒ ⇒ (<P>+<T>, <P><T>+) ⇒ ⇒ (a+<T>, a<T>+) ⇒ ⇒ (a+<T><P>, a<T><P>+) ⇒ ⇒ (a+<P><P>, a<P><P>+) ⇒ ⇒ (a+b<P>, ab<P>+) ⇒ (a+bc, abc+). Схемой СУ-перевода есть пятер- ка T = (N, Σ, ∆, R, S), где N – множество нетерминальных символов; Σ, ∆ – соответственно входной и выходной алфавиты; R – конечное множество правил вида A → α, β, где α ∈ (N ∪ Σ), β ∈ (N ∪ ∪ ∆) и вхождения нетерминалов в це- Теоретические и методологические основы программирования 24 почку β образуют перестановку вхож- дений нетерминалов в цепочку α; S – начальный нетерминал из N. Переводом, определяемым схе- мой Т, служит множество пар {(x, y)(S,S) ⇒* (x, y), x∈Σ* и y ∈ ∆}. Схема СУ-перевода будет про- стой, если для каждого правила A → α, β из R соответствующие друг другу вхождения нетерминалов встречаются в одном и том же порядке. Переводы, определяемые про- стыми СУ-схемами, образуют важный класс переводов, потому что их техно- логически легко реализовать преобра- зователями с магазинной памятью. В частности, такие преобразователи по- лучаются из автоматов с магазинной памятью, если их снабдить выходом и разрешить на каждом такте выдавать выходную цепочку конечной длины. Легко показать, что справедлива Теорема 1. СУ-перевод Т простой тогда и только тогда, когда Т = τ(P) для некоторого МП-преобразователя Р. Таким образом, построение транслятора, реализующего перевод, сводится к программному моделирова- нию преобразователя с магазинной памятью. Более совершенны атрибутные транслирующие грамматики [8], иначе называемые контекстно-зависимыми. Они сохраняют в неизменном виде все преимущества КС-грамматик и в то же время снабжены специальными сред- ствами описания нетерминальных сим- волов и символов действия в этих грамматиках, с помощью которых эти компоненты обеспечиваются необхо- димыми сведениями для корректной трансляции языков программирования. В качестве специальных средств опи- сания выступают атрибуты – синтези- руемые и наследуемые [6]. Т.е. в АТГ существует возможность сопровождать каждый из нетерминальных символов и символов действия неограниченным количеством атрибутов, выражающих те или иные свойства терминальных символов, которые подставляются вме- сто указанных нетерминалов. Именно эти атрибуты обеспечивают возмож- ность порождения корректных фраз (в синтаксическом смысле) в естествен- ных языках, а также возможность обеспечения операндов необходимыми адресами в языках программирования. Резолютивный вывод для реализации синтаксически управляемых переводов Суть этого подхода состоит в следующем. После того как правила транслирующей грамматики преобра- зованы в правила логики предикатов, необходимо ввести дополнительные, обусловливающие порядок (стратегию) применения резолютивного вывода для доказательства истинности полученной формулы. Под порядком применения резолютивного вывода подразумевает- ся очередность расположения дизъ- юнктов, принадлежащих логической модели, в итоговом списке дизъюнктов S этой модели. От этой очередности зависит эффективность доказательства теоремы. Исследования этой проблемы показали, что наиболее эффективным доказательство становится в случае, когда порядок резолютивного вывода совпадает с порядком вывода иссле- дуемой цепочки языка при ее распо- знавании в определенной грамматике. Иными словами, когда осуществляется распознавание только с помощью ле- вого посимвольного вывода заданной цепочки в этой грамматике путем под- становок начиная с символа S и под- становок, соответствующих правилам рассматриваемой грамматики, вплоть до получения целевой цепочки. Реализация универсального тран- слятора в любой Prolog-системе [6] осуществляется путем построения сис- тем логических аксиом, соответствую- щих правилам грамматик входного и выходного языков, и последующим преобразованием аксиом – приведе- нием их к виду, удобному для приме- нения правила резолюций. Покажем, что справедлива сле- дующая теорема. Теорема 2. Для каждой грамма- тики G существует формальная систе- Теоретические и методологические основы программирования 25 ма (Е), содержащая предикат, пред- ставляющий язык L(G). Доказательство. Проведем дока- зательство для случая регулярных и КС-грамматик. Пусть G = (K, V, σ, P) – регулярная грамматика. Каждому не- терминалу θ ∈ V грамматики G ставим в соответствие предикатный символ θ′ так, что различным нетерминальным символам алфавита V соответствуют различные предикатные символы. Пусть V′ = {θ′ / θ ∈ V} – полученное множество предикатных символов. По- строим формальную систему (Е), ак- сиомы которой строятся по продукци- ям грамматики G следующим образом: продукцию вида θ → a заменяем на аксиому θ′a, продукцию θ → ϕa заме- няем аксиомой ϕ′x → θ′ax, продукцию θ → θa – аксиомой θ′x → θ′ax, где ϕ, θ – произвольные нетерминальные символы; а – терминальный символ грамматики G; х – переменная. Пусть z – произвольная цепочка, выводимая в G. Полный вывод цепочки z можно представить в виде σ ⇒ ψ1t1 ⇒ ψ2t2 ⇒ … ⇒ ψntn ⇒ z, где ψi – нетерминальные символы; ti – цепочки терминальных символов. Этому выводу соответствует последо- вательность продукций грамматики G σ → ψ1v1, ψ1 → ψ2v2, …, ψn-1 → → ψnvn, ψn → vn+1, причем t1 = v1, t2 = v1v2 … tn = v1v2 … vn, z = v1v2 … vn+1. Заменив каждую продук- цию этой последовательности согласно указанным выше преобразованиям, получим последовательность аксиом системы (Е) ψ1′x → σ′v1x, ψ2′x → ψ1′v2x, …, ψn′x → → ψn-1′vnx, ψn′vn+1. Тогда полный вывод цепочки z в (Е) можно представить в виде ψn′vn+1 ≡> ψn-1vnvn+1 ≡> … ≡> ψ2′v3 … vn+1 ≡> ≡> ψ1′v2 … vn+1 ≡> σ′v1 … vn+1. Таким образом, предикат σ′ представляет язык L(G). Пусть G = (K, V, σ, P) – произ- вольная КС-грамматика. Преобразуем ее к виду в нормальной форме Хом- ского. Тогда продукции грамматики будут иметь один из следующих видов: θ → ϕψ, θ → a. Как и в случае регулярных грам- матик, каждому нетерминалу θ сопос- тавим различные предикатные симво- лы. Пусть V′ = {θ′ / θ ∈ V} – полученное множество предикатных символов. По- строим формальную систему (Е), схема Р′ которой строится по схеме Р грам- матики G следующим образом: про- дукцию вида θ → a заменяем аксиомой θ′a, продукцию θ → ϕψ – аксиомой ϕ′x → ψ′y → θ′xy, где ϕ, θ, ψ – произ- вольные нетерминальные символы; а – терминальный символ грамматики G; x, y – переменные. Пусть z – произвольная цепочка, выводимая в G. Полный вывод цепочки z можно представить в виде σ ⇒ ϕ1ϕ2 ⇒ ϕ1ψ2ψ3 ⇒ … ⇒ ϕ1ψ2 ... θn ⇒ ⇒ ϕ1ψ2 … tn ⇒ … ⇒ t1t2 … tn = z, где ϕi, ψi, …, θi – нетерминальные сим- волы, ti – терминальные символы. Этому выводу соответствует последо- вательность продукций грамматики G σ → ϕ1ϕ2, ϕ2 → ψ2ψ3, …, γn-1 → θn-1θn, θn → → tn, θn-1 → tn-1, …,ϕ1 → t1. Заменив каждую продукцию этой последовательности согласно ука- занным выше преобразованиям, полу- чим последовательность аксиом систе- мы (Е) ϕ1′ → ϕ2′ → σ′xy, ψ2′x → ψ3′y → ϕ2′xy, …, θn-1′x → θn′y → γn-1′xy, θn′tn, …, ϕ1′t1. Тогда полный вывод цепочки z в системе (Е) можно представить в виде θn′tn ≡> γn-1′ ≡> … ≡> ϕ2′t2 … tn ≡> σ′t1t2 … tn. Таким образом, предикат σ′ представляет язык L(G). Теорема дока- зана. Теоретические и методологические основы программирования 26 На основании доказанной тео- ремы можно произвольную граммати- ку преобразовать в систему логиче- ских аксиом. Это, в частности, отно- сится и к СУ-переводам – формаль- ным моделям трансляторов, опреде- ляемых парой грамматик – входного языка и перевода. Например, КС-грамматика с сис- темой продукций σ → ab, σ → aσb мо- жет быть преобразована в формальную систему с аксиомами σ'ab, σ'x → σ'axb. СУ-перевод, реализующий отношение между арифметическими выражения- ми в алфавите {a, b, c} и их постфикс- ными записями может быть преобра- зован в формальную систему (E), со- держащую логические аксиомы вида 1. Pa,a. 2. Pb,b. 3. Pc,c. 4. Ex,y → Px,(y). 5. Px,y → Tx,y. 6. Tx,y → Pt,z → Tx∗t, xz∗. 7. Tx,y → Ex,y. 8. Ex,y → Tt,z→ Ex+t, yz+. Покажем, что в этой формальной системе существует вывод пары (a+bc, abc+). Действительно, имеем 9. Tb, b (правило заключения 2, 5). 10. Tb,b → Pc,c → Tbc,bc* (аксиома 6). 11. Pc,c → Tbc, bc (правило заключения 9, 10). 12. Tbc,bc (правило заключения 3, 11). 13. Ta,a (правило заключения 1, 5). 14. Ea,a (правило заключения 7, 13). 15. Ea,a → Tbc, bc → Ea +bc, abc+ (аксиома 8). 16. Tbc,bc → Ea +bc, abc+ (правило заключения 14, 15). 17. Ea +bc, abc+ (правило заключения 12, 16). Далее осуществляется преобра- зование аксиом формальных систем в множество дизъюнктов по правилу α → β = ¬α ∨ β. Преобразованная сис- тема (Е) будет иметь вид 1. Pa,a. 2. Pb,b. 3. Pc,c. 4. ¬Ex,y ∨ Px,(y). 5. ¬Px,y ∨ Tx,y. 6. ¬Tx,y ∨ ¬Pt,z ∨ Tx∗t, xz∗. 7. ¬Tx,y ∨ Ex,y. 8. ¬Ex,y ∨ ¬Tt,z ∨ Ex+t, yz+. Если аксиомы системы представ- лены в таком виде, то для доказатель- ства выводимости пар цепочек входно- го и выходного языков можно приме- нять метод резолюций. Покажем, на- пример, что в полученной формальной системе существует вывод пары (a+bc, abc+). Для этого добавим к имеюще- муся множеству дизъюнктов 9. ¬ E a+bc, abc+ и построим следующий вывод 10. ¬Pb,b ∨ Tb,b (аксиома 5). 11. Тb,b (правило резолюций 2, 10). 12. ¬Tb,b ∨ ¬Pc,c ∨ Tb∗c, bc∗ (аксиома 6). 13. ¬Pc,c ∨ Tb∗c, bc∗ (правило резолюций 11, 12). 14. Tb∗c, bc∗ (правило резолюций 3, 13). 15. ¬Pa,a ∨ Ta,a (аксиома 5). 16. Ta,a (правило резолюций 1, 15). 17. ¬Ta,a ∨ Ea,a (аксиома 7). 18. Ea,a (правило резолюций 16, 17). 19. ¬Ea,a ∨ ¬Tbc,bc ∨ Ea+bc, abc+ (аксиома 8). 20. ¬Tbc,bc ∨ Ea+bc, abc+ (правило резолюций 18, 19). 21. Ea+bc, abc+ (правило резолюций 14, 20). 22. (правило резолюций 9, 21). Вывод пустого дизъюнкта озна- чает, что пара (a+bc, abc+) принадле- жит СУ-переводу. Теоретические и методологические основы программирования 27 Пусть Σ и ∆ – два алфавита. Го- моморфизмом называется любое ото- бражение h: Σ → ∆*. Язык L характеризует отношение T, если существуют такие два гомо- морфизма h1 и h2, что T = {(h1(x), h2(x)) / x∈ L}. Теорема 3. Если отношение T ха- рактеризуется языком L, то T – CУ- перевод. Доказательство. Отношение го- моморфизма формально представимо. Это следует из аксиом Ee, e; Ea1, h(a1); Ea2, h(a2); . . . . . . . . . Ean, h(an). Кроме того, T = {(h1(x), h2(x)) / x∈ L} и отношения y1 = h1(x), y2 = h2(x) предста- вимы предикатами H1 и H2 соответст- венно в формальных системах (E1) и (E2). Добавив к аксиомам этих систем Lx → H1x,y1 → H2x,y2 → Ty1,y2, получим формальную систему, в кото- рой предикатом Т представляется от- ношение Т. Теорема доказана. Пусть К – алфавит из m симво- лов a1, a2, …, am; T – СУ-перевод на па- ре языков L, l. Теорема 4. Если L и l – разре- шимые языки над алфавитом К, то СУ- перевод T разрешим. Доказательство. Пусть Т – пре- дикат, представляющий отношение Т; L′ и l′ – предикаты, представляющие дополнения языков L и l соответствен- но; L и l – предикаты, представляю- щие собственно языки. Отношение “x непосредственно следует за y” в лексикографическом упорядочении представляется посред- ством предиката S в формальной сис- теме, аксиомами которой являются 1. Sαa1, αa2. 2. Sαa2, αa3. . . . . . . . . . . . . 3. Sαam-1, αam. 4. Sam, a1a1. 5. Sx,y → Sxam,ya1. Добавим к этим аксиомам сле- дующие: 6. Sx,y → Qy,x. 7. Qx,y → Qy,z → Qx,z. Тогда Q представляет отношение “x < y”. Добавим 8. Qx,y → Dx,y. 9. Qy,x → Dx,y. Тогда предикат D представляет отношение “x ≠ y”. Добавим к этим ак- сиомам следующие 10. l′y → T′x,y. 11. L′x → T′x,y. 12. Lx → ly → Tx,z → Dy,z → T′x,y. Получим формальную систему, в которой предикат T′ представляет от- ношение T′. Теорема доказана. Доказанные теоремы — обосно- вание примененимости метода резо- люций для построения лингвистиче- ских трансляторов. Метод резолюций в случае ло- гики предикатов, вообще говоря, не заканчивает свою работу. Поэтому на входной и выходной языки должны быть наложены некоторые ограниче- ния, а именно: разрешимость входно- го языка, которая обеспечивает за- вершенность фазы синтаксического анализа, и формальная представи- мость отношения на языках, которая обеспечивает завершенность фазы перевода. Эти условия выполняются в слу- чае разрешимости отношения СУ- перевода. Но алгоритм трансляции, с учетом дополнительных условий, мо- жет быть описан другими предикатами в системах логического программиро- вания. Теоретические и методологические основы программирования 28 Выводы Показана возможность примене- ния логических формализмов различ- ных типов для реализации синтаксиче- ских анализаторов и перевода. Опи- санные результаты, по мнению авто- ров, — это лишь первые шаги в теоре- тических исследованиях на пути при- менения аксиоматического похода к построению языковых трансляторов. Основную роботу – формирование соответствующих методологических и технологических основ новой инфор- мационной технологии – еще пред- стоит сделать. Это направление иссле- дований актуальное, перспективное и многообещающее. 1. Глушков В.М. Об одном методе автоматиза- ции программирования // Пробл. киберне- тики. – №2. – С.181—184. 2. Парасюк И.Н., Сергиенко И.В. Пакеты про- грамм анализа данных: технология разра- ботки. – М: Финансы и статистика, 1988. – 160 с. 3. Bratko I. Prolog Programming for Artificial Intelligence: Addison Wesley, M.A., 1986. – 560 с. 4. Чень Ч., Ли Р. Математическая логика и ав- томатическое доказательство теорем. – М: Наука, 1983. – 360 с. 5. Тей А., Грибомон П., Яцы Ж. Логический подход к искусственному интеллекту – М: Мир, 1990. – 430 с. 6. Ахо А., Ульман Дж. Теория синтаксического анализа, перевода и компиляции. – М: Мир, 1978. – Т.1. – 612с. 7. Р. Смальян. Теорія формальних систем. – М: Наука, 1981. — 208с. 8. Семантика языков программирования / Под ред. В.М. Курочкина. – М: Мир, 1980. – 396 с. 9. Lewis P.M., Rozenkrantz D.J., Stearns R.E. At- tributed Translation. General Electric Com- pany, Research and Development Center, New York 12345, Received August 30, 1973 // J. of Computer and System Sciences. 1974. – 9, N.3, Dec. – 142 p. Получено 04.09.03 Об авторах Парасюк Иван Николаевич, член-корреспондент НАНУ, доктор техн. наук, профессор, заведующий от- делом Провотар Александр Иванович, доктор физ.-мат. наук, профессор, заве- дующий кафедрой НУ им. Т. Шевченко. Кондратенко Виктория Александровна, канд. физ.-мат. наук, ведущий инженер- программист Место работы авторов: Институт кибернетики им. В.М. Глушкова НАН Украины, просп. Академика Глушкова, 40, Киев-187, 03680, Украина Тел. 266 0458

Axiomatic models and methods used to design of language translators

Репозитарії

Схожі ресурси