Методи та засоби алгебраїчного програмування в розробці математичних програмних систем

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

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

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

Автореферат

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

МЕТОДИ ТА ЗАСОБИ АЛГЕБРАЇЧНОГО ПРОГРАМУВАННЯ В РОЗРОБЦІ МАТЕМАТИЧНИХ ПРОГРАМНИХ СИСТЕМ

Волков Владислав Анатолійович

01.05.03 - математичне та програмне забезпечення обчислювальних машин і систем

Київ - 2005

Анотація

Волков В.А. Методи та засоби алгебраїчного програмування в розробці математичних програмних систем. - Рукопис.

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

Дисертаційну роботу присвячено дослідженню проблеми взаємодії в єдиному програмному середовищі компонент, що підтримують різнорідні види математичної діяльності. Така взаємодія забезпечується інтеграцією основних парадигм програмування (імперативної, функціональної, логічної, та алгебраїчної) на основі алгебраїчної. Головним результатом даного дослідження є методологія координації різноманітних видів математичної активності у різнорідному програмному середовищі шляхом подання систем у вигляді взаємодіючих математичних агентів. Розроблено базові засоби системи алгебраїчного програмування АПС, що підтримують інтеграцію основних парадигм програмування. Сформульовані архітектурні рішення, які реалізують ієрархію мовних засобів і забезпечують одночасний доступ до всіх рівнів програмування, починаючи з мови конкретної предметної області й закінчуючи рівнем мови C/С++. Ця архітектура реалізована у засобах програмної підтримки розробленої методології та використана у розробці системи перевірки формальних вимог VRS. Розроблено декларативне (алгебраїчне) представлення породжуючої схеми для класу алгоритмів типу поповнення критичними парами. Досліджені властивості цього представлення, реалізовано комплекс інструментальних програмних засобів для роботи з алгоритмами подібного типу; за допомогою цих засобів реалізовано декілька варіантів алгоритмів. Розроблено підхід до розв'язання задач інтеграції символьних обчислень з численними методами та засобами штучного інтелекту. На основі цього підходу реалізовано систему комп'ютерної алгебри AIST, орієнтовану на підтримку процесу викладання математики, та систему чисельно-аналітичних перетворень, призначену для дослідження задач прикладного математичного аналізу.

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

Аннотация

Волков В.А. Методы и средства алгебраического программирования в разработке математических программных систем. - Рукопись.

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

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

Разработаны базовые средства системы алгебраического программирования АПС, поддерживающие интеграцию основных парадигм программирования. Сформулированы архитектурные решения, реализующие иерархию языковых средства и обеспечивающие одновременный доступ ко всем уровням программирования, начиная с языка конкретной предметной области и заканчивая уровнем языка C/С++. Таким образом достигается эффективное распределение сложности разрабатываемой программной системы по различным уровням. Эта архитектура реализована в средствах программной поддержки разработанной методологи и использована в ходе разработки системы проверки формальных тренований VRS. Представлены основные компоненты математической среды: решатель, прувер и ридер. Они входят в состав математического агента и используются для выполнения основного цикла обработки математического текста: его чтения и понимания. В процессе этой обработки проверяется правильность текста, строятся доказательства утверждений и формируется база знаний.

Разработано новое декларативное (в виде системы переписывающих правил) представление пополняющих алгоритмов, позволяющее специализацию для различных вариантов их реализации. Это представление служит своего рода порождающей (generic) программой для работы как с алгоритмом Кнута-Бендикса, так и алгоритмом Бухбергера. Исследованы свойства этого представления, реализован комплекс инструментальных программных средств для работы с алгоритмами подобного типа; с помощью этих средств реализовано несколько вариантов алгоритмов. Разработан подход к решению задач интеграции символьных вычислений с численными методами и средствами искусственного интеллекта. На основе этого подхода реализовано систему компьютерной алгебры AIST, ориентированную на поддержку процесса преподавания математики, и систему численно-аналитических преобразований, предназначенную для исследования задач прикладного математического анализа.

Ключевые слова: символьные вычисления, автоматическое доказательство теорем, компьютерная алгебра, математические агенты, транзиционные системы, формальные спецификации.

Abstract

Volkov V.A. Methods of algebraic programming in development of mahematical software systems. - Manuscript . - The thesis for degree of Candidate in physics and mathematics by the speciality 01.05.03 -- Mathematical and programming software of computational machines and systems. - Glushkov Institute of Cybernetics of National Academy of Sciences of Ukraine, Kyiv 2005.

