Аксіоматичні моделі і методи проектування лінгвістичних трансляторів

Размещено на http://www.allbest.ru/

Національна академія наук України

Інститут кібернетики імени В.М. Глушкова

На правах рукопису

УДК 681.3

АКСІОМАТИЧНІ МОДЕЛІ І МЕТОДИ

ПРОЕКТУВАННЯ ЛІНГВІСТИЧНИХ ТРАНСЛЯТОРІВ

01.05.03 - математичне та програмне забезпечення

обчислювальних машин і систем

Автореферат дисертації на здобуття наукового ступеня

кандидата фізико-математичних наук

КОНДРАТЕНКО Вікторія Олександрівна

Київ-2001

Дисертацією є рукопис.

Роботу виконано в Інституті кібернетики імені В.М. Глушкова НАН України.

Науковий керівник: доктор фізико-математичних наук, професор

ПРОВОТАР Олександр Іванович, Київський

Державний лінгвістичний університет,

завідувач кафедри інформатики.

Офіційні опоненти: доктор фізико-математичних наук, професор

ВЕЛЬБИЦЬКИЙ Ігор Вячеславович,

Міжнародний науковий центр технології програмування

ТЕХНОСОФТ НАН України, директор.

кандидат фізико-математичних наук, доцент

ШКІЛЬНЯКСтепан Степанович,

Київський національний університет імені Тараса Шевченка

Провідна установа: Інститут програмних систем НАН України.

Захист відбудеться 25.05.2001 р. о 14 годині на засіданні спеціалізованої вченої ради Д26.194.02 при Інституті кібернетики імені В.М. Глушкова НАН України за адресою:

03680 МСП Київ 187, проспект Академіка Глушкова, 40.

З дисертацією можна ознайомитися в науково-технічному архіві інституту.

Автореферат розісланий 23.04.2001 р.

Учений секретар

спеціалізованої вченої ради СИНЯВСЬКИЙ В.Ф.

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Як відомо, традиційні методології проектування лінгвістичних трансляторів, тобто таких, що орієнтовані на роботу з компонентами природних мов, ґрунтуються на граматичних моделях останніх і побудові спеціалізованих стекових автоматів для граматичного аналізу (розпізнавання) виразів вхідної мови й породження (генерації) синтаксично (але не семантично) адекватних виразів вихідної мови. Недоліки такого підходу полягають в тому, що для кожної пари мов необхідний свій спеціалізований автомат, трудозатрати на створення якого обчислюються людино-роками навіть для алгоритмічних мов середньої складності.

Крім того, переклади лінгвістичних текстів, виконані такими трансляторами, як правило, є досить абсурдними - до невпізнанності спотворюють зміст тексту. Пояснюється це тим, що транслятори-перекладачі ґрунтуються на концепції синтаксично керованої трансляції, всупереч необхідної - семантично керованої трансляції.

Дослідженню цих актуальних теоретичних і практичних проблем, пов'язаних зі створенням і реалізацією ефективних лінгвістичних трансляторів, присвячена дисертаційна робота.

Зазначимо, що запропонований в дисертації підхід до проектування лінгвістичних трансляторів, в основі якого лежать методи штучного інтелекту, став можливим завдяки теоретичному й практичному доробку як закордонних (М. Девіс, П. Гілмор, Х. Патнем, Дж. Робінсон, Новіков П. С., Поспєлов Г. С.) так і вітчизняних учених (Сергієнко І.В., Редько В.Н., Андон П.І., Скурихін В.І., Капітонова Ю. В., Летичевський О. А.).

Мета работи. Мета дисертаційної роботи полягає в розробці й реалізації аксіоматичних моделей проектування лінгвістичних трансляторів, що дозволить значно скоротити трудозатрати на розробку останніх.

Для досягнення поставленої мети в роботі розв'язувалися наступні задачі:

- аналіз формальних моделей і методів проектування лінгвістичних трансляторів;

- розробка правил еквівалентних перетворень продукцій контекстно-вільних (КВГ) і атрибутних транслюючи граматик (КЗГ) у правила логіки предикатів;

- розробка алгоритму трансляції на основі резолютивного виведення;

- побудова й дослідження абстрактних моделей логічних числень;

- реалізація моделей і методів проектування лінгвістичних трансляторів.

Наукова новизна. В дисертації одержані наступні нові результати:

- запропонований аксіоматичний підхід до проектування лінгвістичних трансляторів;

- розроблені алгоритми трансформації аксіоматичних моделей трансляції в правила логіки предикатів;

- розроблені алгоритми розпізнавання ланцюжків формальної мови та реалізації синтаксично-керованих переведень, що грунтуються на резолютивному виведенні;

- доведено ряд теорем для абстрактних моделей логічних числень;

- побудовані узагальнені конструкції алгоритму уніфікації й методу резо-люцій;

- реалізовані основні компоненти мови GIPLANG в системі програмування Arity Prolog.

