Computations in Extensions of Multisorted Algebras Michael Lvov [0000-0002-0876-9928] Kherson State University, 27, Universytets’ka St., 73000 Kherson, Ukraine Lvov@ksu.ks.ua Abstract. 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 mathemat- ical 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 specifi- cations, based on constructive improvement of notion of extension of multi- sorted algebraic system. This approach is illustrated by examples of realization of interpreters of operations in the field of rational numbers, ringing of one var- iable 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. Keywords. systems of computer mathematics, symbolic computations, multi- sorted algebras, extensions of algebras, interpreters of algebraic operations. Introduction 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 mathe- matical systems [1, 2, 3] showed that implementation of algebraic computations re- quires careful preliminary design of MAS via development of MAS sort hierarchies and specifications of interpreters of multi-sorted algebraic operations [8]. Due to a number of reasons [9], for implementing calculations based on symbolic trans- formations we use the system of algebraic programming APS [4, 5, 6] which was adapted for our purposes by V. Peschanenko [10]. APS uses an algebraic programming technology based on rewriting systems and rewriting strategies. Thus, an interpreter of an algebraic operation is defined by a sys- tem of rewriting rules. 1 Problem formulation 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 para- graph 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 ex- tensions (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 embed- ding 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), quad- ratic radicals field (binary dynamic extensions), univariate polynomial rings (linear dynamic extensions) and the algebra of propositions (binary dynamic extensions). 1.1 Multi-sorted algebras as mathematical model of algebraic computations 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 alge- braic 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 val- ues 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 argu- ments 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 multi- sorted 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 Mult : Real × VectorSpace → VectorSpace Below we will use more common, traditional mathematical notations for opera- tions. Since the infix notation is usually used for scalar multiplication, we have: Real * VectorSpace → VectorSpace Definition 1.4. Let Bool be a sort with the value range S Bool  {True, False} . A multi-sorted predicate P is a mapping P : Su1 ... Sum  S Bool , 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=, 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 con- sidered 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= 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=. Thus, a multi-sorted algebra A can be represented by a set of restrictions (algebras) Av, v ∈ U, that A  Au ,...,Au  . 1 k Example 1 Consider a software system that implements simplification of algebraic and trigo- nometric 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: MultiPolynom – the ring of multivariate polynomials. MultiPolynom + MultiPolynom → MultiPolynom MultiPolynom * MultiPolynom → MultiPolynom … MultiTrig – the ring of multivariate trigonometric polynomials. Sin(LinComb) → MultiTrig Cos(LinComb) → MultiTrig MultiTrig + MultiTrig → MultiTrig … LinComb – the vector space of linear combinations of several variables (arguments of trigonometric polynomials). Pi LinComb + LinComb → LinComb Rat * LinComb → LinComb … Rat – the field of rational numbers (coefficients of polynomials and trigonometric polynomials). Rat + Rat → Rat Rat - Rat → Rat Rat = Rat → Bool Rat < Rat → Bool … The relation of dependence between sorts generates a structure of dependence on the set of algebras Au, u ∈ U: an algebra Av depends on the algebra Au if the sort v depends on the sort u. If the relation of dependence has no cycles, then a multi-sorted algebra can be constructed step by step (incrementally) by constructing an algebra Av, if algebras Au on which it depends are already constructed. 1.2 Axioms and constructs of multi-sorted algebra For constructing algebras Au we use their axiomatic and constructive descriptions (definitions). Fig. 1. Diagram of dependency of algebras of Example 1. Definition 1.7. An axiom of an algebra Au is an identity or a conditional identity in a signature Σu. An axiomatic description in an algebra Au is a finite set of axioms (axiom system) of the algebra Au. We will use algebraic terminology and the relevant systems of axioms from the book [11]. A constructive description of an algebra Au is a definition of a constructor of the sort Su (i.e. a definition of terms of sort Su) and a set of interpreters of opera- tions of Σu. Definition 1.8. A signature of constructors Tu is a finite set of symbols of opera- tions together with a map that with each symbol   Tu associates a symbols of the sort u together with a list of symbols of sorts of its arguments (if  an operation symbol, the expression u   (u1 ,...,um ) means that this symbol is associated with the symbol of the sort u and the symbols of the sorts of its arguments u1,…,um.) A constructor of sort Su of an algebra Au is a system of equations which defines syntactically the elements of sort Su as terms in Tu signature. So, the sort Su is the set of terms in (its own) signature Tu of constructors of Su sort. Definition 1.8 is the key one in our approach to specification of algebraic computa- tions. Let us present the relevant examples and explanations. Example 2. The field Rat of rational numbers. Rational numbers are represented in the form of simple fractions. The constructor of a sort defines the standard representation of elements of this sort. The most com- mon is the canonical form. That is why, p SRat  { : p  SInt , q  SNat , GCD( p, q)  1} q (1) 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: SRat  { p // q : p  SInt , q  SNat , GCD( p, q)  1} (2) 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 as- pects 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. S Polynom  {Q : Q  M  P, M  S Monom, P  S Polynom, df (3) degQ  deg M ; deg(M )  deg(P)} S Monom 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 im- plement algorithms for performing each of its operations in such a way that the axi- oms 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 pur- poses we use APLAN language. So we include this language in the specification lan- guage. 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= . 1.3 The methods of construction of multi-sorted algebras Construction of the structure of multi-sorted algebras means specification, prototyp- ing 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 depend- ence, 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. 1.3.1 The method of algebra extension 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 f 2 : (v1 ,...,vm )  v respectively, if Su1  Sv1 ,...,Sum  Svm , then (a1 ,...,am )  Su1  ... Sum the equality f1 (a1,...,am )  f 2 (a1,...,am ) holds. An embedding is an isomorphic map Re d : 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 : Re d 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 indi- cates 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 sorted- ordered. 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 Re d : Rat  Int , defined by the equality Re d (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 recur- sive construct Polynom, the arguments of which is the sort Monom. Let us comple- ment the specification of the sort Polynom with an embedding Re d : Polynom Monom, defined by the equality Re d (M  0)  M . So the sort Polynom is defined as an extension of the sort Monom. Fig. 2. Diagram of extensions in example 4. In turn, the sort Monom is an extension of the sort Degree with a function Red de- fined 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 Lin- Monom 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 multisort- ed algebras. In particular, it allows defining the overloaded algebraic operations and algebraic type casting functions. 2 Methods of synthesis of algebraic programs 2.1 Static and dynamic extensions 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, con- tains both the base and recurrent part. Examples of dynamic extensions: 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 . LinComb w  (LinMonomu)  (LinComb w) An univariate polynomial ring Polynom over the field Coef. This ring is traditional- ly 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 num- bers. We introduce the following notations: Rad0  Q, Radn  {r : r  a  b * pn , a, b  Radn1 , n  1,2,...}. The field Rad is the union of the increasing sequence Radn of fields.  Rad   Radn , Rat  Rad0  Rad1  ...  Radn  ... (4) n0 Thus, the constructor Rad has the form Rad r  ( Rad a)  ( Rad b) * Nat p | ( Rat q) (5) Note that sequence of extensions (4) is a sequence of finite algebraic extensions of fields with roots of polynomials x 2  pn  0 . Representation (5) includes a description of basic elements Rat q and a description of the extension mechanism - the constructor ( Rad a)  ( Rad b) * Nat p . This specifica- tion 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 specifica- tion of the LinComb vector space with the inclusion of the item describing of the ele- ments 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 al- gebra 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, (6) B( n1)   ( A1 ,...,B( n) ,..., An ) (7) The embedding Re d : A  B defines the embedding Re di : Bi1  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.  B   Bn , B0  B1  ...  Bn  ... (8) n0 In MAS development practice there were some generalizations of the definition (8). Namely, instead of the sequence of algebras {Bi }i0 let consider the set of indexed algebras {Ai }iI , 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   A j . Let us assume there is an em- jJ bedding of algebras Bj, where BJ1  BJ 2  BJ1  J 2 . Then B B J J  I , J  (9) An example of such algebra is a ring K[[x]] , the elements of which are sums of monomial with rational degrees: K[[x]]  {P : P  a x j jJ , J  Rat, J  j (10) 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 Synthesis of algebraic programs 2.2.1. Example of an algebraic program output with sort specifications 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; }; Operations Add: a//b + c//d = Form((a*d + b*c)//(b*d)); Sub: a//b - c//d = Form((a*d - b*c)//(b*d)); Mult: a//b * c//d = Form((a*c)//(b*d)); Div: a//b / c//d = Form((a*d)//(b*c)); Div: a/b = Form(a//b),a/0 = Exeption(‘Divison by zero’); Pow: n >= 0 -> (a//b)^n = (a^n//b^n), n < 0 -> (a//b)^n = (b^-n//a^-n); Predicates Equ: a//b == c//d = (a == c)&(b == d); Gre: a//b > c//d = (a*d > b*c); Les: a//b < c//d = (a*d < b*c); UnLes: a//b >= c//d = (a//b > c//d)  ( a//b == c//d); UnGre: a//b <= c//d = (a//b < c//d)  ( a//b == c//d); Consider the output of the Add operation interpreter. From specifications we have: a//b + c//d = Form((a*d + b*c)//(b*d)); (11) a//1 = a; (12) we get: a + c//d = Form((a*d + 1*c)//(1*d)); (13) Applying the sort equality Int a*1 = 1*a = a to (13), we obtain: a + c//d = Form((a*d + c)//d) (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 op- eration 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 specifica- tion of the Rat sort). Another exception is the exponentiation operation, which is ex- pressed 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 canoniza- tion 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 construc- tor 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 speci- fication 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 be- cause 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. 2.2.2 Interpreters output in linear dynamic extensions Example 8. Specifications of Polynom sort and calculations with univariate polyno- mials. Specifications of the Polynom sort define this sort as a Euclidean domain and a lin- ear dynamic extension of Monom. Sort Polynom::EuclideDomain; Parameter Field Coef, Const Variable Argument; Constructor{ Polynom P = Monom M ++ Polynom Q // Constructor of sort 0 ++ P = P, //Embedding function PolynomToPolynom M ++ 0 = M; //Embedding function PolynomToMonom LeadMon(P) = M, // Access functions LeadCoef(P)= Cf(M), Arg(P)= Arg(M), Deg(P)= Deg(M); Deg(M)> Deg(Q), Arg(M)= Arg(Q); //Contextual condition Form: MMonom, Q  Polynom, 0 ++ P = P, M ++ 0 = M, Arg(M) = Arg(Q), Deg(M)> Deg(Q), Cf(M)<>0 }; Operations Add: Deg(a)==Deg(b)→ (a++A)+(b++B)=(a+b) !+ (A+B); (15) Sub: Deg(a)==Deg(b)→ (a++A)-(b++B)=(a-b) !+ (A-B); Mult: // Polynom * Polynom → Polynom; Commutative (a++A)*(b++B)=(a*b)++((a*B+A*b)+A*B); Mult: // Coef * Polynom → Polynom; Commutative c*(b++B)= c*b ++ c*B; (b++B)*c = Form(c*b, c*B); Div: (a++A)/b = a/b ++ A/b; Pow: a^n=sqr(a^n div 2)*a^(n mod 2); // From sort MiltSemiGroup IntDiv: Deg(P)==Deg(Q) → P div Q = LeadCoef(P)/LeadCoef(Q), Deg(P)< Deg(Q) → P div Q = 0, Deg(P)> Deg(Q) → P div Q = LeadMon(P)div LeadMon(Q)++ P-(LeadMon(P)div LeadMon(Q))*Q div Q); Mod: P mod Q = P - (P div Q)*Q; // From EuclideDomain 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 defini- tions 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 Euclid- eDomain sort Euclidean algorithm is defined. Pow operation should be defined earli- er – 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 interpreta- tion of vector operations are derived from their specifications quite similar to the case of static extensions: dim(Poli )  i  1, dim(Poli1 )  i  2, Poli  Poli1 , V  Poli 1  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; Also on the sort Monom we define an additional partial operation Add: a$x + b$x = (a + b)$x. This system takes into account both conditions, i.e. of a sequence of extensions Monom  Pol0  Pol1 , Poli  Poli1 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. Construc- tive 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. 2.2.3 Example of algebraic program output within sort specifications. Dynamic binary extension 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 varia- bles. Denote as O and I the truth and falsity values respectively. Then F ( x1 , x2 ,...,xn )  xn & F ( x1 x2 ,...,xn1 , I )  xn & F ( x1 , x2 ,...,xn1 , O) . If we denote A( x1 ,...,xn1 )  F ( x1 ,...,xn1 , I ), B( x1 ,...,xn1 )  F ( x1 ,...,xn1 , O) , we obtain the representation F ( x1 , x2 ,...,xn )  x1 & A( x1 ,...,xn1 )  x1 & B( x1 ,...,xn1 ) (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 proposi- tional logic formulas. Indeed, through BoolAlgm denote the set of propositional logic formulas in variables x1, …, xm. Then BoolAlg n  {F : F  xn & A  xn & B, A, B  BoolAlg n1} Thus, sort BoolAlg is the union of an increasing sequence of algebras BoolAlgm: BoolAlg0 = Bool, BoolAlg0 BoolAlg1 … BoolAlgm… (18) BoolAlg = BoolAlgm Note that formula (17) defines a canonical form of a formula of the algebra of propositions. Denote df BF( A, B, x)  x & A  x & B (19) Then BF( A1 , B1 , x) & BF( A2 , B2 , x)  BF( A1 & A2 , B1 & B2 , x) , (20) BF( A1 , B1 , x)  BF( A2 , B2 , x)  BF( A1  A2 , B1  B2 , x) (21) BF( A, B, x)  BF(A, B, x) . (22) 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 ) (23) Conclusion 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 me- thodical 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. References 1. Lvov, M., Kuprienko, A., Volkov, V.: Applied Computer Support of Mathematical Train- ing. Proceedings of Internal Workshop in Computer Algebra Applications. 25-26. Kiev. (1993). 2. Lvov, M.: AIST: Applied Computer Algebra System. Proceedings of ICCTE’93. 25-26. Kiev. (1993). 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 clas- ses. 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 Univer- sity 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 sup- porting the study of algebra in school. Upravlyayuschie sistemy i mashiny (Control sys- tems 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: calcula- tions in the algebra of statements. Bulletin of Kharkiv National University (Series “Math- ematical Modeling. Information Technology. Automated Control Systems”). 863, 157-168 (2009). 15. Lvov, M.: About one approach to verification of algebraic calculations. Problems of pro- gramming. 4, 23-35 (2011). 16. Lvov, M.: Inheritance method for the implementation of algebraic calculations in mathe- matical 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).