The thesis is devoted to studying a problem of interaction of components supporting heterogeneous types of mathematical activities in a single programming environment. This interaction is provided due to an integration of main programming paradigms (imperative, functional, logical and algebraic ) on a base of algebraic one. The main result of this resarch is a methodology for coordination of different types of mathematical activities in homogenous programming environment via representation of systems as matematical agents.

Basic tools of Algebraic Programming System supporting integration of the main programming paradigms are developed. Architecture solutions that implement hierarchy of language's tools and provide simultaneous access to all programming levels, starting from the level of specific subject domain and up to the level of C/C++ language. This architecture is implemented in tools of programming support of the developed methodology and applied in the development of a system for formal requirements verification VRS. Declarative (algebraic) representation of generic schema for a class of completion by critical pairs like algorithms is developed. Properties of this representation are studied, a workbench for these algorithms is implemented and on a base of a few concrete algorithms are implemented. An approach to integration of symbolic computation with numeric one and artificial intelligence tools is created. Two computer algebra systems are implemented on a base of this approach. The first one is for support of mathematical training and the second is for numeric-symbolic transformations devoted for studying of applied analysis problems.

Кey words: symbolic computations, automatic theorems proving, computer algebra, mathematical agents, transition systems, formal specifications.

1. Загальна характеристика роботи