Практична цінність. Дисертаційна робота виконувалася в Інституті кібер-нетики ім. В.М. Глушкова НАН України у відповідності з планами науково-технічних робіт за такими темами: “Розробка та обгрунтування основ процедурно-об'єктного макромодульного програмування та відповідних ефективних інструментальних засобів створення прикладних програмних систем на ПЕОМ для різних інтегрованих середовищ та застосувань” (В.Ф.155.01), “Створення комп'ютерних систем методами макромодульного програмування (М.Н.155. 02).

Запропонований і розроблений аксіоматичний підхід може бути використаний як складовий елемент методології побудови лінгвістичних трансляторів у системах логічного програмування. Створене програмне забезпечення впроваджене в ряді організацій Держбуду України для побудови трансляторів вхідних мов програмних комплексів автоматизованого проектування будівельних конструкцій та внутрішніх і зовнішніх мереж водо- та теплопостачання.

Апробація. Основні результати дисертаційної роботи доповідалися й обговорювалися на XIX і XX Міжнародних науково-технічних конференціях "Проблемы физической и биомедицинской электроники" (Київ, 1999-2000), Республіканському семінарі "Оптимизация вычислений" (Київ, 1986), семінарах наукової ради НАН України з проблеми “Кібернетика” (Київ, 1985-2000), конференціях молодих учених і спеціалістів Інституту кібернетики і Національного технічного університету "КПІ".

Публікації. За темою дисертації опубліковано 8 робіт.

Структура й обсяг дисертації. Дисертація складається із вступу, чотирьох розділів, висновку, списку літератури (81 найменування). Загальний обсяг роботи 130 сторінок.

ЗМІСТ РОБОТИ

У першому розділі дисертації викладені основні конструкції та поняття логічних систем, які використовуються впродовж усієї роботи. Зокрема, мова йде про традиційні логічні системи, якими є числення висловлювань та числення предикатів, а також розглядаються деякі особливості використання методу резолюцій в цих логічних системах. Крім того, в розділі розглядається задача архітектурного проектування комп'ютерів і методи її розв'язання.

Нехай задана множина комп'ютерів С = {c1, с2,..., сN}; множина архітектурних типів комп'ютерів А = {a1, a2,..., аm}; множина рівнів функціональної повноти комп'ютерів F = {f1, f2,..., fd}; множина тривалостей виконання процесорних команд В = {b1, b2,..., bh}; множина типів команд Т = {t1, t2,..., tg}; множина споживчих вартостей комп'ютерів S = {s1, s2,..., sq} та предикати: Т(ci, aj) - < комп'ютер сi належить до архітектурного типу aj>; Ф (ci, fk) - < комп'ютер сi має функціональну повноту рівня fk>; Р (сi, tx, uy, uz, bw) - <тривалість виконання комп'ютером ci процесорної команди типу tx, перший операнд якої розміщений в рівні пам'яті uy, а другий - в рівні пам'яті uz, складає bw періодів тактової частоти>; S (ci, se) - <споживча вартість комп'ютера сi дорівнює se>; VIG (ci, aj, fk, tx, uy, uz, bw, se) - < комп'ютер сi має архітектурний тип aj, функ-ціональну повноту fk, тривалість виконання команди tx-типу, перший операнд якої розміщений в рівні пам'яті uy, другий операнд - в рівні памяті uz, рівну bw і споживчу вартість, рівну se>. Тоді математична модель задачі вибору комп'ютера необхідної якості задається формулою

($aj)($fk)($bw)($se)($tx)($uy)($uz)($ci) (VIG(ci, aj, fk, tx, uy, uz, bw, se) Ю

Ю (T(ci, aj) Щ F(ci, fk) Щ R(ci, tx, uy, uz, bw) Щ S(ci, se))).

Така модель дозволяє розв'язувати задачі про вартість комп'ютерів, їх архітектурний тип, функціональну повноту і т. д., використовуючи метод резолютивного виведення.

У другому розділі розглядаються загальні питання компіляції та формалізмі, які при цьому використовуються.

У параграфі 2.1 наводиться спрощена структура компілятора, який складається з трьох блоків - лексичного, синтаксичного, генератора кодів та робочих таблиць компілятора. При цьому лексичний блок призначений для розбиття речення на лексеми. Синтаксичний блок переводить послідовність лексем в іншу послідовність, яка більш точно відображає порядок, в якому повинні виконуватися операції в програмі. Генератор коду “розвертає” атоми, побудовані синтаксичним блоком, в послідовність команд процесора, які виконують відповідні дії. І, нарешті, робочі таблиці компілятора містять дані, які використовуються при роботі його блоків.

У зв'язку з тим, що в теорії проектування трансляторів показано, що будь-який з архітектурних блоків компілятора може бути реалізований на основі формальних граматик, у параграфі 2.2 наводиться визначення формальної граматики як четвірки

