About one Approach for the Verification of Algebraic Computations

About one Approach for the Verification of Algebraic Computations

The approach to verification of interpreters of multi-sorted algebraic operations by their speci­fi­cations, based on constructive clarification of expansion concept of multi-sorted algebraic system and provingthe axioms of algebraic system is considered. This approach is illustrated by the examples...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2025
Автор: Lvov, M.S.
Формат: Стаття
Мова:Russian
Опубліковано: PROBLEMS IN PROGRAMMING 2025
Теми:
UDC 004.415.28
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/823
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
id pp_isofts_kiev_ua-article-823
record_format ojs
resource_txt_mv ppisoftskievua/89/ea46166b2e492f277f1e7ec4b2e3e789.pdf
spelling pp_isofts_kiev_ua-article-8232025-09-02T15:42:07Z About one Approach for the Verification of Algebraic Computations Об одном подходе к верификации алгебраических вычислений Про один підхід до верифікації алге­б­раїчних обчислень Lvov, M.S. UDC 004.415.28 УДК 004.415.28 УДК 004.415.28 The approach to verification of interpreters of multi-sorted algebraic operations by their speci­fi­cations, based on constructive clarification of expansion concept of multi-sorted algebraic system and provingthe axioms of algebraic system is considered. This approach is illustrated by the examples of verification of interpreters of operations of rational numbers field, polynomials of one variable and propositional algebra. This approach has been used for development of the computer mathematics systems of the educational purpose.Problems in programming 2011; 4: 23-35 Рассмотрен подход к верификации интерпретаторов многосортных алгебраических операций по их спецификациям, основанный на конструктивном уточнении понятия расширения многосортной алгебраической системы и доказательстве аксиом алгебраической системы. Этот подход иллюстрируется примерами верификации интерпретаторов операций поля рациональных чисел, многочленов одной переменной и алгебры высказываний. Подход использован при разработке систем компьютерной математики учебного назначения.Problems in programming 2011; 4: 23-35 Розглянуто підхід до верифікації інтерпретаторів багатосортних алгебраїчних операцій за їх специфікаціями, оснований на конструктивному уточненні поняття розширення багатосортної алгебраїчної системи і доведенні аксіомалгебраїчної системи. Цей підхід проілюст­ровано прикладами верифікації інтерпретаторів операцій поля раціональних чисел, багаточленів однієї змінної та алгебри висловлень. Підхід буловикористано при розробці систем комп’ю­терної математики навчальногопризначення. Problems in programming 2011; 4: 23-35 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-09-02 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/823 PROBLEMS IN PROGRAMMING; No 4 (2011); 23-35 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 4 (2011); 23-35 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 4 (2011); 23-35 1727-4907 ru https://pp.isofts.kiev.ua/index.php/ojs1/article/view/823/875 Copyright (c) 2025 PROBLEMS IN PROGRAMMING
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2025-09-02T15:42:07Z
collection OJS
language Russian
topic
UDC 004.415.28
spellingShingle
UDC 004.415.28
Lvov, M.S.
About one Approach for the Verification of Algebraic Computations
topic_facet
UDC 004.415.28

УДК 004.415.28

