Terms over many sorted universal algebra.pdfVIP

JOURNAL OF FORMALIZED MATHEMATICSVolume 6, Released 1994, Published 1998Institute of Mathematics, University of Bia lystok Terms Over Many Sorted Universal Algebra1Grzegorz BancerekInstitute of MathematicsPolish Academy of SciencesSummary. Pure terms (without constants) over a signature of many sorteduniversal algebra and terms with constants from algebra are introduced. Facts onevaluation of a term in some valuation are proved.MML Identi er: MSATERM.WWW: /JFM/Vol6/msaterm.htmlThe articles [19], [24], [1], [13], [20], [25], [11], [9], [12], [15], [2], [5], [17], [3], [23], [4], [14],[6], [7], [8], [21], [22], [10], [16], and [18] provide the notation and terminology for this paper.1. Terms over a Signature and over an AlgebraLet I be a non empty set, let X be a non-empty many sorted set indexed by I , and let i bean element of I . Note that X(i) is non empty.In the sequel S denotes a non void non empty many sorted signature and V denotes anon-empty many sorted set indexed by the carrier of S.Let us consider S, V . The functor S -Terms(V ) yielding a subset of FinTrees(the carrierof DTConMSA(V )) is de ned by:(Def. 1) S -Terms(V ) = TS(DTConMSA(V )):Let us consider S, V . Note that S -Terms(V ) is non empty.Let us consider S, V . A term of S over V is an element of S -Terms(V ).In the sequel A is an algebra over S and t is a term of S over V .Let us consider S, V and let o be an operation symbol of S. Then Sym(o; V ) is anonterminal of DTConMSA(V ).Let us consider S, V and let s1 be a nonterminal of DTConMSA(V ). A nite sequenceof elements of S -Terms(V ) is said to be an argument sequence of s1 if:(Def. 2) It is a subtree sequence joinable by s1.We now state the proposition(1) Let o be an operation symbol of S and a be a nite sequence. Then ho; the carrierof Si-tree(a) 2 S -Terms(V ) and a is decorated tree yielding if and only if a is anargument sequence of Sym(o; V ).The scheme TermInd deals with a non void non empty many sorted signature A; a non-empty many sor