G = (V, T, P, S),

де V - скінченна множина структурних елементів мови (нетермінальних символів); T - скінченна множина лексем мови (термінальних символів); P - скінченна множина правил (продукцій) взаємозв'язку як між елементами множини V, так і між структурними елементами й лексемами; S - початковий нетермінальний символ, з якого починається виведення допустимих фраз у цій граматиці.

Розпізнавання виразів мови, що породжується такою граматикою, відбувається за допомогою виведення заданих виразів у граматиці шляхом підстановок, починаючи з символа S. При цьому використовуються виключно ліві або праві виведення, так як вони дуже зручні для систематичної обробки і для кожного виведення існує єдине ліве або єдине праве виведення.

Будемо говорити, що пара фігурних дужок і символ в них, тобто вираз виду {a}, утворюють єдиний символ - символ дії. Нехай символи дій розглядаються як імена процедур, які друкують вхідні символи. Тоді транслююча граматика переведення інфіксних арифметичних виразів в еквівалентні арифметичні вирази в постфіксній польскій формі запису буде мати вигляд

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}.

Визначення. Транслюючою граматикою або граматикою переведення називається контекстно вільна граматика, множина термінальних символів якої поділена на множину вхідних символів і множину символів дії.

У параграфі 2.3 визначається поняття синтаксично керованих переведень (СК-переведень) стосовно транслюючих граматик. Такі переведення утворю-ються з виразів вхідної мови та виразів із символів дії. Вхідна мова породжу-ється вхідною граматикою, яку одержують із транслюючої граматики шляхом вилучення з її продукцій символів дії. Вирази із символів дії - це синоніми постфіксних польських форм запису, що відповідають інфіксним арифметичним виразам вхідної мови. Такому синтаксично керованому переведенню, яке визначається транслюючою граматикою, належить, наприклад, пара <a+b*c, {a}{b}{c}{*} {+} >.

Нехай S і D - два алфавіти і T Н S* ґ D* - довільне відношення на парі мов L Н S*, l Н D* ( L - область визначення, а l - множина значень відношення).

Визначення. Схемою СК-переведення називається п'ятірка U = (N, S, D, R, S), де N - множина нетермінальних символів; S - вхідний алфавіт; D - вихідний алфавіт; R - скінченна множина правил виду A®a,b, де aО(N ИS)*, bО(NИD)* і входження нетерміналів в слово b утворює перестановку входжень нетерміналів в слово a; S - початковий нетермінал із N.

Відношенням переведення, заданого схемою U, називається множина пар {(x,y)Ѕ(S,S) Ю* (x,y), xОS* і yОD*}.

Відношення переведення TНS*ґD* на парі мов LН S*, l Н D* називається відношенням трансляції, якщо область його визначення розв'язувана.

Відношення трансляції утворюють важливий клас переведень тому, що їх легко реалізувати перетворювачами з магазинною пам'яттю.

Параграф 2.4 присвячений атрибутним транслюючим граматикам (АТГ) для мов програмування. Атрибутні транслюючі грамматики зберігають переваги контекстно вільних граматик і в той же час містять спеціальні засоби опису нетермінальних символів і символів дій - атрибути, для коректної трансляції мов програмування. В АТГ існує можливість супроводжувати кожний нетермінальний символ і символ дії довільною кількістю атрибутів. Саме ці атрибути дозволяють породжувати коректні фрази (в синтаксичному розумінні) при перекладі з однієї мови на іншу, а також задавати семантику мов програмування.

Визначення. Атрибута транслюючи граматика - це транслюючи граматика, в якій

- кожний вхідний символ, символ дії або нетермінальний символ має скінченну множину атрибутів і кожний атрибут має скінченну множину допустимих значень;

- всі атрибути нетермінальних символів і символів дії поділяються на спадкові і синтезовані;

- правила обчислення спадкових атрибутів визначаються наступним чином: кожному входженню спадкового атрибута в праву частину продукції співставляється правило обчислення значення цього атрибута як функції деяких інших атрибутів, що входять в ліву або праву частину даної продукції, але розміщуються лівіше від нього; задається початкове значення кожного спадкового атрибута;

- правила обчислення синтезованих атрибутів визначаються так: кожному входженню синтезованого атрибута в продукції співставляється правило обчислення значень цього атрибута як функції інших атрибутів, які входять у праву частину даної продукції, і знаходяться правіше від нього.

Введемо символи дії {ДОДАТИ}, {ПОМНОЖИТИ}, які відповідають атомам ДОДАТИ й ПОМНОЖИТИ. Тоді АТГ граматика переведення інфіксних арифметичних виразів в еквівалентні арифметичні вирази в постфіксній польскій формі запису буде мати вигляд

1) <E>x => <E>q + <T>r{ДОДАТИ}y, z, p,

(x, p) ¬ НОВТ y ¬ q z ¬ r;