УДК 004.415.28
format Article
author Lvov, M.S.
author_facet Lvov, M.S.
author_sort Lvov, M.S.
title About one Approach for the Verification of Algebraic Computations
title_short About one Approach for the Verification of Algebraic Computations
title_full About one Approach for the Verification of Algebraic Computations
title_fullStr About one Approach for the Verification of Algebraic Computations
title_full_unstemmed About one Approach for the Verification of Algebraic Computations
title_sort about one approach for the verification of algebraic computations
title_alt Об одном подходе к верификации алгебраических вычислений
Про один підхід до верифікації алге­б­раїчних обчислень
description The approach to verification of interpreters of multi-sorted algebraic operations by their speci­fi­cations, based on constructive clarification of expansion concept of multi-sorted algebraic system and provingthe axioms of algebraic system is considered. This approach is illustrated by the examples of verification of interpreters of operations of rational numbers field, polynomials of one variable and propositional algebra. This approach has been used for development of the computer mathematics systems of the educational purpose.Problems in programming 2011; 4: 23-35
publisher PROBLEMS IN PROGRAMMING
publishDate 2025
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/823
work_keys_str_mv AT lvovms aboutoneapproachfortheverificationofalgebraiccomputations
AT lvovms obodnompodhodekverifikaciialgebraičeskihvyčislenij
AT lvovms proodinpídhíddoverifíkacííalgebraíčnihobčislenʹ
first_indexed 2025-09-17T09:24:22Z
last_indexed 2025-09-17T09:24:22Z
_version_ 1850410159769124864
fulltext Теоретичні та методологічні основи програмування 23 } УДК 004.415.28 М.С. Львов ОБ ОДНОМ ПОДХОДЕ К ВЕРИФИКАЦИИ АЛГЕБРАИЧЕСКИХ ВЫЧИСЛЕНИЙ Рассмотрен подход к верификации интерпретаторов многосортных алгебраических операций по их спецификациям, основанный на конструктивном уточнении понятия расширения многосортной алгебраической системы и доказательстве аксиом алгебраической системы. Этот подход иллюстрируется примерами верификации интерпретаторов операций поля рациональных чисел, многочленов одной переменной и алгебры высказываний. Подход использован при разработке систем компьютерной математики учебного назначения. Введение Разработка алгоритмов алгебра- ических вычислений – одна из основных задач, возникающих при реализации программных систем, основанных на символьных преобразованиях [1, 2]. Математическая модель этой задачи – многосортные алгебраические системы (МАС) [3]. Практика разработки даже достаточно простых математических систем учебного назначения [4–6] показала, что реализация алгебра- ических вычислений нуждается в тщате- льном предыдущем проектировании МАС в виде иерархий сортов и спецификаций интерпретаторов много- сортных алгебраических операций [7–8]. Для реализации вычислений, осно- ванных на символьных преобразованиях, используется система алгебраического программирования APS [1, 8, 9], адаптированная В. Пеcчаненко [10]. APS использует технологии алгебра- ического программирования, основанные на системах правил переписываний и стратегиях переписываний. Таким образом, интерпретаторы алгебраических операций определяются системой правил переписываний термов (rewriting rules system). В данной работе рассматривается подход к верификации интерпретаторов многосортных алгебраических операций по их спецификациям, основанный, во- первых, на конструктивном уточнении понятия расширения многосортной алге- браической системы и, во-вторых, на алоритме доказательства аксиом МАС как тождеств. Основная идея заключается в следующем: если интерпретаторы опера- ций МАС специфицированы и каждая аксиома – равенство или условное равенст- во, она является тождеством или условным тождеством в конструктивной реализации МАС, т. е. ее можно доказывать. Этот подход проиллюстрирован примерами реализации интерпретаторов операций поля рациональных чисел, мно- гочленов одной переменной и алгебры высказываний. Отметим, что эта работа – прямое продолжение [11]. 1. Многосортные алгебры как модель алгебраических вычислений Определение 1. Пусть – конечное множество символов, называе- мое сигнатурой сортов. Символы , ,...,{ 1 kuuU = lu },...,1{ kl∈ , называются именами сортов или сортами. Перечислим имена стандартных сортов: Variable – сорт переменных, Bool – сорт логических значений, Nat – сорт полукольца натуральных чисел, Int – сорт кольца целых чисел, Real – сорта поля действительных чисел. © М.С.Львов, 2011 ISSN 1727-4907. Проблеми програмування. 2011. № 4 Теоретичні та методологічні основи програмування 24 Другие имена сортов будем вводить при определении соответствую- щих алгебраических понятий. Определение 2. Пусть – конечное семейство множеств, индексированных именами сортов, называемых носителями соответствующих сортов. }{ 1 kuu ,...,SSS = VariableS – множество переменных, BoolS – множество {False, True}, NatS – множество натуральных чисел, IntS – множество целых чисел, alSRe – множество действительных чисел. Определение 3. Многосортной операцией над называется отображение f S vuu SSSf m →×× ...: 1 , где – сорта аргументов и результата операции соответственно, а m – арность . Uvuu m ∈,,...,1 f f Тип операции определяется спис- ком имен сортов ее аргументов и значения и обозначается . Сигнатурой операций называется конечное множество символов операций вместе с отображением, которое каждому символу vuu m →),...,( 1 Σ Σ∈ϕ ставит в соответствие многосортную операцию вместе с ее типом. Запись ϕf vuu m →),...,(: 1ϕ означает, что символу ϕ соотвтествует операция типа vuu m →),...,( 1 . Многосортной операцией является, например, операция умножения в векторном пространстве. Если Vectorspace – имя векторного пространства над полем Real действительных чисел, то операция умно- жения задается спецификацией Mult eVectorSpaceVectorSpacalMult →×Re: . В дальнейшем будем пользоваться обычными математическими обозначени- ями операций. Поскольку умножение вектора на скаляр – бинарная операция с инфиксной формой записи, ее специ- фикация имеет вид eVectorSpaceVectorSpac*alRe → . Определение 4. Многосортным пре- дикатом P называется отображение Booluu SSSP m →×× ...: 1 , где Uuu m ∈,...,1 . Последовательность определяет тип предиката, а число m – его арность. muu ,...,1 Сигнатура Π многосортных преди- катов определяется аналогично сигнатуре операций. Определение 5. Многосортной алгебраической системой A называется четверка ><= ΠΣ ,,, USA , где – множество сортов с именами из , S U },...,{ 1 lϕϕΣ = – сигнатура многосорт- ных операций, },...,{ 1 pππΠ = – сиг- натура многосортных предикатов. Замечание 1. Поскольку сорт Bool можно включить во множество сортов, предикаты можно рассматривать как мно- госортные операции. Поэтому сигнатуры операций и предикатов можно объединить, рассматривая многосортные алгебры. Определение 6. Пусть ><= Σ,,USA – многосортная алгебра и – сим- волы ее сортов. Будем говорить, что сорт зависит от сорта , если одна из операций Uvu ∈, v u Σ имеет тип vuuu m →×××× ......1 . обозначим подмножество сортов, от которых зависят сорт . Подмножество элементов vU v Σ , которые имеют тип vuuu m →×××× ......1 , обозначим vΣ , а семейство областей значений сортов – . Ограничением алгебры vU vS vA A на сорт называется МАС v >=< vvvv USA Σ,, . Таким образом, МАС A может быть представлена набором ограничений (алгебр) UvAv ∈, , т. е. . >=< kuu AAA ,..., 1 Пример 1. Задача состоит в том, чтобы построить программную систему, которая поддерживает упрощение целых алгебраических и тригонометрических вы- ражений. Модуль алгебраических вычис- лений системы должен поддерживать вы- числения в кольце полиномов и кольце тригонометрических выражений многих Теоретичні та методологічні основи програмування 25 переменных над полем рациональных чи- сел . Спецификациям подлежат алгебры – ограничения на следующие сорта: Rat – поле рациональных чисел, Rat – кольцо полиномов многих переменных, omMultiPolyn Lincomb – векторное пространство ли- нейных комбинаций многих перемен- ных (аргументы тригоном. полиномов), – кольцо целых триго- нометрических выражений многих переменных. nomMultiTPoly Отношение зависимости сортов порождает структуру зависимости на множестве алгебр : алгебра зависит от алгебры , если сорт зависит от сорта . Итак, многосортная алгебра представляет собой иерар- хическую структуру (рис.1), которую можно реализовывать инкрементным образом. UuAu ∈, vA uA v u Рис. 1. Диаграмма отношения зависи- мости алгебр примера 1 Аксиомы и конструкции МАС. Для построения алгебр будем использо- вать их аксиоматические и конструктив- ные описания (спецификации). uA Определение 7. Аксиомой алгебры называется равенство или условное равенство в сигнатуре uA uΣ . Аксиоматичес- ким описанием алгебры , по определе- нию, является конечная система аксиом алгебры . uA uA Замечание 2. Алгебры с аксиомами типа равенств называют многообразиями. Алгебры с аксиомами типа равенств или условных ра- венств называют квазимногообразиями. Будем пользоваться алгебраической терминологией и системами аксиом из [11]. Для определения конкретной алге- бры вместе с аксиомами часто используют так называемые постулаты минимальности. Например, поле рациональных чисел можно определить как минимальное поле, содержащее множество натуральных чи- сел. Аналогично, кольцо многочленов над полем – минимальное комму- тативное кольцо с единицей, содержащее поле и ][xF F F x . Конструктивное описание алгебры состоит в определении конструктора сорта и спецификаций интерпретаторов операций uA uS uΣ . Определение 8. Сигнатурой конст- рукторов называется конечное множе- ство символов конструкторов вместе с отображением, которое каждому символу T Tu ∈τ ставит в соответствие символ сорта u вместе со списком символов сортов его аргументов. Если τ – символ конструктора сорта , то выражение u ),...,( 1 muuu τ= означает, что τ соответствует символ сорта и символы сортов его аргументов . u muu ,...,1 MultiPolynom MultiTPolynom Rat LinComb Variable Конструктором сорта называет- ся система равенств, которая определяет синтаксически элементы сорта в виде термов вида uS uS ),...,( 1 muuτ в сигнатуре Τ . Определение 8 – ключевое в нашем подходе к спецификации алгебраических вычислений. Пример 2. Поле Rat рациональных чисел. Элементы этого поля – рациональ- ные числа, представленные в виде обыч- ных дробей. Конструктор сорта определяет стандартную форму представления элемен- та этого сорта. Чаще всего это канони- ческая форма. Таким образом, }1),(,,:{ =∈∈= qpGCDSqSp q pS NatIntRat . Теоретичні та методологічні основи програмування 26 Роль конструктора сорта играет символ “–” (горизонтальная черта). Этот же символ математики используют для обозначения операции деления, в частно- сти, в Rat. Это – математическая традиция. Такую же роль играет, например, символ корня, символы сложения и умножения в представлении ( 2*ba + ). Однако, для задачи специфи- каций алгебраических вычислений это не совсем удобно. Конструкторы сортов должны иметь свои обозначения. Поэтому отдельно вводится понятие сигнатуры операций Σ и сигнатуры конструкторов . В частности, для конструктора сорта Rat используется двойная наклонная черта: Τ }1),(,,://{ =∈∈= qpGCDSqSpqpS NatIntRat . В стандартных формах представ- ления элементов сортов синтаксические аспекты, определяемые символами конст- рукторов, практически всегда дополняется семантическими аспектами, задаваемыми в виде контекстных условий. В нашем примере – это равен- ство . 1),( =qpGCD Пример 3. Кольцо Polynom поли- номов одной переменной над полем Rat. Элементы этого поля – полиномы, пред- ставляемые в виде суммы мономов, упорядоченных в порядке убывания степеней. )}.deg()deg( ,:...{ 1 10 +> ∈+++= ii MonomikPolynom MM SMMMMS В спецификациях сорта Polynom это определение рекурсивно. При таком подходе отдельно нужно определить понятие степени полинома. Monom df Polynom MonomPolynom SPM MQSP SMPMQQS ∪> =∈ ∈++== )}deg()deg( ;degdeg, ,,:{ Для определения носителей сортов будем использовать специальный язык спецификаций, который допускает нерекурсивные и рекурсивные синтаксические определения элементов сортов, определения функций доступа и контекстных условий. Приведем определения сортов: Rat r ={ (Int a)//(Nat b); // Конструктор сорта Num(r) = a, Den(r) = b; // Функции доступа (селекторы) GCD(a, b) = 1 //Контекстное условие }; Monom M ={ (Rat c)$(Const Variable x)^(Nat n); // Конструктор сорта Coef(M) = c, // Функции доступа Var(M) = x, Deg(M) = n }; Polynom P = { (Monom M)++(Polynom Q); //Конструктор сорта LeadMonom(P) = M, // Функции доступа LeadCoef(P) = Coef(M), Deg(P) = Deg(M); Deg(P) > Deg(Q) // Контекстное условие }; Реализовать вычисления в алгебре UvAv ∈, означает реализовать алгоритмы выполнения каждой ее операции так, чтобы выполнялись аксиомы этой алгебры. Определение 9. Интерпретатором операции сигнатуры называется функ- ция, реализующая алгоритм выполнения этой операции. uΣ Интерпретаторы операций описыва- ются в языке APLAN системы APS. Итак, для аксиоматического и кон- структивного описания алгебры в ее определение включается конечное множе- ство аксиом и конеченое множество интерпретаторов . Многосортная алгебра определяется следующим образом: vA vAx vI vA >=< vvvvvvv I,Ax,,T,U,SA Σ . Теоретичні та методологічні основи програмування 27 2. Расширения многосортных алгебр Определение 10. Пусть и – многосортные алгебры. называется расширением , если и для любой пары операций и типов uA vA vA uA vu SS ⊂ 1f 2f uuuf m →),...,(: 11 , , если , то vvvf m →),...,(: 12 mm vuvu SS,...,SS ⊆⊆ 11 →××∈∀ muum SSaa ...),...,( 11 ),...,(),...,( 1211 mm aafaaf =→ . Вложением называется изо- морфное отображение vu SSd ′→:Re , которое отображает на подмножество . Ограничение алгебры на подмножество , изоморфное , определяется системой условных тождеств : uS vv SS ⊂′ uA vS ′ uA )(),...,(1 xExE k )}(),...,(|{ 1 aEaESaS kvv ∈=′ . Применение системы как системы переписываний «реду- цирует» терм к терму )(),...,(1 xExE k vSa ′∈ uSa ∈′ : . Конструктивное описание как расширения состоит в описании конструктора и вложения в алгебру . ')(Re 1 aad =− vA uA vA uA vA Замечание 3. Понятие конструк- тивного расширения многосортных алгебр – основное в данной работе. Основы теории упорядочено-сортных ал- гебр в ее применении к теории програм- мирования изложены в [12, 13]. Пример 4. Рассмотрим констру- ктор поля Rat (пример 2). В соответствии с определением, он определяет конструкцию Rat, аргументы которой – сорта Int и Nat. Дополним спецификации сорта Rat вложением , определеным равенством IntRat:dRe → aad =)1//(Re . Тем самым сорт Rat определен как расши- рение сорта Int. Рассмотрим конструктор кольца Polynom (пример 3). Он определяет рекур- сивно сорт Polynom через сорт Monom. Дополним спецификации сорта Polynom вложением MonomPolynom:dRe → , опре- деленным равенством MMd =++ )0(Re . Тем самым сорт Polynom определен как расширение сорта Monom. В свою очередь, сорт Monom – расширение сорта Degree с функцией Red, определенной равенством k^xk^x$ =1 , расширение сорта LinMonom с функцией Red, определенной равенством x$a^x$a =1 и расширение сорта Rat с функцией Red, определенным равенством . a^x$a =0 Сорта Degree и LinMonom, в свою очередь – расширения сорта Variable с редукциями x^x =1 и . Диаграмма расширений примера показана на рис. 2. xx$ =1 Использование расширений – один из основных методов спецификаций много- сортных алгебр. В частности, он позволяет определить перегруженные алгебраические операции и функции приведения алгебраических типов. Polynom Monom Рис. 2. Диаграмма расширений примера 4 Degree LinMonom Rat Variable Теоретичні та методологічні основи програмування 28 Статические и динамические расширения Определение 11. Расширение B алгебры A называется статическим (нерекурсивным), если в его конструкторе ),...,,...,( 1 nAAAB τ= ни один из аргументов не совпадает с B . Примеры статических расши- рений: 1) поле Rat – статическое расширение кольца Int, поскольку Rat R = (Int A) // (Nat B); 2) полугруппа мономов Monom одной образующей – статическое расширение поля коэффициентов Coef, поскольку )()^)$(( NNatxVaraCoefMMonom = . Определение 12. Расширение B алгебры A называется динамическим (рекурсивным), если в конструкторе ),...,,...,( 1 nAAAB τ= по меньшей мере один из аргументов совпадает с B . Конструкторы динамических рас- ширений определяются рекурсивно. На- пример: 3) векторное пространство Lincomb линейных комбинаций многих перемен- ных над полем Coef – линейное динами- ческое расширение одномерного прост- ранства Linmonom, элемент которого имеет вид Элемент имеет вид с конструктором .$xa LinCombw∈ mm x$a...x$aw ++++= 11 )()( wLinCombuLinMonomwLinComb ++= , ; uu =++ 0 4) кольцо Polynom над полем Coef – линейное динамическое расширение Monom: )()( wynomPolMMonomwPolynom ++= , . uM =++ 0 Практика использования динами- ческих расширений показала полезность их дальнейшей классификации как линейных и бинарных расширений. Определение 13. Динамическое расширение B алгебры A называется ли- нейным, если в ее конструкторе ),...,,...,( 1 nAAAB τ= в точности один из аргументов совпадает с B . Динамическое расширение B алгеб- ры A называется бинарным, если в ее конструкторе ),...,,...,( 1 nAAAB τ= в точно- сти два аргументы совпадают с B . В примерах 3), 4) рассмотрены линейные динамические расширения. Рассмотрим пример бинарного динами- ческого расширения: 5) числовое поле Rad, элементы которого – суть линейные комбинации квадратных корней натуральных чисел, свободных от квадратов, с рациональными коэффициентами, можно представить как бинарное расширение поля Rat следующей конструкцией. Пусть – последовательность всех простых чисел, расположенных в порядке возрастания. Введем следующие обозначения: ,...,...,, 21 nppp ,...};2,1,, ,*:{, 1 0 =∈ +=== − nRadba pbarrRadRatRad n nn Поле Rad можно представить в виде беско- нечного объединения возрастающей после- довательности полей . nRad (1)10 0 ...Rad...RadRadRat ,RadRad n n n ⊂⊂⊂⊂= = ∞ = U Конструктор Rad имеет вид )2(.*)()( |)( pNatbRadaRad qRatrRad + = Заметим, что (1) – последователь- ность конечных алгебраических расшире- ний полей корнями полиномов . 02 =− npx В представление (2) включены как описание элемента базовой алгебры , так и описание механизма расширения – конструктор qRat pNatbRadaRad *)()( + . Теоретичні та методологічні основи програмування 29 Такая спецификация в точности соответствует определению (1). Формулы (1) непосредственно обобщаются на произвольные динамические рас- ширения. Если алгебра B – динамическое расширение алгебры A с конструктором ),...,,...,( 1 nABAB τ= , возрастающую последовательность определим таким образом: ......10 ⊂⊂⊂ nBBB ,)0( AB = ),...,,...,( )(1)1( nnn ABAB τ=+ . Вложение опреде- ляет вложение , откуда непосредственно следует представление BA:dRe → iii BB:dRe →+1 A в виде объединения возрастающей последовательности алгебр, каждая из которых – статическое расширение предыдущей. ......, 10 0 ⊂⊂⊂⊂= ∞ = n n n BBBBB U . Таким образом, динамические рас- ширения алгебр – суть последователь- ности статических расширений. 3. Верификация вычислений в расширениях многосортных алгебр В работе [11] понятие расширения алгебр используется для синтеза интерпретирующих правил операций и их оптимизации. При этом специфицируются только правила «общего случая». Производные правила выводятся из общих редуцированием – применением функции Red. Таким образом, задача верификации алгебраи- ческих вычислений сводится к задаче обоснования правильности правил «общего случая». Какие свойства присущи «правильным» спецификациям операций? Как отличать «правильные» определения от «неправильных»? Для ответа на эти вопросы нужно проверить выполнение следующих условий: 1) правила спецификации алгебраических операций, определенных конструктивно в спецификациях алгебры, должны удовлет- ворять системе аксиом этой алгебры; 2) результат выполнения операции долж- ны удовлетворять синтаксическим опре- делениям и контекстным условиям конст- руктора сорта. Пример 10. Верификация сорта Boolalg. Сорта Boolalg специфицирует алгеб- ру высказываний многих переменных. Пусть ) – произвольная фор- мула формулы логики высказываний n переменных. Обозначим – соответст- венно истина и ложь. Тогда ,...,,( 21 nxxxF IO, ).,,...,,(& ),,...,(&),...,,( 121 12121 OxxxFx IxxxFxxxxF nn nnn − − ¬∨ ∨= Если обозначить ),,,...,(),...,( ),,,...,(),...,( 1111 1111 OxxFxxB IxxFxxA nn nn −− −− = = получим представление )3().,...,(& ),...,(&),...,,( 111 11121 − − ¬∨ ∨= n nn xxBx xxAxxxxF Выполним последовательно эти преобразования для переменных . В результате получим рекурсивное пред- ставление формулы логики высказываний. Через обозначим множество формул логики высказываний от перемен- ных . Тогда 11,..., xxn− mBoolA lg mxx ,...,1 }.lg, ,&&:{lg 1−∈ ¬∨== m mmm BoolABA BxAxFFBoolA Итак, алгебра Boolalg – объединение возра- стающей последовательности алгебр : mBoolAlg )4(.lglg ....lg...lg ,lg 0 10 0 U ∞ = = ⊂⊂⊂⊂ = m m mg BoolABoolA BoolABoolAlBoolA BoolBoolA Теоретичні та методологічні основи програмування 30 Формула (3) задает рекурсивную каноническую форму формул алгебры высказываний. Обозначим BxAxxBABF df &&),,( ¬∨= . ),,( xBABF – конструктор сорта Boolalg, причем выполнены контекстные условия Интерпретаторы логических операций определяются фор- мулами: ).(),( bArgxAArgx >> )5(),,&,&( ),,(&),,( 2121 2211 xBBAABF xBABFxBABF = = )6(),,,( ),,(),,( 2121 2211 xBBAABF xBABFxBABF ∨∨= =∨ ),,(),,( xBABFxBABF ¬¬=¬ . (7) Это означает, что основные логи- ческие операции выполняются поаргуме- нтно. Легко проверить, что функция вло- жения определяется равенством AxAABF =),,( . Рассмотрим одну из аксиом сорта Bool, например, правило де Моргана BABA ¬∨¬=¬ )&( . Подставив вместо A, B их определения , получаем: ),,(),,,( 2211 xBABFBxBABFA == ).,,(),,( )),,(&),,(( 2211 2211 xBABFxBABF xBABFxBABF ¬∨¬= =¬ Выполним вычисления в левой и правой частях равенства: )8()).,,( )),&(),&(( 2121 2121 xBBAABF xBBAABF ¬∨¬¬∨¬= =¬¬ . Выпишем соответствующие контекстные условия: ))&(()),&(( 2121 BBArgxAAArgx ¬>¬> , )(),( 2121 BBArgxAAArgx ¬∨¬>¬∨¬> . (9) Равенство (8) означает, что доказа- тельство правила де Моргана сводится к доказательству этого правила на аргумен- тах: .)&(,)&( 21212121 BBBBAAAA ¬∨¬=¬¬∨¬=¬ Проверка контекстных условий сводится к доказательству импликации )).&((( ))((&))(( 21 21 AAArgx AArgxAArgx ¬>→ →>> Вывод: Доказательство аксиом алге- бры высказываний осуществляется индук- цией по индексам последовательности (4). Поскольку формулы (5)–(7) сводят вычис- ления логических операций к вычислению этих операций на аргументах, индуктивные рассуждения примера тривиальны. Пример 11. Верификация сорта Polynom. Рассмотрим одну из аксиом сорта Polynom, например, аксиому дистрибу- тивности xzxyzyx +=+ )( . Как и в предыдущем примере, под- ставим вместо zyx ,, их определения: .,, CczBbyAax ++=++=++= Получаем ).)(())(( ))())((( CcAaBbAa CcBbAa +++++++++= =+++++++ Вычислим левую и правую части равенства по правилам сорта Polynom: )).)(( ))((()( ))()()(()( ACaCAc ABaBAbacab CBAcbACBacba +++ ++++++= =++++++++ Контекстные условия имеют вид: ).()(),()( ),()(),()( CDegcDegBDegbDeg ADegaDegcDegbDeg >> >= Требуется доказать acab)cb(a +=+ . (10) )11(),)(())(( )()()( ACaCAcABaBAb CBAcbACBa +++++= =+++++ Теоретичні та методологічні основи програмування 31 . )12().()()(( ))(( CBAcbACBaDeg cbaDeg +++++> >+ Рассмотрим задачу доказательства (12). Это неравенство – следствие правил выполнения операций сложения и умно- жения. Если эти правила правильно оперируют со степенями, оно выполняется автоматически. Поэтому задача доказательства неравенств – контекстных условий аксиом, сводится к задачам доказательства правильности условий в правых частях правил интерпретации операций. В нашем случае нужно доказать: 1) для правила операции сложения: &))()(((&))()(( ADegaDegbDegaDeg >= ));()(( ))()((& BADegbaDeg BDegbDeg +>+→ →> 2) для правила операции умножения: ).)(()( ))()((&))()(( ABAbaBDegabDeg BDegbDegADegaDeg ++>→ →>> Первая из импликаций – следствие общего правила: )).(),(()( 0)( QDegPDegMaxQPDeg QPLeadMon =+→ →≠+ Вторая – следствие правила )()()( QDegPDegPQDeg += . Вывод: доказательство правильно- сти контекстных условий в отдельной операции сводится к доказательству условных неравенств, формулируюмых для данной аксиомы на основании правил вычисления степеней полиномов – резу- льтатов операций. При этом нужно проверять не только основные правила интерпретации, но и производные. Рассмотрим доказательства равен- ств (10), (11). Как и в примере 10, они имеют место с точностью до соотношений вложения сорта: PPMM =++=++ 0,0 , т. е. являются тождествами алгебры многочленов. Но, в отличие от примера 10, равенство (11) не является аксиомой. Его доказательство требует использования аксиом дистрибу- тивности, комутативности и ассоциативности. Таким образом, доказате- льство по индукции осуществляется такой формулировке: 1) базис индукции: для элементов сорта Monom выполняются все аксиомы сорта Polynom; CBAcba ,,,,, 2) предположение индукции: для элеме- нтов сорта Polynom и элементов сорта Monom выполняются все акси- омы сорта Polynom; CBA ,, cba ,, 3) шаг индукции: для элементов CcZBbYAaX ++=++=++= ,, сорта Polynom также выполняются все аксиомы сорта Polynom; 4) вывод индукции: на сорте Polynom выполняются все аксиомы сорта Polynom. Вывод: проверка выполнения отде- льной аксиомы (например, дистрибутив- ности) на элементах сорта Polynom сводит- ся к проверке выполнения всей системы аксиом на аргументах конструктора сорта. Поэтому доказательство осуществляется в вышеуказанной форме только для основных правил интерпретации операций. Пример 12. Верификация сорта Rat. Рассмотрим задачу проверки выполнения аксиомы дистрибутивности для сорта Rat. На множестве Int×Nat должна быть определена конгруэнтность, выделяющая равные пары аргументов (числитель, знаменатель) конструктора сорта Rat. Эта конгруэнтность имеет вид )~,//,//( 12212211 qpqpbaqpbqpa =↔== . Для элементов сорта Rat имеет место соотношение )13()1),((& &)(&)///( = == srGCD rqpssrqp Рассмотрим доказательство дистри- бутивности. Пусть acabcba +=+ )( и 332211 //,//,// qpcqpbqpa === . Теоретичні та методологічні основи програмування 32 Подставив значения в аксио- му дистрибутивности и вычислив левую и правую части равенства по правилам из спецификаций Rat, получаем: cba ,, )./()( )/()( 312131212131 32132321 qqqqppqqppqq qqqpqqpp += =+ Для упрощения выражений введем обозначения: ., ,),( 312131212131 32132321 qqqqDppqqppqqC qqqBpqqppA =+= =+= Верификация аксиомы дистрибу- тивности сводится к проверке тождества над сортом Int и доказательстве (13). Доказательство тождества верифи- цирует данную аксиому, а доказательство (13) верифцирует интерпретатор конс- труктора сорта Rat. BDAC = Алгоритмы верификации алге- браических вычислений в рас- ширениях алгебр. Рассмотрим алгебры >Σ=< AAAAAA ITUSA ,Ax,,,, , (14) . >Σ=< BBBBBB ITUSB ,Ax,,,, Верификация в статических расширениях. Обобщим метод вери- фикации системы алгебраических программ – интерпретаторов операций сорта из его спецификаций при условии, что алгебра v B сорта – статическое расширение алгебры v A сорта : u .,, BAABAA v df u df ⊂== Спецификации сорта v определяют: Конструктор сорта: ),( Wuv τ= . Обяза- тельным аргументом τ является сорт . u Контекстное условие: ).,( Wuπ Условие вложения: ),( Wuρ . Функция вложения: uWuWu =→ ),(),( τρ . Предикат ),( Wuρ функционален: для каждого значения существует единст- венное значение u P такое, что ),( Wuρ . Эту функцию будем обозначать : ρF ))((),( WuFWu p ==ρ . Интерпретатор конструктора сорта: yPx =),(!τ . Вызов интерпретатора ),(! Pxτ , обозначенный восклицательным знаком как префиксом имени функции, делает истинным предикат ).,( Pxπ Конгруэнция конструктора сорта: Конгруэнция Θ на множестве kwwu SSS ××× ... 1 : определяет условие на аргументах конст- руктора сорта: ),...,,(),...,,( '' 1 ' 1 kk ppxppx Θ ≈ если )','(),( PxPx ττ = , то . )','(),( PxPx Θ ≈ Нетрудно видеть, что конструкция элемента сорта является канонической формой. Поэтому эта конгруэнция опреде- ляет классы эквивалентности элементов kwwu SSS ××× ... 1 , имеющих одну и ту же каноническую форму. Cигнатуры операций сортов: сорта u: >=<Σ mu ϕϕ ,...1 ; сорта v: >=<Σ lmv ψψϕϕ ,...,,,... 11 . Мы считаем, что сигнатура операций рас- ширения B – расширение сигнатуры опера- ций базовой алгебры A. Аксиомы сортов сорта u: >=< su AAAX ,...1 ; сорта v: >=< '1,..., sv BBAX . Мы считаем, что система аксиом B – рас- ширение системы аксиом алгебры A. Спецификации операции mϕϕ ,...1 заданы системами равенств. Верификация интерпретаторов опе- раций алгебры B заключается в: доказательстве тотальной корректности интерпретатора функции ),(! Pxτ ; доказательстве тождеств над алгеброй A – следствий аксиом и конгруэнции BAX Θ конструктора алгебры B . Доказательство частичной коррек- тности интерпретатора ),(! Pxτ опирается на его представление в виде суперпозиции функций построения канонической формы аргумента как элемента носителя алгебры ),( Px B и применении вложения к этой форме: )),((!),( xPxPx =→ τρ . Теоретичні та методологічні основи програмування 33 Обозначим canτ функцию, которая возвращает аргумент как элемент носителя алгебры ),( Px B , а redτ – функцию вложения )),((!),( xPxPx =→ τρ . Тогда )),((),(! PxPx canred τττ = . Частичную корректность ),(! Pxτ можно доказать, доказав импликации )15(,))','(&))','(~),(( ))','(),(( PxPxPx PxPxcan π τ Θ → →= )16())).(,(&))(,(~),(( )),((&),( xFxxFxPx xPxPx red ρρ Θ π τρ → →= Определение 14. Расширение алгебры называется прямым, если функция BA⊂ canτ является тождественной. Элемент носителя прямого расши- рения B – произвольный элемент , а конгруэнция еди- нична. Таким образом, при прямых расширениях доказывать нужно только корректность вложения . Расширение примеров 10, 11 прямые. Расширение (пример 12) не является прямым. kwwu SSS ××× ... 1 Θ BA→ 1+⊂ ii AA RatInt → Рассмотрим доказательста тож- деств. Тождества над A , являющиеся следствиями аксиом и конгруэнции , получаются следующим образом: если BAX Θ Bnn df i AXPxxRPxxLB ∈== )),,...,(),,...,(( 11 , причем переменные определены над xxx ,...,1 B , подстановки ),( ii Puτ вместо определяют равенства над . Формальное выполнение интерпретаторов операций алгебры ix kwwu SSS ××× ... 1 B в левой и правой частях равенства ),),,(),...,,(( )),,(),...,,(( 11 11 PPuPuR PPuPuL nn nn ττ ττ = = приводит к равенству ),...,,'(),,,,( '' 11 kk GGfGGf ττ = , где ),,..,,,..,( 11 PPPuuff nn= , ),,..,,,..,('' 11 PPPuuff nn= , ),,,..,,,..,( 11 PPPuuGG nnii = . ),,,..,,,..,( 11 '' PPPuuGG nnii = ni ,..,1= Итак, имеет место отношение эквивалентности ),...,,'(),,,,( '' 11 kk GGfGGf Θ = . (17) Это отношение зависит от перемен- ных . Будем считать, что конгруэнтность PPPuu nn ,,..,,,.., 11 Θ задана системой тож- деств .,..,1, ejWV jj == Тогда верификация интерпретаторов операций алгебры B состоит в доказательстве тождеств )18(,,..,1),,,..,,,..,( ),,..,,,..,( 11 11 ejPPPuuW PPPuuV nnj nnj == = над базовыми сортами . Алго- ритм доказательства (18) должен опираться на аксиомы базовых сортов. Поэтому этот алгоритм существует, если проблема тождества над базовыми алгебрами алгоритмически разрешима. kwwu ,...,, 1 Если расширение – прямое, тождества (18) “покоординатные”. Поэто- му конгруэнтность (17) определяет тожде- ства BA⊂ .,..,1,,' ' kiGGff ii === (19) Верификация в динамических рас- ширениях. Обобщим метод верификации системы интерпретаторов операций сорта при условии, что алгебра – динами- ческое расширение алгебры v vA A . Пусть iiii ABAAAAA ∞ =+ ∪=== 0010 ),,(, τ – спецификация конструкции линейного динамического расширения BA⊂ . XXxXxAXAx redi =→∈∈ ),(),(,,0 τρ Теоретичні та методологічні основи програмування 34 – вложения, определенные для элементов этого расширения. iA Как и для статических расширений, система аксиом B – расширение системы аксиом базовой ал- гебры A. Это означает, что этой системе должны удовлетворять все алгебры . Тогда: iA – верификация функции τ! проводится индукцией по индексу и состоит в доказательстве импликаций (15), (16); i – верификация интерпретаторов опе- раций на B с помощью аксиом осущест- вляется индукцией по индексу и состоит в доказательстве тождеств (19) над алгебрами в индуктивном предположении, что все аксиомы доказаны как тождества алгебры . Если алгоритм доказательства на базовой алгебре использует только аксиомы i 1+iA iA AA =0 A , индукция позволяет расширить этот алгоритм на B . Метод расширений используется, как правило, для пределения новых операций. Например, сорт Int расширяется до Rat с целью определения операции деления (пример 12). Сорт Polynom расширяется как векторное пространство. Для этого сорт Monom рассматривается как одномерное векторное пространство, а шаг расширения состоит в добавлении новой координаты. В этом примере – i - мерное векторное пространство. Операции умножения на скаляр, сложение и вычитание, а также все аксиомы векторного пространства удов- летворяют рассмотренному методу. Однако операция умножения многочленов и все аксиомы, содержащие умножение, должны быть рассмотрены отдельно. iA Пусть PolynomQPRQP ∈= *,, , , jQiP == deg,deg }deg:{ kppAk ≤= . Тогда . Итак, если . jiR +=deg jiji AQ*P,AQ,AP +∈∈∈ Верификация операции умножения методом математической индукции, выше- рассмотренная, сводит доказательство ак- сиом на к доказательству тождеств на . Поэтому базис индукции должен содержать доказательство аксиом как тож- деств на базовых алгебрах, т. е. на моно- мах. Например, в (12) нужно считать, что jiA + 1−+ jiA .,,,,, MonomCcBbAa ∈ . Обобщим эти соображения на про- извольные алгебры. Метод индукции при- меним, поскольку степень произведения является монотонно возрастающей функ- цией степеней множителей. Сформулируем это в общем для бинарных операций. Пусть iiii ABAAAAA ∞ =+ ∪=== 0010 ),,(, τ и ),( baϕ - бинарная операция, определен- ная на алгебре B . Тогда, если существует такая монотонно возрастающая по каждому из аргументов функция , что для произвольных ),( jis ji AbAa ∈∈ , , ),(),( jisAba ∈ϕ метод индукции сводит до- казательство аксиом алгебры B , содер- жащих операцию ,ϕ к доказательству этих аксиом для переменных, определенных на алгебре .A Выводы Наш подход к верификации алгебра- ических вычислений характеризуется та- кими особенностями. 1. Определение иерархии зависимо- стей сортов позволяет упорядочить про- цесс построения и верифиции новых сор- тов с целью расширения функциональ- ности системы компьютерной математики. 2. Включение в спецификации сор- тов аксиом и интерпретаторов операций позволяет использовать аксиомы для вери- фикации интерпретаторов операций. 3. Определения сортов как конст- руктивных расширений позволяет сводить задачи верификации сорта к верификации вычислений в базовых сортах. 4. Классификация расширений как статических и динамических позволяет Теоретичні та методологічні основи програмування 35 определять и использовать либо прямой, либо индуктивный метод верификации. 5. Данный подход особенно эффективен при реализации вычислений в алгебрах, аксиоматика которых хорошо известна и полна. 1. Kapitonova J., Letichevsky A., Lvov M., Volkov V. Tools for solving problems in the scope of algebraic programming // Lectures Notes in Computer Sciences. – 1995. – N 958. – P. 31–46. 2. Львов М.С. Основные принципы постро- ения педагогических программных средств поддержки практических занятий // Управляющие системы и машины. – 2006. – № 6. – C. 70–75. 3. Песчаненко В.С. Об одном подходе к проектированию алгебраических типов данных // Проблеми програмування. – 2006. – № 2–3. – С. 626–634. 4. Lvov M., Kuprienko A., Volkov V. Applied Computer Support of Mathematical Training // Proc. of Internal Work Shop in Computer Algebra Applications, Kiev. – 1993. – P. 25–26. 5. Lvov M. AIST: Applied Computer Algebra System // Proc. of ICCTE’93. – Kiev. – P. 25–26. 6. Львов М.С. Терм VII – школьная система компьютерной алгебры // Компьютер в школе и семье. – 2004. – № 7. – С. 27–30. 7. Песчаненко В.С. Расширение стандарт- ных модулей системы алгебраического программирования APS для использования в системах учебного назначения // Компьютерно-ориен- тированные системы обучения: – Киев: НПУ им. М.П. Драгоманова.– 2005. –№ 3(10). – C. 206–215. 8. Letichevsky A., Kapitonova J., Volkov V., Chugajenko A., Chomenko V. Algebraic programming system APS (user manual). // Glushkov Institute of Cybernetics, National Acad. of Sciences of Ukraine. – Kiev, 1998. – 50 р. 9. Капитонова Ю.В., Летичевский А.А., Волков В.А. Дедуктивные средства системы алгебраического программиро- вания // Кибернетика и системный анализ. – 2000. – № 1. – С. 17–35. 10. Песчаненко В.С. Использование системы алгебраического программирования APS для построения систем поддержки изучения алгебры в школе // Управляющие системы и машины. – 2006. – № 4. – С. 86–94. 11. Львов М.С. Синтез интерпретаторов алгеб- раических операций в расширениях много- сортных алгебр // Вісник Харьківського національного університету. – 2009. – № 847. – С. 221–238. 12. Ван дер Варден Б.Л. Алгебра. Изд. 2-ое. – М.: ГРФМЛ, 1979. – 624 с. 13. Goguen J., Meseguer J. Ordered-Sorted Algebra I: Partial and Overloaded Operations. Errors and Inheritance // Theoretical Computer Science. – Oxford: Elsevier, 1992. – Vol. 105 (N 2). – P. 217–273. 14. Дж. А. Гоген, Ж. Мезегер. Модели и ра- венство в логическом программировании // Математическая логика в программиро- вании. – М.: Мир, 1991. – C. 274–310. Получено 16.05.2011 Об авторе: Львов Михаил Сергеевич, кандидат физико-математических наук, доцент, профессор кафедры информатики. Место работы автора: Херсонский государственный университет, ул. 40-лет Октября, 27. Херсон, Украина,73000. Тел.: (0552) 32 6781. Факс.: (0552) 32 6785. lvov@ksu.ks.ua

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