М.Lvov About one Approach for Designing of Algebraic Computations: Computations in Boolean Algebra. Designing of algorithms for algebraic computations. - презентация

1 М.Lvov About one Approach for Designing of Algebraic Computations: Computations in Boolean Algebra. Designing of algorithms for algebraic computations – the main task arising when realising mathematical systems based on symbolic transformations Mathematical model for this problem – multisorted algebraic systems (MAS) The process of realising of algebraic computations needs carefull preliminary design MAS as hierarchy of its sorts and specifications of algebraic operations interpreters

2 Theory and detailes in: Lvov М.S. Synthesis of Interpreters of Algebraic Operations in Extensions of Multisorted Algebras. (ukr, prepared for print) Lvov М.S. Veryfication of Interpreters of Algebraic Operations in Extensions of Multisorted Algebras. (prepared for print) Lvov М.S. Method of Inheritance for design of algebraic computations in mathematical educational systems. (ukr, prepared for print) Lvov М.S. Method of Morphisms for design of algebraic computations in mathematical educational systems. (ukr, prepared for print)

3 Approach IEM Inheritance, Extensions, Morphisms Base principles and ideas of IEM are quite simple and well known in mathematics and programming Boolean algebra is very simple, well known and interesting example of subject domain for applying of IEM

4 Algebraic programming system APS (V. Peschanenko) APS uses technologies of algebraic programming, based on rewriting rules systems and strategies of rewriting. The interpreter of algebraic operation defined by rewriting rules system. We shall consider problems: of design, synthesis, verification of interpreters of boolean algebra operations (logical operations).

5 FG Can(F) = Can(G) Syntax equality Semantic (logical) equality Compute the value of logical expression in signature of logical operations By the value of expression we means its canonical form i.е. such expression that Sign «=» means syntax equality (equality in free terms algebra) (1) (2) Problem Definition

6 Traditional logical canonical forms are PDNF, PCNF. We shell use Recursive Normal Form (RNF). Paradigm of Algebraic Computations Initial Model B.A. Constructive Model В.A. Can Val (3)

7 Method of Inheritance In algebraic computations are used: Classical (axiomatically of constructively defined) algebraic structures, Algebraic structures, defined by designer Logical Designing of algebraic computations consists in defining of hierarchy of inheritance of MAS

8 ConSemigroup10: Signature Semigroup10: Signature Axioms DisSemigroup10: Signature AlgLogic: Signature Axioms Рис. 3. Diagram of Inheritance for Boolean Algebra

9 Axiomatic descriptions plays constructive role. Its defines signatures, computations with constants. Inheritance is used for definitions of algebraic operations interpreters with constants SGOperation := rs(a) { a 1=a, 1 a=a, a 0=0, 0 a=0 }; Dis := rs(a) { a O = a, O a = a, a I = 0, I a = I }; Con := rs(a) { A&I = a, I&a = a, A&O = 0, O&a = O };

10 Аbstract Algorithms Inheritance is used for descriptions of algorithms on abstract level (independently of algebras support). Example: Euclids Algorithm (abstract Euclidian ring). Derived logical operations Imp := rs(a, b) { a b = ¬a b }

11 Method of Extensions Axiomatic definition of sort AlgLogic is initial for further development. Three constructive models of AlgLogic: AlgLogic ALInitALConst r Bool Variable Initial diagram of Method of extentions for Boolean algebra. Important: Constructive definition of algebra A consists in definitions of its support Sup(A), interpreters of its operations

12

13

14 Define for L(A 1, B 1, x), L(A 2, B 2, x) A(x), A 1, B 1, A 2, B 2 A. Base rules: L(A 1, B 1, x) L(A 2, B 2, x) = L(A 1 A 2, B 1 B 2, x), (10) L(A1, B1, x) & L(A2, B2, x) = L(A1 & A2, B1 & B2, x), (11) L(A1, B1, x) = L( A1, B1, x). (12) Rules (10) - (12) are base for operations on logical operations. Let