2) <E>x => <T>p,

x ¬ p;

3) <T>x => <T>q*<P>r {ПОмножитИ}y, z, p,

(x, p) ¬ НОВТ y ¬ q z ¬ r;

4) <T>x => <P>p,

x ¬ p;

5) <P>x => (<E>p),

x ¬ p;

6) <P>x => <I>p,

x ¬ p,

де <E> - початковий нетермінальний символ, НОВТ означає, що значення p, x повинні обчислюватися за допомогою процедури НОВТ.

Така АТГ дозволяє обчислювати значення синтаксично правильних арифметичних виразів.

Третій розділ дисертації присвячений аксіоматичним моделям проектування лінгвістичних трансляторів та теоретичним узагальненням основних співвідношень логічних систем і методу резолюцій.

У параграфі 3.1 обгрунтовується можливість використання логіки предикатів для перетворення правил довільних граматик в адекватні формули логіч-них числень. Відомо, що при перетворенні продукцій транслюючих і атрибутних транслюючих граматик у правила логіки висловлювань виникають проблеми, повязані з відсутністю в ній механізму відображення символів дії й подання атрибутів. У логіці предикатів такий механізм є. Символи дії в ній виражаються предикатними символами, а атрибути - аргументами предикатів. Крім цього, в численні предикатів є механізм керування порядком розміщення посилань у логічних формулах.

У параграфі 3.2 вводяться правила перетворення продукцій граматики в формули логіки предикатів. Головні з цих правил такі:

- кожний нетермінальний символ граматики міняємо на одноіменний одномісний предикат, аргументом якого є список, що містить ідентифікатори синтаксичних конструкцій, які є посиланнями в продукції, або - на вказаний термінальний символ в залежності від змісту продукції;

- права частина кожного правила логіки предикатів з'єднує між собою за допомогою кон'юнктивних зв'язок предикати, аргументами яких є компоненти аргумента списка.

При розробці правил еквівалентних перетворень продукції атрибутних транслюючих граматик у правила логіки предикатів ці правила доповнюються новими, а саме:

- предикати перетворюються в багатомісні у випадку, коли нетермінальні компоненти продукцій граматики мають атрибути. При цьому кожний із атрибутів утворює додатковий аргумент відповідного предиката. Предикат, який відповідає висновку в продукції транслюючої граматики, повинен містити всі аргументи, що входять у предикати-посилання цієї продукції;

- у тілі кожного правила логіки предикатів, яке відповідає продукції з атрибутної транслюючої граматики, повинні знаходитися процедури визначення спадкових і синтезованих атрибутів;

- кожному символу дії з продукції атрибутної транслюючої граматики ставиться у відповідність (в тілі правила логіки предикатів, що моделює цю продукцію) виклик процедури, який реалізує цю дію, а також виклик процедур визначення значень атрибутів символу дії.

Відомо, що контекстно вільні граматики не здатні забезпечити коректність в узгодженні синтаксичних особливостей мови. Більше того, вони допускають синтаксичну абсурдність у породжених виразах і не мають засобів для усунення вказаних недоліків.

Атрибутні транслюючі граматики можуть породжувати ідеально коректні вирази щодо синтаксичних вимог. Такі можливості цих граматик досягаються шляхом введення в граматику відповідних атрибутів, які вирішують проблему синтаксичної узгодженості.

Так, граматика з узгодженням роду (чоловічий чи жіночий), яка виключає семантично абсурдні вирази типу "Стерти цей останній рядок у цьому останньому рядку" задається наступною системою продукцій:

1) <фраза> => <дієслово>,<група_імен (Х)>;

2) <група_імен (Y1)> => <займен (K)>, <прикмет (K)>, <імен (K, Z1)>, {Y1<Z1};

3) <група_імен(Y2)> => <займен (K)>, <прикмет (K)>, <імен (K, Z2)>, {Y2 < Z2}, <приймен>, <група_імен (Z2)>;

4) <дієслово> => друкувати;

5) < дієслово > => стерти;

6) <займен (чол)> => цей;

7) <займен (жін)> => ця;

8) <прикмет (чол)> => другий;

9) <прикмет (жін)> => друга;

10) <прикмет (чол)> => останній;

11) <прикмет (жін)> => остання;

12) <імен (чол, 1)> => символ;

13) <імен (чол, 2)> => пароль;

14) <імен (жін, 3)> => рядок;

15) <імен (жін,4)> => сторінка;

16) <приймен> => в.

аксіоматичний лінгвістичний транслятор

Такі властивості граматика набуває після введення атрибутів (X,Y1,Y2,Z1,Z2) та символів дії {Y1<Z1}, {Y2 < Z2}.

За допомогою описаних правил розглянута АТГ може бути коректно перетворена в правила логіки предикатів, які мають такий вигляд:

1) фраза ([Г/ГС]) <= дієслово ([Г]), група_імен (ГС);

