Development of algorithms of algebraic computations is one of the main problems, which arises with realization of mathematical software based on symbolic transformations. Multi-sorted algebraic systems (MAS) are mathematical model for this problem. Present paper deals with the solution of this problem. We propose the approach to realization of interpreters of multi-sorted algebraic operations by its specifications, based on constructive improvement of notion of extension of multisorted algebraic system. This approach is illustrated by examples of realization of interpreters of operations in the field of rational numbers, ringing of one variable polynomial over the field, algebra of Boolean functions. Practice of this approach using for development of mathematical educational software shows its effectiveness and even universality.
Development of algorithms that perform algebraic computations is one of the main
problems that arise when one implements mathematical systems based on symbolic
transformations. A mathematical model of this problem is the notion of a multi-sorted
algebraic system (MAS). The practice of development of simple educational
mathematical systems [
APS uses an algebraic programming technology based on rewriting systems and rewriting strategies. Thus, an interpreter of an algebraic operation is defined by a system of rewriting rules.
In the paper we propose an approach to implementing interpreters of multi-sorted algebraic operations in accordance with their specifications which is based on the constructive refinement of the concept of an extension of a multi-sorted algebraic system. The definitions of a MAS and its (constructive) extension are given in paragraph 1. A typical example of a constructive extension is the example of the field of rational numbers as an extension of the ring of integers (example 2).
Constructive MAS extensions are classified as static, linear or binary dynamic extensions (definition 1.3.1, 2.1.).
We show that an interpreter of an algebraic operation in a constructive extension can be synthesized automatically in accordance with its specification which defines the rules of interpretation of the operation in extension, and the conditions of embedding of the base algebra in its extension.
The algorithm of synthesis of an interpreter of an operation is determined by the type of an extension. Therefore, in paragraph 2.2 we give examples of implementation of interpreters of operations of the field of rational numbers (static extensions), quadratic radicals field (binary dynamic extensions), univariate polynomial rings (linear dynamic extensions) and the algebra of propositions (binary dynamic extensions). 1.1
Definition 1.1. Let U = {u1, …, uk} be a finite set of symbols which is called the sorts signature. The symbols ul, l ∈{1,…, } are called the names of sorts, or simply the sorts.
In particular, we will use the following sort names: Variable, Bool, Nat, Int, Real.
We will introduce other sort names within the definitions of the appropriate algebraic notions.
Definition 1.2. Let S {Su1 ,...,Suk } be a finite family of sets indexed by sort names, the elements of which are called the value ranges of the corresponding sorts: ─ SVariable is the set of variables, ─ SBool is the set {False, True}, ─ SNat is the set of natural numbers, ─ SInt is the set of integers, ─ SReal is the set of real numbers.
Definition 1.3. A multi-sorted operation f on a family S is a map f : Su1 Su2 ...S um Sv , where u1,...,um, v U are sorts of arguments and values of the operation f, respectively, and m is the arity of f.
The type of an operation is determined by the list of names of sorts of its arguments and the name of the sort of its range of values. The type of an operation f will be denoted as (u1,...,um ) v . A signature Σ of operations is a finite set of symbols of operations together with a map that associates with each symbol a multisorted operation f together with its type (if is a symbol of an operation, then the expression : (u1,...,um ) v that this symbol is associated with an operation of the type (u1,...,um ) v ).
An example of a multi-sorted operation is scalar multiplication in a vector space. If VectorSpace is the sort name of a set of vectors over the field Real of real numbers, then the multiplication operation Mult “*” defines the map
Below we will use more common, traditional mathematical notations for operations. Since the infix notation is usually used for scalar multiplication, we have:
Definition 1.4. Let Bool be a sort with the value range SBool {True, False} . A multi-sorted predicate P is a mapping P : Su1 ... Sum SBool , where u1,...,um U , the sequence u1, …, um determines the type of the predicate, and the number m is its arity. A signature Π of multi-sorted predicates is defined analogously to the signature of operations as a set of operations of predicate symbols, associated with multi-sorted predicates together with their types.
Definition 1.5. A multi-sorted algebraic system A is a tuple A=<S, U, Σ, Π >, where S is a set of sorts indexed by the symbols of the set U, {1,...,l} is a signature of multi-sorted operations, Π = {π1, …, πp} is a signature of multi-sorted predicates.
Remark. Since the sort Bool can be added to the set of sorts, predicates can be considered as multi-sorted operations. Therefore, instead of considering multi-sorted algebraic systems, we will combine the signatures of operations and predicates and consider multi-sorted algebras.
Definition 1.6. Let A=<S, U, Σ > be a multi-sorted algebra and u, v U be sort symbols. We will say that the sort v depends on the sort u, if one of the operations of the signature Σ has the type of the form u1 ...u ...um v . As Uv denote a subset of sorts which depend on the sort v. Denote the subset of elements of Σ of type u1 ...u ...um v as Σv, and the family of ranges of values of sorts Uv as Sv. A restriction Av of a multi-sorted algebra A to a sort v is the multi-sorted algebra Av=<Sv, Uv, Σv>.
Thus, a multi-sorted algebra A can be represented by a set of restrictions (algebras) Av, v ∈ U, that A Au1 ,...,Auk .
Consider a software system that implements simplification of algebraic and trigonometric expressions. The core of the system must implement the computations in the ring of polynomials and the ring of multivariate trigonometric polynomials over the field of rational numbers. Specifications shall be given for the following algebras – restrictions to the mentioned sorts:
For constructing algebras Au we use their axiomatic and constructive descriptions (definitions).
Horizontal line is a symbol of the sort constructor. The same mathematical symbol is used to denote the operation of division, in particular in Rat. This is not convenient for the tasks of specification of algebraic computations. Therefore, we introduce the concept of a signature of operations Σ and a signature of constructors T. In particular, for denoting the constructor of the sort Rat we will use double forward slash: SPolynom {Q : Q M P, M SMonom, P SPolynom,
df degQ degM;deg(M ) deg(P)} SMonom
SRat {p // q : p SInt , q SNat,GCD( p, q) 1}
An important factor is that in the standard forms of presentation of elements of sorts the syntactic aspects of the definition are always combined with semantic aspects defined as contextual conditions i.e. predicates. In our case such a predicate is the equality GCD(p, q) = 1.
Example 3. The ring Polynom univariate polynomials over the field Rat.
Elements of this field are polynomials represented as sums of monomials, written in descending order of degrees. This definition should be recursive, and the concept of degree has to be defined separately.
To define the carriers of sorts we will use a special specification language, which allows non-recursive and recursive syntactic definitions of sorts’ elements, definitions of the access functions and contextual conditions. For example: Rat r ={(Int a)//(Nat b); // Constructor of sort Num(r) = a, Den(r) = b; // Access functions
GCD(a, b) = 1 // Contextual condition }; Monom M = {(Rat c)$(Const Variable x)^^(Nat n); Coef(M) = c, Var(M) = x, Deg(M) = n // Access functions }; Polynom P = {(Monom M)++(Polynom Q); // Constructor LeadMon(P) = M, // Access functions LeadCoef(P) = Coef(M), Deg(P) = Deg(M); Deg(P) > Deg(Q) // Contextual condition };
In order to implement computations in an algebra Av, v in U, it is necessary to implement algorithms for performing each of its operations in such a way that the axioms of the algebra are satisfied.
Definition 1.9. An interpreter of an operation of a signature Σu is a function which is implemented by an algorithm which performs the corresponding operation.
Interpreters of operations are defined using a programming language. For our purposes we use APLAN language. So we include this language in the specification language.
Thus, for axiomatic and constructive description of an algebra Av to its definition we add a finite set of axioms Axv and finite set of interpreters Iv. Then a multi-sorted algebra Av is defined as follows: Av= <Sv, Uv, Tv, Σv, Axv, Iv>. 1.3
Construction of the structure of multi-sorted algebras means specification, prototyping and implementation of algebraic computations. Specification of the structure of multi-sorted algebra is done in terms of extensions, homomorphisms, isomorphism and inheritance of multi-sorted algebras. Thus, together with the diagrams of dependence, which are graphical models of specifications of signatures of operations and constructors, the diagrams of extensions, diagrams of morphisms (isomorphism and homomorphism) and diagrams of inheritance are designed. We consider the method of extension. The methods of morphisms and inheritance are beyond the scope of this work.
Definition 1.10. Let Au and Av be multi-sorted algebras. A multi-sorted algebra Av is called an extension of Au, if Su Sv and for any pair of operations f1, f2 of types f1 : (u1,...,um ) u and f2 : (v1,...,vm ) v respectively, if Su1 Sv1 ,...,Sum Svm , then (a1,...,am ) Su1 ... Sum the equality f1(a1,...,am) f2 (a1,...,am) holds.
An embedding is an isomorphic map Red : Su S'v , which maps Su onto a subset S'v Sv . A restriction of an algebra Av to a subset _ isomorphic to Au, is determined by a system of conditional identities E1(x),...,Ek (x) : Sv {a Sv | E1(a),...,Ek (a)}. The use of the system E1(x),...,Ek (x) as a rewriting system «simplifies» the term a S'v to a term a Su : Red 1(a) a' .
A constructive description of an extension Av means a description of a constructor of Av and an embedding of Au into an algebra Av. In Figure 2 the double arrow indicates that Av is an extension of the algebra Au, in Av the construct v (u1,...,u,...,um ) and embedding Redu,v are defined.
Note. The relation of MAS extension (the relation “sort-subsort”) is basic in this work. Multi-sorted algebras, partially ordered by this relation, are called sortedordered. The fundamentals of the theory of sorted-ordered algebra in the applications to the theory of programming are presented in [12]. In Russian they are stated in [13].
Example 4. Consider the constructor of the field Rat (Example 2). According to the definition it defines a construct Rat, the arguments of which are sorts Int and Nat. Let us complement the specification of Rat sort by the embedding Red : Rat Int , defined by the equality Red(a //1) a . Thus the sort Rat is defined constructively as an extension of sort Int.
Now consider the constructor of the Polynom ring (Example 3). It defines a recursive construct Polynom, the arguments of which is the sort Monom. Let us complement the specification of the sort Polynom with an embedding Red : Polynom Monom, defined by the equality Red(M 0) M . So the sort Polynom is defined as an extension of the sort Monom.
In turn, the sort Monom is an extension of the sort Degree with a function Red defined by the equality 1$x^^k = x^^k, extension of the sort LinMonom with a function Red defined by the equality a$x^^1 = a$x and extension of Rat with a function Red defined by the equality a$x^^0 = a. The Sorts Degree and LinMonom are extensions of the sort Variable with the functions of reduction, specified in accordance with the following equalities x^^1 = x and 1$x = x. Thus, the extensions diagram has the following form
The extension mechanism is one of the main methods of specification of multisorted algebras. In particular, it allows defining the overloaded algebraic operations and algebraic type casting functions.
Definition 2.1. An extension B of an algebra A is called static (non-recursive), if in its constructor B (A1,...,A,...,An ) none of the arguments coincides with B.
Examples of static extensions:
The field Rat is a static extension of the ring Int. Actually, Rat R (Int A) //(Nat B)
The semigroup of monomials Monom with one generator is a static extension of the coefficients Coef field, because MonomM (Coef a)$(Var x)^(Nat N) .
Definition 2.2. An extension B of an algebra A is called dynamic (recursive), if in its constructor B (A1,...,A,...,An ) at least one of the arguments coincides with B.
A constructor of a dynamic extensions is a recursive definition, and therefore, contains both the base and recurrent part.
A vector space LinComb of linear combinations of several variables over a field Coef is a linear dynamic extension of LinMonom, an element of which has the form a$x. An element w LinComb has a form w a1$x1 a2$x2 ... am$xm .
An univariate polynomial ring Polynom over the field Coef. This ring is traditionally denoted as F[x].
Polynom w = (Monom M)++(Polynom w)
Definition 2.3. A dynamic extension B of an algebra A is called linear, if in its constructor B (A1,...,A,...,An) exactly one of the arguments coincides with B.
A dynamic extension B of an algebra A is called binary, if in its constructor B (A1,...,A,...,An) exactly two of the arguments coincide with B.
Example 5. The field of square radicals
Examples 3 and 4 are examples of linear dynamic extensions. Consider an example of a dynamic binary extension:
The field Rad, the elements of which are linear combinations of square roots of square-free positive integers with rational coefficients, can be represented as a binary extension of Rad using the following construction. Let p1,p2,…,pn… is a sequence of all prime numbers arranged in ascending order. Denote as Q the field of rational numbers. We introduce the following notations:
Rad0 Q, Radn {r : r a b* pn , a,bRadn1,n 1,2,...}.
The field Rad is the union of the increasing sequence Radn of fields.
Rad Radn , Rat Rad0 Rad1 ... Radn ...
n0 Thus, the constructor Rad has the form
Rad r (Rad a) (Rad b) * Nat p |(Rat q) (4) (5) (6) (7) (8)
Note that sequence of extensions (4) is a sequence of finite algebraic extensions of fields with roots of polynomials x2 pn 0 .
Representation (5) includes a description of basic elements Rat q and a description of the extension mechanism - the constructor (Rad a) (Radb) * Nat p . This specification exactly corresponds to the definition (4). On the other hand, the basic element description is unnecessary if it can be got from the embedding. Indeed, the specification of the LinComb vector space with the inclusion of the item describing of the elements of the basic algebra LinMonom has the form
LinComb w (LinMonomu) (LinComb w)|(LinMonomu)
However, the inclusion LinMonom LinComb is defined by the equality u ++ 0=u. Therefore a separate description LinMonom u is unnecessary. We admit both types of specifications.
Formula (4) can be directly generalized to arbitrary dynamic extensions. If an algebra B is a dynamic extension of the algebra A with the constructor B (A1,...,B,...,An ) , the increasing sequence B0 B1 ...Bn ... is defined as follows:
B(0) A, B(n1) (A1,...,B(n) ,...,An )
B Bn , B0 B1 ... Bn ...
n0
The embedding Red : A B defines the embedding Redi : Bi1 Bi , from which one obtains a representation of A in the form of an increasing sequence of algebras, where each one is a static extension of the previous one.
In MAS development practice there were some generalizations of the definition (8). Namely, instead of the sequence of algebras {Bi}i0 let consider the set of indexed algebras{Ai}iI , where I is a linearly ordered set of indices. An algebra BJ , J I, J is defined as a union of algebras Aj, j J : BJ jJAj . Let us assume there is an embedding of algebras Bj, where BJ1 BJ2 BJ1J2 . Then
B BJ
JI, J K[[x]]{P: P
ajxj jJ,JRat, J
(9) (10)
An example of such algebra is a ring K[[x]], the elements of which are sums of monomial with rational degrees:
Dynamic extensions are sequences of static extensions. This allows one to use the general scheme of implementation of dynamic extensions to derive the appropriate rewriting systems. 2.2
Example 7. Below is a specification of Rat sort and a derivation of calculations with rational numbers. Specifications of the Rat sort determine this sort as a field, linear order and static extension of Int.
Sort Rat:: Field, LinOrd; //Inherited Constructor Rat r ={(Int a)//(Nat b); // Sort constructor a//1 = a; // The embedding function RatToInt Num(r) = a, Den(r) = b; // Access functions GCD(a, b) = 1 // Contextual condition Form: Num(Form(r)) Int, Den(Form(r)) Nat,
GCD(Num(Form(r), Den(Form(r)) = 1;
a*1 = 1*a = a to (13), we obtain: a + c//d = Form((a*d + c)//d) (12) (13) (14)
Similarly, for the second operand: a//b + c = Form((a + b*c)//b);
The resulting relations are particular cases of (12) - a specification of the Add operation with the RatToInt embedding. Together with the general relation (11) they define implementation rules for addition of fractions: Add:=rs{ a//b + c//d = Form((a*d + b*c),(b*d)), a + c//d = (a*d + c)//d, a//b + c = (a + b*c)//b };
Similarly interpreters of operations of subtraction and multiplication on Rat can be derived. An exception is the division operation, which is absent in the signature of Int sort. Therefore, it is necessary to define and specify it as multi-sorted (see specification of the Rat sort). Another exception is the exponentiation operation, which is expressed using multiplication.
Now let us focus on the Form function. Definition of this function connects it with the symbol of sort constructor. The role of this function is essentially in the canonization of sort element. During execution of a rule of the general form this function is called on the result of the operation. Therefore, Form is an interpreter of the constructor sort symbol. For the symbol // of Rat sort constructor we will use the notation !/. The general rule of addition will take the form
a//b + c//d = a*d + b*c)!/(b*d).
We will always include the sign “!” in the infix notation of sorts constructors and it will always mean the call of the constructor of sort interpreter.
Add:=rs{ a//b + c//d = (a*d + b*c)!/(b*d), a + c//d = (a*d + c)//d, a//b + c = (a + b*c)//b };
Interpreter of sort constructor is called only in the first rule.
The method of derivation of an interpreter of an operation of sort v from its specification in the case when the algebra Av is defined as a static extension of algebra Au can be generalized as an algorithm of synthesis of an algebraic program.
Note that this method can be implemented in the form of an algebraic program because it relies only on equational derivation. For automation of elimination of the Form functions more sophisticated methods and technologies have to be used, e.g. a theorem prover over the basic sort u.
In this example, we show that the methods of derivation of specifications discussed above leads to mathematically sound systems of interpretation rules.
First of all, note that there are two fundamentally different methods of definition operations. Operations Add, Sub, Mult, Div are defined in terms of constructors of operands. Such a definition of operation will be called constructive. It demonstrated by the definition of the operation IntDiv (division with remainder). Mod operation is defined in terms of operations of signatures Polynom sort. We will call such definitions of operations abstract or derived. Since this signature is inherited from the abstract sort EuclideDomain, the specification of Mod is given in this sort. In EuclideDomain sort Euclidean algorithm is defined. Pow operation should be defined earlier – in specification of the sort MiltSemiGroup.
A constructor of a sort is defined recursively. So the Polynom algebra is a sequence of nested algebras which begins with the algebra Monom (Monoms of one variable): Mon Pol0 Pol1 ... Polk ... (16)
The algebra Poli is a set of polynomials of i-th degree. Then Poli is a vector space of dimension i + 1. In this interpretation polynomial degree determines the index in the sequence. Therefore, the operation of addition Add (15) is determined by three equalities, the first of which defines the rule of addition, if both operands belong to one algebra, the other two – when they belong to different algebras:
a,b Poli ;a Poli ,b Pol j ,i j; a Poli ,b Pol j ,i j
Thus, the extension (16) is an extension of vector spaces. The rules of interpretation of vector operations are derived from their specifications quite similar to the case of static extensions:
dim(Poli ) i 1, dim(Poli1) i 2, Poli Poli1 ,
V Poli1 V a A, A Poli ;0 A A, a 0 a .
Deg(a)==Deg(b)→(a++A)+(b++B)=(a+b)!+(A+B), //basic rule Deg(A)< Deg(b) → A + (b++B)= b !+ (A+B), //partial cases Deg(a)> Deg(B) → (a++A) + B = a !+ (A+B)
The derived rules still do not consider the second of the conditions M++0=M. Therefore, each of these rules should still be converted: Deg(a)== Deg(b)→ a + (b++B)=(a+b)!+ B.
Deg(a)== Deg(b)→(a++A) + b=(a+b)!+ A.
So, for the Add operation of sort Polynom we obtain the following system of rules: Deg(a)== Deg(b)→ (a++A) + (b++B) = (a+b)!+ (A+B), Deg(a)== Deg(b)→ a + (b++B)=(a+b) !+ B, Deg(a)== Deg(b)→ (a++A) + b = (a+b) !+ A, Deg(A)< Deg(b) → A + (b++B) = b !+ (A+B), Deg(A)< Deg(b) → A + b = b ++ A, Deg(a)> Deg(B) → (a++A) + B = a !+ (A+B), Deg(a)> Deg(B) → a + B = a ++ B;
Conclusion. Specifications of the sort Polynom determine a dynamic extension of the vector space. Derived operations should be excluded from the specifications of Polynom and included in specifications of the relevant abstracted algebras. Constructive operations of the signature of vector space are defined by the main case. The special cases are derived by the methods of derivation of static extensions.
Because there are two embedding relations for the sort Polynom, the derivation of a complete rules system is done sequentially: firstly by the first relation and then by the second one. Multiplication and an incomplete division are specified separately as additional operations on the vector space Polynom.
Consider an example of a binary dynamic extension of the Bool algebra – the algebra of logic BoolAlg [14]. This algebra is an extension of the Variable base sort, because the elements of sort are Latin letters interpreted as logical formulas. We will show that derivation of interpreters of logical operations is performed by the same methods.
The elements of the set BoolAlg are formulas of the propositional logic of many variables. Let F(x1, x2,…, xn) be an arbitrary formula of propositional logic of n variables. Denote as O and I the truth and falsity values respectively. Then
F(x1, x2 ,...,xn ) xn & F(x1x2 ,...,xn1, I ) xn & F(x1, x2 ,...,xn1,O) .
If we denote we obtain the representation
A(x1,...,xn1) F(x1,...,xn1, I ), B(x1,...,xn1) F(x1,...,xn1,O) ,
F(x1, x2 ,...,xn ) x1 & A(x1,...,xn1) x1 & B(x1,...,xn1) (17)
Now perform sequentially the same transformations of formulas A, B w.r.t. the variables xn-1, …, xn. As a result we obtain a recursive representation of the propositional logic formulas. Indeed, through BoolAlgm denote the set of propositional logic formulas in variables x1, …, xm. Then
BoolAlgn {F : F xn & A xn & B, A, B BoolAlgn1} Thus, sort BoolAlg is the union of an increasing sequence of algebras BoolAlgm: BoolAlg0 = Bool, BoolAlg0 BoolAlg1 … BoolAlgm… (18) BoolAlg = BoolAlgm
df
BF(A, B, x) x & A x & B
Note that formula (17) defines a canonical form of a formula of the algebra of propositions. Denote
Then
BF(A1, B1, x) & BF(A2, B2, x) BF(A1 & A2, B1 & B2, x) , BF(A1, B1, x) BF(A2 , B2 , x) BF(A1 A2 , B1 B2 , x)
BF(A, B, x) BF(A,B, x) .
Thus, the basic logic operations are performed per the argument! Finally, it is easy to check that the embedding function is defined by the equality
BF(A, A, x) A)
In this paper we have shown that the concept of a constructive extension of MAS is the key one in design and implementation of symbolic computations. Most of all, this applies to symbolic computations in mathematical systems for educational purposes, where classical algebras and algebraic systems are used.
Actually, the constructive approach, along with the axiomatic approach in algebra is well known [12-13]. The idea of a constructive definition of an algebra element through the elements of basic algebras is systematically used in algebraic research. On the other hand, the overloading mechanism for algebraic operations is a standard tool in programming of mathematical systems.
Thus, the main theoretical result is the idea of systematic usage of the construct of extension in programming of MAS signatures as overloaded signatures. Other methodical components of proposed approach are given in [14-17].
The practice of usage of this approach in development of mathematical systems for education has shown its effectiveness and even universality. This is the main practical result. (19) (20) (21) (22) (23) 3. Lvov, M.: Therm VII - school computer algebra system. Computer in school and family.7, 27-30 (2004). 4. Letichevsky, A., Kapitonova, J., Volkov, V., Chugajenko, A., Chomenko, V.: Algebraic programming system APS (user manual). Glushkov Institute of Cybernetics, National Academy of Sciences of Ukraine, Kiev (1998). 5. Kapitonova, J., Letichevsky, A., Volkov, V.: Deductive means of the system of algebraic programming. Cybernetics and system analysis. 1, 17–35 (2000). 6. Kapitonova, J., Letichevsky, A., Lvov, M., Volkov, V.: Tools for solving problems in the scope of algebraic programming. Lectures Notes in Computer Sciences. 958, 31-46 (1995). 7. Lvov, M.: Basic principles of constructing pedagogical software to support practical classes. Control systems and machines. 6, 70-75 (2006). 8. Peschanenko, V.: Extending standard modules algebraic programming system APS for use in systems for educational purposes. Scientific journal of the National Pedagogical University named after M.P. Drahomanov. 3 (10), 206-215 (2005). 9. Peschanenko, V.: About one approach to the design of algebraic data types. Problems of programming (Problemy prohramuvannia). 2-3, 626-634 (2006). 10. Peschanenko ,V.: Use of the algebraic programming system APS to build systems for supporting the study of algebra in school. Upravlyayuschie sistemy i mashiny (Control systems and machines). 4, 86-94 (2006). 11. Van der Varden, B: Algebra. Nauka, Moscow (1979). 12. Goguen, J., Meseguer, J.: Ordered-Sorted Algebra I: Partial and Overloaded Operations.
Errors and Inheritance. Technical Report, SRI International, Computer Science Lab (June 1983). 13. Goguen J.A., Meseguer J. (1987) Models and equality for logical programming. In: Ehrig H., Kowalski R., Levi G., Montanari U. (eds) TAPSOFT '87. TAPSOFT 1987. Lecture Notes in Computer Science, vol 250. Springer, Berlin, Heidelberg 14. Lvov, M.: About one approach to the implementation of algebraic calculations: calculations in the algebra of statements. Bulletin of Kharkiv National University (Series “Mathematical Modeling. Information Technology. Automated Control Systems”). 863, 157-168 (2009). 15. Lvov, M.: About one approach to verification of algebraic calculations. Problems of programming. 4, 23-35 (2011). 16. Lvov, M.: Inheritance method for the implementation of algebraic calculations in mathematical systems of educational purpose. Systems of control, navigation and communication. 3(11), 120-130 (2009). 17. Lvov, M.: The method of morphisms of the implementation of algebraic calculations in mathematical systems of educational purpose. Information processing systems. 6(80), 183-190 (2009).