15 Additional Rules (partial cases): In the rule (10) suppose A 1 = B 1. then obtain: A 1 L(A 2, B 2, x) = L(A 1, A 1, x) L(A 2, B 2, x) = L(A 1 A 2, A 1 B 2, x). This equality defines the conditional rewriting rule Var(A1 ) < x A1 L(A2, B2, x) = L(A1 A2, A1 B2, x). (10a) Analogously L(A1, B1, x) A2 = L(A1, B1, x) L(A2, A2, x) = L(A1 A2, B1 A2, x). Var(A2 ) < x L(A1, B1, x) A2 = L(A1 A2, B1 A2, x) (10b) Rules (10), (10а), (10b) forms rewriting rules system of interpreter of disjunction for operands of the form L(A, B, x).

16 Dis := rs(A1, B1, A2, B2, x) { L(A1, B1, x) L(A2, B2, x) = L(A1 A2, B1 B2, x), Var(A1 ) < x A1 L(A2, B2, x) = L(A1 A2, A1 B2, x), Var(A2 ) < x L(A1, B1, x) A2 = L(A1 A2, B1 A2, x) }; Con := rs(A1, B1, A2, B2, x) { L(A1, B1, x) & L(A2, B2, x) = L(A1 & A2, B1 & B2, x), Var(A1 ) < x A1 & L(A2, B2, x) = L(A1 & A2, A1 & B2, x), Var(A2 ) < x L(A1, B1, x) & A2 = L(A1 & A2, B1 & A2, x) }; Not := rs(A1, B1, x) { L(A1, B1, x) = L( A1, B1, x) };

17 Main Result of Extensions Method Definition of algebra as direct limit of increasing sequence of algebras in issue gives the algorithm of synthesis of interpreters for algebraic operations Full rewriting ruses systems for logical operations: Disjunction Dis := rs(a, A1, B1, A2, B2, x) { a O = a, O a = a, // Inherited a I = 0, I a = I, L(A 1, B 1, x) L(A 2, B 2, x) = L(A 1 A 2, B 1 B 2, x),// base Var(A 1 ) < x A 1 L(A 2, B 2, x) = L(A 1 A 2, A 1 B 2, x), // additional Var(A 2 ) < x L(A 1, B 1, x) A 2 = L(A 1 A 2, B 1 A 2, x) };

18

19

20

21

22 Литература 1.Lvov M., Kuprienko A., Volkov V. Applied Computer Support of Mathematical Training Proc. of Internal Work Shop in Computer Algebra Applications, Kiev. – – pp Lvov M. AIST: Applied Computer Algebra System Proc. of ICCTE93. Kiev. – pp Львов М.С. Терм VII – шкільна система компютерної алгебри Компютер у школі та сімї. – – 7.- С М.Львов. Концепция информационной поддержки учебного процесса и ее реализация в педагогических программных средах. Управляющие системы и машины N2 (в печати). 5.Львов М.С. Синтез інтерпретаторів алгебраїчних операцій в розширеннях багатосортних алгебр (підготовлено до друку) 6.Львов М.С. Верифікація інтерпретаторів алгебраїчних операцій в розширеннях багатосортних алгебр (підготовлено до друку) 7.М.С.Львов. Метод спадкування при реалізації алгебраїчних обчислень в математичних системах навчального призначення (підготовлено до друку) 8.Львов М.С. Метод морфізмів реалізації алгебраїчних обчислень в математичних системах навчального призначення (підготовлено до друку) 9.Goguen J., Meseguer J. Ordered-Sorted Algebra I: Partial and Overloaded Operations. Errors and Inheritance. SRI International, Computer Science Lab., Песчаненко В.С. Розширення стандартних модулів системи алгебраїчного програмування APS для використання у системах навчального призначення // Науковий часопис НПУ імені М.П. Драгоманова Серія 2. Компютерно-орієнтовані системи навчання: Зб. наук. Пр./Редкол.- К.:НПУ ім.М.П.Драгоманова, - 3 (10), C Песчаненко В.С. Об одном подходе к проектированию алгебраических типов данных // Проблеми програмування С Песчаненко В.С. Использование системы алгебраического программирования APS для построения систем поддержки изучения алгебры в школе // Управляющие системы и машины С 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, Ukraine, Капитонова Ю.В., Летичевский А.А., Волков В.А. Дедуктивные средства системы алгебраического программирования, Кибернетика и системный анализ, 1, 2000, Kapitonova J., Letichevsky A., Lvov M., Volkov V. Tools for solving problems in the scope of algebraic programming. Lectures Notes in Computer Sciences. – 958. – – pp Львов М.С. Основные принципы построения педагогических программных средств поддержки практических занятий. Управляющие системы и машины N6. c