2) група_імен (Y1, K, [М,П,С]) <= займен (К, [М]), прикмет (К, [П]), імен (K, Z1, [C]),Y1 < Z1;

3) група_імен (Y2, K, [М,П,С, Прийм/ГС]) <= займ (K, [M]), прикмет (К, [П]), імен (K, Z2, [C]), Y2 < Z2, приймен (Прийм), група_імен (Z2, K, ГС);

4) дієслово ([друкувати]);

5) дієслово ([стерти]);

6) займен (чол,[цей]);

7) займен (жін,[ця]);

8) прикмет (чол,[другий]);

9) прикмет (жін,[друга]);

10) прикмет (чол,[останній]);

11) прикмет (жін,[остання]);

12) імен (чол,1,[символ]);

13) імен (чол,2,[пароль]);

14) імен (жін,3,[рядок]);

15) імен (жін,4,[сторінка]);

16) приймен ([в]).

У параграфі 3.3 показано, що можливість переходу від продукцій атрибутної транслюючої граматики до правил логіки предикатів дозволяє використати метод резолюцій для аналізу породжуваних нею мов.

Задача аналізу полягає в наступному: якщо G1,...,Gn - правила граматики, записані у вигляді формул логіки предикатів, то вираз L належить породженій ними мові, якщо формула G1 and G2 and... and Gn and (not(L)) суперечлива.

У цих термінах аналіз виразу L = "стерти, цей, останній, пароль" описується такою системою аксіом:

1) фраза ([Г/ГС]) Ъ (not)дієслово ([Г]) Ъ (not)група_імен (ГС);

2) група_імен ([М,П,С]) Ъ (not)займен (К, [М]) Ъ (not)прикмет (К, [П]) Ъ (not)імен (К, [С]);

3) дієслово ([стерти]);

4) займен (чол, [цей]);

5) прикмет (чол, [останній]);

6) імен(чол, [пароль]);

7) not(фраза ([стерти, цей, останній, пароль]));

8) (not)дієслово ([стерти]) Ъ (not)група_імен ([цей, останній, пароль]);

9) (not)група_імен([цей, останній, пароль]);

10) (not)займен (К, [цей]) Ъ (not)прикмет (К, [останній]) Ъ (not)імен (К, [пароль]);

11) (not)прикмет (чол, [останній]) Ъ (not)імен (чол, [пароль]);

12).

Виведення пустого диз'юнкта означає, що вираз L породжується граматикою.

Питання реалізації СК-переведень за допомогою методу резолюцій викладені в параграфі 3.4. Така реалізація відбувається шляхом побудови систем логічних аксіом (у відповідності з правилами граматик вхідної й вихідної мов) та подальшим їх перетворенням до вигляду, зручному для застосування правила резолюцій. Справедлива наступна теорема.

Теорема 1. Якщо L і l - розв'язувані мови над алфавітом К, то СК-переведення T розв'язуване.

Ця теорема є обгрунтуванням застосування правила резолюцій для побудови лінгвістичних трансляторів. Адже відомо, що метод резолюцій у випадку логіки предикатів, взагалі кажучи, не закінчує свою роботу. Тому на вхідну й вихідну мови повинні бути накладені деякі обмеження: зокрема - розв'язуваність вхідної мови, що забезпечує завершеність фази синтаксичного аналізу та синтаксична керованість відношення T, що забезпечує завершеність фази переведення.

Ці умови виконуються й у випадку розв'язуваності відношення СК-переведення. Але алгоритм трансляції, з урахуванням додаткових умов, може бути описаний іншими предикатами в системах логічного програмування.

У параграфі 3.5 наведені деякі теоретичні узагальнення логічних систем і співвідношень в них. В основі цих узагальнень лежить поняття стрілки - абстраговане від даних поняття відображення. Показано, що співвідношення логіки висловлювань виконуються в абстрактних алгебраїчних структурах - топосах, які задовольняють умовам булевості. Доведення цих результатів спирається на ряд теорем про властивості класифікатора в точковому топосі. Зокрема, мають місце наступні теореми:

Теорема 2. Об'єкт WґW в точковому топосі чотирьохзначний.

Теорема 3. Якщо J - точковий топос і <true, true>o f = <true, true>o g, <false, false>o f = <false, false>og, <true, false>of = <true, false>og, <false, true>of = = <false, true>o g, то f = g.

Показано, що в довільному булевому топосі мають місце співвідношення, аналогічні співвідношенням булевої алгебри. Доведення цих результатів здійснюється шляхом пошуку категорних аналогів цих співвідношень у топосі та застосуванні діаграмних методів доведення теорем. Зокрема, мають місце теореми про закон ідемпотентності:

Теорема 4. У довільному топосі J справедливі співвідношення <1W, 1W > o Щ = 1W, <1W, 1W > o Ъ = 1W;

про правило поглинання:

Терема 5. У точковому топосі J справедливі співвідношення Ъ o Ш = ШґШ o Щ, Щ o Ш = ШґШ o Ъ;

про закон комутативності:

Теорема 6. В булевому топосі J справедливе співвідношення + = <pr1, pr2> o +;

про співвідношення для констант:

Теорема 7. У булевому топосі J справедливе співвідношення <1W, falseW > o + = 1W.

Ці результати дозволяють зробити висновок про те, що логічні системи, аксіоматичні моделі та різні їх трансформації з точки зору такого загального підходу до поняття функції утворюють фрагмент теорії булевих топосів.

У параграфі 3.6 розглядаються деякі узагальнення правила резолюцій і алгоритму уніфікації в рамках математики, відмінної від категорії множин Set.

Таке узагальнення відбувається шляхом доведення правила резолюцій у точковому топосі й побудові категорного алгоритму уніфікації, виходячи з поняття кограниці у відповідній категорії.

Нехай операторна сукупність - це множина операторних символів, індексованих їх розмірністю. Якщо W - операторна сукупність, то через Wn позначимо множину операторів розмірності n.

Множина TW(X) термів у множині Х над операторною сукупністю W визначається рекурсивно наступним чином:

x ОX Ю бxс О TW(X),

s О Wn, t1, t2,…, tn О TW(X) Ю s ( t1, t2,…, tn) О TW(X).

Довільне відображення w: X ® TW(Y) будемо називати підстановкою термів над множиною Y замість елементів множини X.

Визначаючи композицію підстановок співвідношенням (fg)(x) = f(g(x)), ми тим самим визначаємо категорію TW, об'єктами якої є множини, а стрілками - підстановки термів.

Будемо говорити, що підстановка f: X®Y уніфікує множину пар (si,ti ), iО ОN термів, якщо "i О N, f(si) = f(ti). Такі уніфікатори існують не завжди. Однак, якщо вони існують, то найбільш загальний уніфікатор визначається як уніфікатор f:X®Y, такий, що для будь-якого іншого уніфікатора g:X®Y' існує єдина підстановка h:Y®Y', що задовольняє співвідношенню f o h = g. Таке визначення уніфікатора збігається з поняттям коурівнювача f і g в TW.

Наступні дві теореми лежать в основі алгоритму побудови коурівнювача в довільній категорії за допомогою інших коурівнювачів.

Теорема 8. Якщо стрілка q:b®c - урівнювач f,g:a®b і r:c®d - урівнювач

f' q

a' b c,

g' q

то q o r:b®d урівнювач [f, f'],[g,g']:a+a'®b.

Теорема 9. Для будь-якої епістрілки h:a'®a, стрілка q:b®c є коурівнювач пари стрілок f,g:a®b тоді і тільки тоді, коли вона є коурівнювачем пари

h o f

a' b.

h o g

У довільному топосі визначаюче співвідношення методу резолюцій буде мати вигляд

<<<pr2, pr1> o Ъ, <pr2 o Ш, pr3> o Ъ> o Щ, <pr1, pr3> o Ъ > Ю = true.

Теорема 10. У точковому топосі справедливе визначаюче співвідношення методу резолюцій.

У четвертому розділі викладені питання реалізації аксіоматичних моделей лінгвістичних трансляторів.

Параграф 4.1 присвячений опису граматики мови програмування GIPLANG. Зокрема, задається породжуюча граматика для чисел, арифметичних виразів, операторів та ін. Внаслідок введення необхідних атрибутів та симво-лів дії в продукції утворюється атрибутна транслююча граматика мови GIPLANG, деякі з правил якої мають вигляд:

1) <програма> => РЯДОК p1 {НОМРЯД}p2 {ВСТАН. Номер РЯДКА}p3 <тіло програми> кІнецЬ

(p3,p2) <- p1;

2) <тіло програми> => РЯДОК p1 {НОМРЯД }p2 {ВСТАН. Номер РЯДКА}p3 <тіло програми>

(p3,p2) <- p1;

3) <тіло програми> => ЯКЩО <вираз>p1 ВІДНОШЕННЯ r1 <вираз>q1 ПЕРЕХІД_НА s1 {УМ_ПЕРЕХІД}p2,q2,r2,s2 <інші рядки>

p2 <- p1 q2 <- q1 r2 <- r1 s2 <- s1;

4) <вираз>t2 => <терм>p1<E-список>p2,t1

p2 <- p1 t2 <- t1.

У параграфах 4.2 та 4.3 описуються правила перетворення арифметичних виразів транслюючої граматики мови GIPLANG в правила логіки предикатів та методи трансляції арифметичних виразів.

Введемо позначення:

1.wr(Ls,Lw,Swr) - вираз-предикат, де

Ls - початковий список нерозпізнаних лексем;

Lw - список лексем, які залишилися нерозпізнаними;