Актуальність теми. Традиційно, вираз "математичне програмне забезпечення ЕОМ" розумівся, перш за все, у контексті чисельних обчислень. Протягом більше ніж 50 років використання обчислювальної техніки було розроблено багате програмне забезпечення, що надає можливості роботи з обчислювальними алгоритмами із різноманітних предметних областей. Однак за останні 15-20 років спостерігаються наступні яскраво виражені тенденції. Навіть ефективні чисельні методи, реалізовані на потужних суперкомп'ютерах, не можуть повністю виключити формульних перетворень. Класичним прикладом таких недоліків, що наводить D.Davenport, є факт, що розрахунок розвитку атмосферних процесів з точністю, необхідною метеорологам для 48-годинного прогнозу на найбільш потужних комп'ютерах, доступних на сьогоднішній час (типу CRAY), вимагає більше 48 годин. Таким чином, актуальним є створення програмних засобів, що підтримують символьнi/аналiтичнi обчислення (iнший термiн, що часто використовується - системи комп'ютерної алгебри). З теперішнього часу бiльшicтю сучасних систем комп'ютерної алгебри (Mathematica, Maple, Axiom, MuPad) підтримуються можливості змішаних чисельно-аналiтичних обчислень. Разом з графiчними засобами вiзуалiзацii така iнтеграцiя надає iдеальнi засоби для “наукових обчислень”. Взаємодія чисельних методiв та аналiтичних перетворень при цьому може досягатися найрiзноманiтнішими засобами, але, як правило, такий союз реалізується через зовнішню взаємодію ядра системи та відповідних бiблiотек чисельних перетворень.

З іншого боку, розв'язок нетривіальних математичних задач, як правило, вимагає використання як процедурного алгебраїчного знання (алгоритмів), так і логічного дедуктивного знання (теорем). Вже в 1963 р. John Mc Carthy висловив припущення, що ідея інтеграції алгебри і логіки може мати той самий ефект для розвитку науки, що мала в 20-му сторіччі інтеграція аналізу і фізики.

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

Починаючи з першої половини 90-х років, проводяться регулярні міжнародні конференції і семінари серії AISMC (Artificial Intelligence and Symbolic Mathematical Computing), де збираються дослідники, які працюють на перетині логічного програмування і комп'ютерної алгебри. Публікуються спеціальні випуски профільних журналів у цих галузях комп'ютерної математики (Journal of Automated Reasoning, Journal of Symbolic Computation), присвячені інтеграції методів і засобів.

Виділяються два аспекти: проблема комбінування алгоритмів і теорем в рамках єдиної системи і гетерогенна інтеграція різноманітних пакетів. Методологічно це вимагає інтеграції різних парадигм програмування, що є в основі різнорідних видів математичної активності: розв'язування задач, доведення і обчислення. Дизайн мовних та архітектурних рішень, які підтримують таку інтеграцію, став предметом інтенсивного вивчення. Підтвердженням цьому може слугувати ряд конференцій серії FroCos (Frontiers in Combining Systems), які ілюструють цю тенденцію у галузі логічного програмування.

Декілька років тому стартувала спільна ініціатива (CALCULEMUS) ряду європейських дослідницьких груп, що спеціалізуються у галузі комп'ютерної алгебри та автоматичного доведення теорем. Вона послугувала важливим структуруючим фактором у цій галузі досліджень. На сьогодні це співробітництво оформилось у вигляді Європейскої дослідницької та учбової мережі (European Research Training Network) і серії однойменних конференцій-семінарів.

Розробка інтелектуального математичного програмного забезпечення має давні історичні корені і традиції в Інституті кібернетики ім. В.М. Глушкова НАН України. Ці роботи, ініційовані В.М. Глушковим, беруть початок у 1965 р. створенням системи автоматичного доведення теорем для елементарної теорії груп. Пізніше в Інституті активно розвивались напрямки, пов'язані як з комп'ютерною алгеброю (система АНАЛИТИК), так і з автоматичним доведенням (система САД, що базується на мові практичної математичної логіки та об'єднує близьку до природної, формалізовану математичну мову з Алгоритмом Очевидності). В кінці 80-х років з'явилась перша версія Системи Алгебраїчного Програмування (АПС) (APS - Algebraic Programming System), яка базується на логіці переписування.

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

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

Зв'язок роботи з науковими програмами, планами, темами. Робота виконувалася у рамках тематик: “Розробка методів та засобів розв'язання логічних задач на алгебро-алгоритмічних моделях предметних областей”, шифр ВГЕ.100.09, номер держреєстрації 01940009539; “Розробка математичної теорії взаємодії компонент комп'ютерного середовища та її застосування у системі програмування АПС”, шифр В.Ф.100.03, номер держреєстрації 0198U000320; “Розробка ефективних формалізмів для відображення процесів свідомої (інтелектуальної) діяльності у техногенному середовищі і засобів її комп'ютерної підтримки”, шифр В.Ф.100.04, номер держреєстрації 0198U001775; “Розробити дедуктивні методи верифікації теорем з математики та програмного забезпечення ЕОМ”, шифр В.Ф.100.05, номер держреєстрації 0102U000496; “Розробити методи та засоби продукування і маніпулювання знаннями в операційному середовищі інтелектуалізації інформаційних технологій”, шифр В.Ф.К.105.01, номер держреєстрації 0102U003204; “Розробити ефективні формалізми та засоби їх підтримки для розв'язання інтелектуальних задач у техногенному середовищі”, шифр В.Ф.100.06, номер держреєстрації 0103U000704.

Мета і задачі дослідження:

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

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

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

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

· комп'ютерної алгебри;

· автоматичного доведення теорем;

· перевірки інженерних вимог до програмного продукту.

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

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

· система комп'ютерної алгебри AІST, орієнтована на підтримку процесу викладання математики;

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

· середовище для декларативного представлення та дослідження алгоритмів типу поповнення критичними парами.

Ці системи були успішно застосовані в учбово-методичному процесі ряду українських вищих учбових закладів, зокрема, Херсонського педагогічного університету, Національного університету імені Тараса Шевченка, Кіровоградського педагогічного інституту.

Апробація роботи та публікації. Наукові і практичні результати доповідались та обговорювались постійно на семінарах відділів теорії цифрових автоматів та теорії рекурсивних машин Інституту кібернетики ім. В.М. Глушкова НАН України (керівники проф. Ю.В. Капітонова і чл.-кор. НАН України O.А. Летичевський) (Київ, 1992-2004); на наукових семінарах Стенфордського дослідницького інституту (Менло-парк, США, 1998); Міжнародного інституту дослідження символьних обчислень (Лінц, Австрія, 2000); на Міжнародній школі для молодих вчених, організованій Науковим комітетом НАТО (Марктобердорф, ФРН, 1997); Міжнародному семінарі "Workshop on the Computer Algebra Applіcatіon" (Киів, 1993); Міжнародній школі "Вопросы оптимизации вычислений" (Київ, 1993); Всеукраїнській конференції "Розробка та застосування математичних методів в наукових дослідженнях" (Львів, 1995); Міжнародній конференції "Artіfіcіal Іntellіgence and Symbolіc Mathemeatіcal Computatіon" (Кембрідж, Великобританія, 1994); Міжнародній конференції "Интеллектуальные системы и компьютерное моделирование" (Москва, Росія, 1995); Міжнародній конференції "On Algebraіc Engіneerіng" (Aіzu, Японія, 1997); Міжнародному семінарі "Rewrіtіng Technіque and Effіcіent Theorem Provіng" (Kиїв, 2000); Міжнародній конференції "Искусственный интеллект" (Ялта, 2000); Міжнародному семінарі "CALCULEMUS-99" (Тренто, Італія, 1999); Міжнародній конференції "Applіcatіons of Computer Algebra" (Санкт-Петербург, Росія, 2000); Міжнародній конференції "Logіc and Complexіty іn Computer Scіence" (Париж, Франція, 2001); Міжнародній конференції "SES'01" (Чикаго, США, 2001); Міжнародній конференції "Prolongіng Software Lіfe: Development and Redevelopment ( 2002); Міжнародному семінарі "WІTUL'04" (Ренн, Франція, 2004); Міжнародній конференції, присвяченій 110-річчю винаходу радіо (Санкт-Петербург, 2005); Міжнародній конференції “SDL 2005: Model Driven” (Грімстад, Норвегія, 2005).

Результати дисертаційної праці відображені в 29 друкованих роботах загальним обсягом 9,0 др. арк. (із них 13 статей у наукових періодичних виданнях, 10 - у працях наукових конференцій, 5 тез доповідей та 1 колективна монографія).

2. Основний зміст роботи

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

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

У підрозділі 1.1 розглядаються основні поняття та нотація теорії систем переписування термів, необхідні в наступних частинах роботи. Наведено синтаксис термів першого порядку, підстановки термів і функції над ними, поняття відношення переписування, редукції та нормалізації, рівнянь над термами і правил переписування термів. Перераховані властивості систем переписування, в тому числі основні: Черча-Россера (або конфлюентність) і завершуваність (або нетеровість). Описані переваги та недоліки, характерні для систем переписування, що задовольняють цим властивостям, тобто, що є конвергентними (або канонічними).

У підрозділі 1.2 розглядаються засоби переписування термів в різних програмних системах. Досліджені елементи переписування у системах комп'ютерної алгебри (Mathematіca, Maple та ін.), системах автоматичного доведення теорем (в логіці першого порядку ? daTac, EQP, Larch Prover, OSHL, Otter, RRL, SETHEO, SATURATE; вищого порядку ? HOL, Іsabelle, Mark2, MERІLL, PVS), інтегрованих середовищ специфікування і рoзрoбки у високорівневих мовах (таких, що базуються на екваціональній логіці ? мови сімейства OBJ и OPAL; на логіці переписування ? Maude, ELAN, CafeOBJ; мови специфікації апаратного забезпечення ACL2, Nqthm). Окремо розглядаються спеціалізовані системи, призначені для дослідження і експериментування з алгоритмами типу поповнення критичними парами ? СіME, ReDuX.

Проведено порівняльний аналіз засобів переписування в трьох основних типах комп'ютерних систем. Більшість систем автоматичного доведення теорем та мов високорівневих специфікацій явно базуються на деякому екваціональному численні або мають спеціальні функції, що базуються на переписуванні, які використовуються, наприклад, для обробки асоціативно-комутативних операцій. Стосовно систем комп'ютерної алгебри можна говорити тільки про елементи переписування, котрі в явному або неявному вигляді присутні в процедурах системи. Як правило ? це можливості використання зовнішніх систем рівнянь у процесі алгебраїчного спрощення термів. При цьому використовується техніка, подібна знаходженню Грьобнерівських базисів поліноміальних ідеалів. Винятком є тільки Mathematіca, де системи правил переписування є складовою частиною мови програмування, якою реалізовано більшість математичних функцій системи. Торкаючись цієї системи, необхідно також зазначити надзвичайно цікавий проект THEOREMA, що розроблюється теперішнього часу в дослідницькому інституті символьних обчислень університету Лінцу (RІSC-Lіnz). Він передбачає, базуючись на можливостях переписування в Mathematіca, створення системи автоматичного доведення теорем, що підтримує так звану “дедукцію у природному стилі”, де переписування застосовується як для рівнянь, так і для формул в логіці вищих порядків. THEOREMA такoж підтримує ряд інших вбудованих процедур доведення, наприклад індуктивну, маючи одночасно доступ до всього багатства можливостей сучасної комп'ютерної алгебри.

Підрозділ 1.3 присвячено аналізу системи алгебраїчного програмування АПС, що базується на логіці переписування.

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

Основним інструментом для перетворень виразів є системи співвідношень (рівностей) в алгебрі даних. Коли така система розглядається як система правил переписування, вона визначає перетворення даних. З іншого боку, коли рівності системи розглядаються як тотожності, вони виражають властивості предметної області, котрі зберігаються у процесі перетворень. Розглянуто головну особливість АПС - можливість інтерпретації систем правил переписування за допомогою різних стратегій. Даний підхід дозволяє використовувати не тільки канонічні, але і будь-які інші системи рівностей. Таким чином, алгебраїчні програми можуть бути побудовані шляхом сполучення вибраної системи правил переписування з різними стратегіями їх застосування. Досліджено різноманітні можливості сполучення різних парадигм програмування. АПС інтегрує на базі алгебраїчної парадигми чотири основні парадигми програмування: імперативну, функціональну, логічну та алгебраїчну. Описана вхідна мова системи - APLAN (Algebraіc Programmіng LANguage). Ця мова дозволяє описувати не тільки алгебраїчне середовище (компоненти, операції і тотожності алгебри даних), але також писати процедури і функції, що використовуються для визначення стратегій, і викликати іх з алгебраїчних програм (систем правил переписування). Засоби представлення процедур дозволяють користувачеві маніпулювати як стандартними бібліотечними стратегіями, так і розроблювати свої власні. Логічна парадигма реалізована на базі алгебраїчної через вбудовану процедуру уніфікації.

Представлено ієрархічну структуру АПС. Верхні рівні ієрархії є предметними областями, котрі використовуються для реалізації прикладних систем. Кожна предметна область складається з множини об'єктів, які належать трьом наступним, основним типам об'єктів системи:

· алгебраїчні програми або ар-модулі;

· модулі алгебраїчних структур даних або а-модулі;

· інтерпретатори, які оброблюють алгебраїчні структури даних в а-модулях.

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

У другому розділі викладено елементи технології інсерційного та алгебраїчного програмування, використані для рoзрoбки інформаційного середовища, що надає можливість роботи з математичними специфікаціями. Виділяються два аспекти, суттєві в дизайні сучасних математичних програмних систем: поведінковий та обчислювальний. Підтверджується ефективність використання теорії агентів і середовищ для вираження семантики взаємодії різних модулів, в той час як логіка переписування використовується для представлення основних обчислювальних моделей. Пропонуються архітектурні рішення, що реалізують ієрархію мовних засобів та забезпечують одночасний доступ до всіх рівнів програмування, починаючи з мови конкретної предметної області та закінчуючи рівнем мови C/С++. Таким чином, досягається ефективний розподіл складності розроблюваної програмної системи за різними рівнями. Розділ складається з трьох підрозділів.

Підрозділ 2.1 присвячено основним поняттям інсерційного програмування, тобто програмування на базі моделі поведінки агентів у середовищах. Виділяється відмінна риса інсерційнного програмування - формалізація поняття середовища і функції занурення (іnsertіon) агентів у середовище. Функція занурення визначає композицію середовища і агента, результатом якої є нове середовище, готове для занурення інших агентів. Агенти і середовища розглядаються як об'єкти різних типів, що мають поведінку, представлену за допомогою транзиційних систем, стани яких розглядаються з точністю до бісімуляційної еквівалентності, що ототожнює транзиційні системи з однаковою поведінкою у всіх можливих оточеннях.

Розмічена транзиційна система над множиною дій A представляє собою множину станів S разом з відношенням переходів T SЧAЧS. Факт, що (s,a,s')T записується у вигдяді і кажуть, що система S переходить зі стану s до стану s' під дією a.

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

.

Розглядаються способи задання поведінки транзиційних систем над множиною дій A, як виразів алгебри поведінок F(A). Ця алгебра має дві операції - префіксінг a.u, який помножує поведінку u на дію a, і недетермінований вибір u+v однієї з двох поведінок u і v. Недетермінований вибір є асоціативною, комутативною та ідемпотентною операцією.

Підрозділ 2.2 присвячено архітектурі математичного інформаційного середовища, представленого у вигляді чотирьох взаємопрониклих шарів, кожному з яких співставляються відповідні засоби мовної підтримки. Самим верхнім шаром є рівень користувача і розроблюваної предметної області. Для цих цілей був розроблений клас мов формальних вимог FRL (Formal Requіrements Language), призначений для специфікування поведінкових, структурних і логічних властивостей моделі. Термін математична специфікація тут розуміється в досить широкому сенсі, оскільки формалізовані вимоги та математичні специфікації стали останнім часом невід'ємною частиною організованого промислового виробництва комп'ютерних виробів. Показано, що в конструкції FRL можуть бути природно вкладені, наприклад, сучасні декларативні та графічні мови моделювання типу UML, SDL і MSC.

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

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

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

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

Третій розділ присвячений порівняльному дослідженню двох найбільш відомих представників класу алгоритмів поповнення критичними парами: алгоритмами Кнута-Бендікса і Бухбергера. Основним результатом є інтегрована процедура, що об'єднує обидва алгоритми. Процедура поповнення Кнута-Бендікса - це напіврозв'язуюча процедура, яка у випадку свого успіху обчислює канонічну систему правил переписування за заданою множиною рівнянь над термами першого порядку. Процедури поповнення термів існують також для переписування за модулем екваціональної теорії, наприклад, у випадку асоціативності і комутативності деяких функціональних символів. Для заданого поліноміального (від багатьох змінних) ідеалу над полем коефіцієнтів F алгоритм Бухбергера обчислює базис, що називається Грьобнерівським або стандартним. Цей базис може розглядатися як множина правил, канонічне відношення редукції над поліномами.

Розроблено нове декларативне (у вигляді системи правил переписування) представлення алгоритмів поповнення, що дозволяє спеціалізацію для різних варіантів їх реалізації. Це представлення слугує свого роду породжуючою (generіc) програмою для роботи як з алгоритмом Кнута-Бендікса, так і алгоритмом Бухбергера. Досліджено такі важливі властивості представлення як коректність і завершуваність. Описано комплекс інструментальних програмних засобів для роботи з алгоритмами подібного типу. В тому числі розглянуто імплементаційні аспекти, що стосуються як послідовних, так і паралельних варіантів алгоритмів. Розділ складається з трьох підрозділів.

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

В абстрактній декларативній формі процедура поповнення для редукцій за відношенням еквівалентності Т була представлена Бечмеєром і Дершовіцем у вигляді числення перетворення екваціональних доведень до нормальної форми. З цієї точки зору алгоритм поповнення представляється як система правил виведення, кожне з яких являє собою бінарне відношення між парами (E,R), де E - множина невпорядкованих рівнянь; R - множина орієнтованих правил переписування; cp(R) - множина критичних пар.

Delete: (E{s = s}; R) |-- (E; R),

Compose: (E; R{s t}; R) |-- (E; R{s u}) , якщо t_R u,

Sіmplіfy: (E {s = t}; R) |-- (E {s = u}; R) , якщо t_R u,

Orіent: (E {s = t}; R) |-- (E, R {s t}; R) , якщо s > t,

Collapse: (E; R {s = t};R) |--(E {u = t}; R), якщо s_R u по l r,

s е › l r,

Deduce: (E; R) |-- (E {s = t};V) , якщо s=t cp(R). (1)

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

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

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

· критерій зв'язності критичних пар для алгоритму Бухбергера може бути успішно перенесено на процедуру поповнення для термів;

· в деяких випадках обидві процедури можуть бути використані в одних і тих самих задачах, подібно доведенню теорем, використовуючи формули у формі з виключеною зв'язкою АБО (так звана xor-нормальна форма) і поповненню скінченно-представлених комутативних структур.

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

· відношення поліноміальної редукції є напівсумісним, слабкішим, і відповідно більш загальним, ніж сумісне відношення переписування;

· невідомо завершувана і конфлюентна системи переписування термів для поліномів в дистрибутивній нормальній формі;

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

· поле не може бути представлено чисто екваціональною специфікацією.

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

(faіl,z) faіl,

(і:0, z) z,

(і:nіl, z) z,

(4:x,5:y,z) (2:Reduce(y,x),4:x,z), якщо Reduce(y,x)y,

(4:x,5:y,z) (5:y,4:x,z) & joіn(CP(x,y)) & joіn(CP(y,x)),

(4:x,5:y ) (2:Reduce(y,x),5:x)), якщо Reduce(y,x)y,

(4:x,5:y ) (5:y,5:x) & joіn(CPr(x,y)) & joіn(CP(y,x)),

(і:x,5:y,z) (5:y,2:Reduce(x,y),z)), якщо Reduce(y,x)y&(і<4),

(і:x,5:y,z) (5:y,і:x,z), якщо (і<4),

(і:x,5:y ) (5:y) & joіn(3:Reduce(x,y)), якщо Reduce(y,x)y&( і<4),

(1:x,5:y ) (5:y) & joіn(4:x),

(2:x,5:y ) (5:y) & joіn(3:x),

(3:x,5:y ) (5:y) & joіn(4:x). (2)

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

1. початкові претенденти ? нередуковані елементи. До них належать елементи вихідної множини, які ще не оброблювалися, та елементи, породжені критичними парами, котрі можуть поповнити поточний базис;

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

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

4. кандидати, повністю редуковані поточним базисом;

5. члени поточного базису.

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

Це представлення використано у реалізації мовою APLAN в системі APS. Відповідним чином параметризоване, воно реалізує алгоритм Кнута-Бендікса або Бухбергера. Представлено структури даних, що використовуються при розробці алгоритмів, основні функції і предикати. Описано стратегію застосування системи співвідношень, наведено її специфікацію у вигляді АПЛАН процедури, сформульовані властивості, яким вона має задовольняти.

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

Розглядається моделювання паралельної реалізації алгоритму Бухбергера у вигляді мульти-модульної АПЛАН програми на основі механізму передачі повідомлень. Описується спеціальна стратегія переписування, що підтримує паралельні обчислення поповнюючих алгоритмів. Наведено результати моделюючих експериментів, які демонструють високий ступінь паралелізму, властивого процедурам, що досліджуються, зокрема алгоритму обчислення базисів Грьобнера. Дана версія розпаралелюючої програми припускає багатопроцесорну архітектуру з розподіленою пам'яттю та крупнозернистим паралелізмом, що базується на передачі повідомлень, але може бути переналагоджена на інші архітектури і стилі шляхом відносно нескладного переписування інтерпретатора АПЛАНа, який підтримує інші концепції паралелізму.

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

Підрозділ 4.1 описує підхід до розв'язання задачі інтеграції символьних і чисельних обчислень. Проведено порівняльний аналіз переваг і недоліків сучасних підходів до розробки систем комп'ютерної алгебри. Аргументована необхідність використання високорівневих алгебраїчних специфікацій алгоритмів у вигляді систем правил переписування, що є способом, найбільш близьким до природної математичної мови. Показано використання середовища, яке забезпечує можливість символьних перетворень для розв'язання задач прикладного математичного аналізу. В тому числі дослідження та реалізації спеціальних функцій математичної фізики, що є розв'язками лінійних диференціальних рівнянь з поліноміальними коефіцієнтами. В цьому випадку функції y=y(x), x [a,b] замінюються спеціальними алгебраїчними поліномами наступного вигляду:

y(x,Eps) : y - y(Eps) = max y(x) - y(x,Eps) < Eps. (3)

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

Представлена реалізація базових засобів, що використовуються для підтримки обчислень в алгебрі поліномів. Серед них найбільш важливими є функції, які реалізують операції арифметики цілих і раціональних чисел "довільної" довжини, різні представлення поліноміальних виразів (“природне”, векторне, рекурсивне), функції канонізації поліномів, розв'язання лінійних рівнянь, розв'язання задачі Коші на відрізку [a,b] і крайової задачі (двоточкової і багатоточкової) для лінійних диференціальних рівнянь з поліноміальними коефіцієнтами.

У підрозділі 4.2 розглядається алгебраїчне середовище як засіб для інтеграції символьних обчислень і штучного інтелекту. В термінах правил переписування формально специфіковані два різних типи розв'язувачів. Перший представляє собою універсальний розв'язувач логічних задач. Показана можливість розширення класичного ПРОЛОГ-подібного розв'язувача спеціальними алгоритмами для розв'язування рівнянь в різноманітних алгебрах. Другий розв'язувач орієнтовано на розв'язання задач, заданих на обчислювальних моделях. Розв'язання задачі складається з двох стадій: складання плану і розв'язання рівнянь. На другій стадії необхідна взаємодія з універсальним розв'язувачем для отримання розв'язку рівнянь.

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

Підрозділ 4.3 присвячено спеціалізації математичного інформаційного середовища для розв'язання задач перевірки формальних специфікацій вимог до програмного або апаратного забезпечення. Обгрунтовуються мотивація застосування математичних (формальних моделей) у процесі розробки, зокрема, при роботі зі специфікаціями в таких мовах як MSC, SDL, UML та інтегрованого використання техніки автоматичного доведення теорем і засобів моделювання. Коротко характеризуються основні поняття і мовні засоби, пов'язані з технологією представлення вимог у формі базових протоколів, що базуються на теорії взаємодії агентів і середовищ. Базові протоколи представляють вимоги у вигляді трійок Хоара б > <P> в, де P - процес, б і в - логічні формули, що визначають перед- і постумови для процесу P. Такі представлення близькі до вимог та функціональних специфікацій, що використовуються в інженерній практиці. Описано підхід для перевірки статичних властивостей базових протоколів - транзиційної несуперечливості, повноти, а також динамічних властивостей систем, що визначаються базовими протоколами: цілісність і безпечність, завершуваність і досяжність, коректність анотованих сценаріїв. Представлені основні функціональності системи VRS (Verіfіcatіon of Requіrements Specіfіcatіons): розробка і відлагодження формальних вимог у вигляді набору базових протоколів; перевірка формальних вимог; породження трас і сценаріїв; доведення властивостей заданих в анотованих MSC і SDL специфікаціях.

В заключній частині наведені основні результати дисертаційної роботи та перспективи її розвитку.

програмування алгебраїчний інсерційний

Висновки

У дисертаційній роботі отримано такі результати:

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

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

3. Базуючись на інтегрованому використанні основних парадигм програмування, запропонована методологія координації різноманітних видів математичної активності в різнорідному програмному середовищі шляхом представлення систем у вигляді взаємодіючих математичних агентів. Сформульовані архітектурні рішення, що реалізують ієрархію мовних засобів і забезпечують одночасний доступ до всіх рівнів програмування, починаючи з мови конкретної предметної області і закінчуючи рівнем мови C/С++. Ця архітектура реалізована в засобах програмної підтримки розробленої методології та використана при розробці системи перевірки формальних вимог VRS.

4. На основі порівняльного дослідження двох найбільш відомих представників класу алгоритмів поповнення критичними парами (Кнута-Бендікса і Бухбергера), розроблено декларативне (алгебраїчне) представлення породжуючої схеми для цього класу алгоритмів. Досліджені властивості даного представлення, реалізовано комплекс інструментальних програмних засобів для роботи з алгоритмами подібного типу. За допомогою цих засобів реалізовано декілька варіантів алгоритмів.

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

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

1. Kapіtonova Y.V., Letіchevsky A.A., L'vov M.S., Volkov V.A. Tools for solvіng problems іn the scope of algebraіc programmіng // Lecture Notes іn Comp. Sci. - 1995. - 958. - P. 30- 47.

2. Денисенко П.М., Летичевський О.А., Біленко В.І., Волков В.А. Реалізація модифікованого методу В.К.Дзядика засобами алгебраїчного програмування // Волинський математичний бюлетень. - 1996. - №3. - С. 76-79.

3. Волков В.А., Капитонова Ю.В., Летичевский А.А. Технологические новации в системе алгебраического программирования // Проблемы программирования. - 1997. - №4. - С. 64- 72.

4. Летичевский А.А, Денисенко П.Н., Биленко В.И., Волков В.А. Реализация численно-аналитических методов приближения функций, заданных обыкновенными дифференциальными уравнениями // Кибернетика и системный анализ. - 1997. - №1. - С.108-112.

5. Летичевский А.А, Денисенко П.Н., Волков В.А. Алгоpитмы компьютеpной алгебpы теоpии аппроксимации в APS // Искусственный интеллект. - 1999. - №2. - С. 248-254.

6. Волков В.А., Денисенко П.Н., Летичевский А.А. APS как средство компьютеризации математики // Там же. - 2000. - №3. - С. 443- 449.

7. Капитонова Ю.В., Летичевский А.А., Волков В.А. Дедуктивные средства системы алгебраического программирования // Кибернетика и системный анализ. - 2000. - №1. - С.17-35.

8. Волков В.А. O декларативном представлении алгоритмов пополнения критическими парами // Там же. - 2001. - №6. - С.18-24.

9. Letіchevsky A.A., Kapіtonova J.V., Kotlyarov V.P., Letіchevsky A.A. Jr, Volkov V.A. Semantіcs of tіmed MSC language // Там же. - 2002. - №4. - С.3-14.

10. Летичевский А.А., Капитонова Ю.В., Волков В.А, Летичевский А.А. (мл.), Вышемирский В.В. Инсерционное программирование // Там же. - 2003. - №1. - С.19-32.

...