М.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 tra

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)

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

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

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

Traditional logical canonical forms are PDNF, PCNF.
We shell use Recursive Normal Form (RNF).
Paradigm of Algebraic Computations
(3)

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

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

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

Method of Extensions
Axiomatic definition of sort AlgLogic is initial for further development.
Three constructive models of AlgLogic:
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

Additional Rules (partial cases):
In the rule (10) suppose A1 = B1. then obtain:
A1 ∨ L(A2, B2 , x) = L(A1, A1, x) ∨ L(A2, B2 , x) = L(A1 ∨ A2, A1 ∨ B2, 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).

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)
};

Main Result of Extension’s 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(A1, B1, x) ∨ L(A2, B2 , x) = L(A1 ∨ A2, B1 ∨ B2, x), // base
Var(A1 ) < x ? A1 ∨ L(A2, B2 , x) = L(A1 ∨ A2, A1 ∨ B2, x), // additional
Var(A2 ) < x ? L(A1, B1, x) ∨ A2 = L(A1 ∨ A2, B1 ∨ A2, x)
};