Swr - список розпізнаних лексем.

2. wol( Ls, Lp1, Nl) - предикат, який реалізує виділення чергової лексеми із початкового списку нерозпізнаних лексем, де

Lp1 - проміжний список нерозпізнаних лексем;

Nl - чергова нерозпізнана лексема.

3. tm(Lp1, Ltm, Nl, Stm) - предикат-терм, де

Ltm - список нерозпізнаних лексем, які повертаються термом;

Stm - список розпізнаних лексем, які повертаються термом.

4. esp(Lp2, Lesp, Nl, Stm, Sesp) - предикат E-список, де

Lp2 - проміжний список нерозпізнаних лексем, який поступає на вхід предиката E-список;

Lesp - список нерозпізнаних лексем, які повертаються предикатом esp(...);

Sesp - список розпізнаних лексем, які повертає предикат esp.

З урахуванням цих та деяких інших позначень правила логіки предикатів для арифметичних виразів будуть мати вигляд (на прикладі четвертого правила граматики):

<вираз>t2 => <терм>p1<E-список>p2,t1

+p2 <- p1 t2 <- t1

wr([],[],[Ls]).

wr(Ls,Lw,Swr) :-

wol( Ls, Lp1, Nl),

tm(Lp1, Ltm, Nl, Stm),

wol( Ltm, Lp2, Nl1),

ifthenelse(per1(Nl1),esp1(Lp2, Lesp1, Nl1, Stm, Sesp1),esp1([],[],[],[],[])),

ifthenelse(per1(Nl1),Swr = Sesp1, Swr = Stm),

ifthenelse(per1(Nl1),Lw = Lesp1, Lw = Ltm),

wr(Lw,Lw1,Swr1).

esp1([],[],[],[],[]).

wol([G/H],Nl,Lp) :-

Nl = G,

Lp = [H],

asserta(wol( Lp, Nl, Lp)),

wol( Lp, Nl11, Lp11),

retract(wol( Lp, Nl, Lp)).

Зрозуміло, що правила побудови арифметичних виразів у транслюючій граматиці для мови GIPLANG по суті є програмою для системи програмування Arity Prolog, яка реалізує лінгвістичний транслятор у частині трансляції арифметичних виразів.

ВИСНОВКИ

Основні результати дисертаційної роботи:

- запропонований аксіоматичний підхід до проектування лінгвістичних трансляторів, який дозволяє значно зменшити трудозатрати на їх створення за рахунок уніфікації методів аналізу та синтезу мов. Суть цього підходу полягає в тому, що процеси розпізнавання виразів вхідної мови й генерація адекватних виразів вихідної мови зводяться до доведення істинності відповідних логічних формул методом резолютивного виведення;

- розроблені алгоритми еквівалентних перетворень продукцій контекстно-вільних транслюючих граматик і атрибутних транслюючих граматик у правила логіки предикатів;

- розроблені алгоритми розпізнавання виразів формальної мови й реалізації синтаксично керованих переведень, що грунтуються на резолютивному виведенні;

- доведено ряд теорем для абстрактних моделей логічних числень і методу резолюцій, які, зокрема, узагальнюють правила еквівалентних перетворень формул числення висловлювань, отже дозволяють розглядати такі перетворення в математиках, відмінних від категорії множин. Запропоновані й обгрунтовані категорні моделі алгоритму уніфікації та правила резолюцій;

- реалізовані основні компоненти транслятора мови GIPLANG для арифметичних виразів в системі програмуваня Arity Prolog.

Основні результати дисертації опубліковані у таких працях:

1. Пулеметова В.А., Кондратенко А.И. Искусственный интеллект в архитектурном проектировании компьютеров //Вестник КПИ. -1994. -Вып. 30. - С. 19-34.

2. Кондратенко В.А. Распознавание цепочек формального языка с помощью метода резолюций //Материалы XIX Международной научно-технической конференции "Проблемы физической и биомедицинской электроники". Электроника и связь. -1999. -N7. -С.71-75.

3. Кондратенко В.А. Синтаксически управляемая трансляция алгоритмов от входных к выходным языкам программирования, основанная на резолютив-ном выводе //Электроника и связь. -2000. -N8. С.33-41.

4. Провотар А.И., Кондратенко В.А., Дудка Т.Н. Булева алгебра как фрагмент теории булевых топосов //Кибернетика и системный анализ. -2001. -N1. -C.163-170.

5. Провотар А.И., Кондратенко В.А. Категорные конструкции алгоритма унификации и метода резолюций //Проблемы программирования. -2000. -N 3-4. -С.22-27.

Особистий внесок. Всі результати, наведені в дисертаційній роботі, належать дисертанту і одержані ним самостійно.

У роботі [1] авторові належать математичні моделі та методи розв'язування задач архітектурного проектування комп'ютерів; [4] - особистий вклад автора полягає в доведенні визначаючих співвідношень для констант, правила поглинання, закону комутативності для додавання та закону суперечності; [5] - автору належить доведення теорем про елементи та узагальнення методу резолюцій.

КОНДРАТЕНКО В.О. Аксіоматичні моделі і методи проектування лінгвістичних трансляторів. - Рукопис.

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.03 - математичне та програмне забезпечення обчислювальних машин та систем. - Інститут кібернетики імені В.М. Глушкова НАН України, Київ, 2001.

Дисертація присвячена актуальним питанням розробки аксіоматичних моделей і методів проектування лінгвістичних трансляторів в системах логічного програмування. Зокрема, запропоновані методи перетворення правил довільних граматик в адекватні формули логічних числень, що дозволяє реалізувати фази компіляції відповідних мов з допомогою методу резолюцій. Сформульовані й доведені достатні умови завершеності фаз синтаксичного аналізу і переведення. Досліджені узагальнені моделі методу резолюцій й алгоритму уніфикації в рамках математик, відмінних від категорії множин.

Ключові слова: граматика, логіка предикатів, алгоритм, метод резолюцій, топос.

КОНДРАТЕНКО В.А. Аксиоматические модели и методы проектиро-вания лингвистических трансляторов. - Рукопись

Диссертация на соискание ученой степени кандидата физико-математических наук по специальности 01.05.03 - математическое и программное обеспечение вычислительных машин и систем. - Институт кибернетики имени В.М. Глушкова НАН Украины, Киев, 2001.

Разработан аксиоматический подход к проектированию лингвистических трансляторов в системах логического программирования.

Этот подход базируется на традиционных логических исчислениях и реализации фаз синтаксического анализа и перевода языков проектирования с помощью метода резолюций. Кроме того, рассмотрен ряд задач, в том числе задача архитектурного проектирования компьютеров, и построены соответствующие математические модели, позволяющие использовать резолютивный вывод для нахождения их решения.

Блоки компилятора - синтаксический и перевода, описываются атрибутной транслирующей грамматикой и синтаксически управляемыми трансляциями соответственно. Предложены методы преобразования правил атрибутных транслирующих грамматик и синтаксически управляемых трансляций в адекватные формулы логических исчислений. Эти методы основаны на превращении синтаксических конструкций в элементарные формальные системы с той же порождающей способностью и последующей их модификацией с целью приведения к виду, удобному для применения метода резолюций. Таким образом достигается возможность построения унифицированного механизма анализа и синтеза языков проектирования, а, следовательно, уменьшение трудозатрат на разработку компиляторов.

Известно, что метод резолюций, вообще говоря, не заканчивает свою работу. Поэтому были сформулированы и доказаны достаточные условия завершения фаз синтаксического анализа и перевода: разрешимость входного языка, которая обеспечивает завершенность фазы синтаксического анализа и формальная представимость отношения на языках, которая обеспечивает завершенность фазы перевода.

Рассмотрены некоторые обобщения метода резолюций и алгоритма унификации и построены соответствующие категорные аналоги в рамках математик, отличных от категории множеств. Такие обобщения достигаются благодаря трем наблюдениям. Во-первых, унификатор может рассматриваться как копредел в подходящей категории. Во-вторых, общие конструкции копределов позволяют написать рекурсивную процедуру вычисления унификатора термов. В-третьих, метод резолюций можно сформулировать как некоторое соотношение булевой алгебры, имеющее аналог, по райней мере, в булевом топосе.

Доказан ряд утверждений (обобщающих правила эквивалентных преобразований формул исчисления высказываний), которые открывают возможность построения обобщенных логических теорий и соответствующих методов доказательства теорем.

Описана атрибутная транслирующая грамматика основных конструкций языка программирования GIPLANG. Правила построения арифметических выражений в этой грамматике по существу являются программой для системы программирования Arity Prolog, которая реализует лингвистический транслятор в части трансляции арифметических выжений.

Ключевые слова: грамматика, логика предикатов, алгоритм, метод резолюций, топос.

Коndratenko V.A. Axiomatic models and methods of designing of linguistic translators. -Manuscript.

Thesis for candidate's degree of physics and mathematical science by speciality 01.05.03 - mathematical support and software of computers and systems. - V.M.Glushkov Institute of Cybernetics, NAS of Ukraine, Kiev, 2001.

The thesis is devoted to urgent questions of development of axiomatic models and methods of projection of linguistic compilers in systems of logic programming. In particular, offered methods of transformation of rules of any grammers in the adequate formulas of logic calculations, that allows to realize phases of compilation of the appropriate languages with the help of a method of the resolutions. The sufficient conditions of completeness of phases of the syntactic analysis and translation are formulated and proved. The investigated generalized models of a method of the resolutions and algorithm of unification within the framework of mathematics distinct from category of sets.

Key words: grammar, first-order logic, algorithm, method of the resolutions, topos.

Размещено на Allbest.ru