TermWare: Semantics Description
DocumentId:GradSof-TermWare-e-Sm-7.10.2002-5


August 18, 2008

Contents

1 Introduction
2 Formal Model
 2.1 Alphabet
 2.2 Terms
 2.3 Operations
 2.4 Ordered rulesets
 2.5 Actions
 2.6 Terminal System With Interactions
3 TermWare Language
 3.1 Hierarchical Name System
 3.2 Embedded Parsers Of Other Languages
4 Java API
 4.1 Terms Operating
  4.1.1 Term
  4.1.2 TermFactory
  4.1.3 ITermTransformer
  4.1.4 ITermRewritingStrategy
  4.1.5 IFacts
  4.1.6 IEnv
  4.1.7 TermSystem
 4.2 Subsidiary Classes
  4.2.1 TermwareInstance
  4.2.2 IParser, IParserFactory
  4.2.3 IPrinter, IPrinterFactory
5 Changes

1 Introduction

Termware is computer algebra system designed for embedding into language processing systems. The formal model, that underlies language semantics, is defined in the article. Also TermWare syntax and internal Java API structure are briefly described here. The article was meant to acquaint a reader both with object-oriented and functional programming and with mathematical logic fundamentals. But if you are — a programmer, who wants to use TermWare in your own projects you can skip the reading of the article except of the first paragraph.

2 Formal Model

The usual terminal algebra is built here, where the language objects are terms (expressions of fi(x1xn) form, variable and elementary data types, the same as those of all functional programming languages). And its only difference from standard approach is that the ordered set constructor is the dedicated term and substitution operations retain order on those terms.

The rest of the part will be devoted to wearing construction:

2.1 Alphabet

  1. Primitive types set (note , it isn’t many-sorted algebra )

    Σpt = {CHAR,SHORT,INT,BigDecimal,BigInteger,BOOL,STRING,ATOM}

  2. Typed constants set Σcpt = {cipt},

    each constant is linked with the value on corresponding primitive type set, i.e. val : Σcpt- > Dompt, where

  3. Terminal symbols set Σt = {ti}
  4. Substitute symbols set Σx = {xi}
  5. Parenthesis ’(’ and ’)’ and comma ’,’
  6. Functional symbols set Σf = {fi}

2.2 Terms

Let’s define concrete terms set Tc :

And substitute terms set Tv

Term, which belongs to Tv∕Tc we will call term with free variables. For each term T the set of substitute symbols, that form the term, will call the set of free variables of the term and will mark as v(T).

2.3 Operations

Let’s define next model functions of our term system:

Rewriting rule is the three: (X,tin,tout) where:

Rewriting operation semantics is defined by following expression:

apply(t,tin,tout) = subst(tout,free_unify(tin,t))

Let’s extend rewriting operations for rules set:

apply(t,{r1...rn}) = {apply(t,r1)...apply(t,rn)}

and for free terms set 1 :

apply({t1...tn},R) = ∪apply(ti,R )

Evidently, the rule can be represented as term: rule(vars,tin,tout) where:

We will say that term set x can be rewritten into term set y, if there exists a chain z1zn such as

z1 = x∧ zn = y ∧ ∀i ∈ {1...n}zn+1 ∈ apply(zn,R)

At last , will say that term set T converges relatively to set of rules R if there exists fixed point of equation:

The set of rules R is called converging relatively to finite set of terms T, if apply*(T,R) is finite.

Rule set has the noetherian property, if

                                      *                      *                    *           *
∀t ∈ T;r1,r2 ∈ Rapply(t,r1)! = apply(t,r2)∃R ∈ R : apply(apply(t,r1),R ) = apply(apply(t,r2),R )∧apply(t1,R )isfinite

Thus we come to wide-known rewriting rules theory , with some differences from canonical statements:

Those differences don’t add anything essentially new to mathematical properties of algebra except that it’s more convenient to work with it, from technical point of view .

2.4 Ordered rulesets

We would extend semantics of ruleset evaluation on non-confluent rule systems, by applying order of rule evaluations in critical pairs. I. e. rules p, s forms critical pair, if exis such term t, than: apply(p,t)apply(s,t). Newman’s lemna say, that if system is locally-confluent (i.e. for each criticat pair exists common reduct for apply(p,t) and apply(s,t) than system is confluent. But many practically interested systens better described in terms of locally-incoherent rules with fixed order of evaluation.

So, let’s introduce partial ordering of rewriting rules by ’concretization’ of input patterns. I.e. we will say that t1ct2 when t1 is ’more concrete’ than t2. And what is more concrete ? - this means that t1 can be represented as partial case of t2, i.e. exists substitution of free variables s: subst(t2,s) t1. Equivalent definition: t : free_unify(t,t1) free_unify(t,t2).

Now, let p = (inp outp) and s = (ins outs) are two rules, which form critical pair. we see that p cs if inpcins, and let’s fix the order as evaluation as: more concrete term evaluated first, i. e.

              (
              {  apply(p,t)             p ≤c s
apply({p,s},t) =   apply(s,t)             s ≤c p
              (  ι{apply(p,t),apply(s,t)}  p ~c s
where ι is operator of non-determenistics choice, defined by strategy.

It’s easy to show, that for each ruleset r1rn where i,j : ij ⇒⁄ ri ~crj can be build equivalent locally-confluent ruleset.

2.5 Actions

Next question, that should be considered is the term calculation representing. Usual approach (set of rules, that convert input term set to output) doesn’t suit us, becouse in real world we need something more:

Among the samples of such applications there are set of rules for determination of the following actions in a business process, where set depends on process variables, or the code generation process, that depends on certain architecture, or the output rules, presented by facts of the deductive database.

Consequently, we need to define operations semantics by including openly environment interaction and rules set modification dependent on state.

Terminal mechanism is the four: < S,E,ϕse > where:

The terminal mechanism behavior is defined by the following transformation in discrete time unit:

< S,E, X > - >< ϕ (X,E, S)|,ϕ (ϕ (X,E, S)|)
                 s        S  e  s        Y

(here x|Y denotes projection x onto coordinate Y in general sense of set theory).

The following diagram can be more clear.

          phi_s  
 <S,E,X> ----------> <S’,Y’>   phi_e  
    |                       ----------> E’  
    ---------------------E

2.6 Terminal System With Interactions

What changes we should make in the term rewriting system to reflect operation semantics requirements - we should just add some syntax of environment interaction:

Input/output pair (X : x y) is replaced by the four (X : (x,ein) (y,eout), where

We will denote the four as x[ein]- > y[eout]. Expression x[ein] for term t can be interpreted as comparison with sample x while executing subst(ein,snd(free_unify(t,x))) (let snd(free_unify(t,x)) = s), y[eout] - as substitution of unification into y and subst(eout,s) execution.

3 TermWare Language

Lexical Units:

Syntax:

See also BNF definitions

Full description of build-in systems see in TermWareAPI reference

Samples of systems, defined by TermWare Language:

 
System(BooleanAlgebra,default,  
ruleset(  
 $x & ($x => z) -> $z ,  
 not($x & $y) -> not($x) | not($y) ,  
 not($x | $y) -> not($x) & not($y) ,  
 $x & ($y | $z) -> ($x & $y) | ($x & $z) ,  
 not(not($x)) -> $x ,  
),  
FirstTop);  
 
System(BooleanLogic,general,  
 ruleset( import(BooleanAlgebra),  
          true => $x -> $x,  
          false => $x -> not($x),  
          true | $x -> true,  
          false | $x -> $x,  
          true & $x -> $x,  
          false & $x -> false,  
          not(true) -> false,  
          not(false) -> true  
        ), FirstTop);  
 

Here, as you can see all rules are shortened (without operations and data base).

The full system model with operations and fact base demands facts semantics and operations description (or rather their programming in Java) and will be of enormous volume for this article.

Therefore below we’ll cite terminal system "of real life" 2, and facts semantics and operations we’ll describe informally :

System(BugFixing,DevelopmentProcess,  
 ruleset(  
 
 received($bug_id) -> check_confirmation($bug_id)  
                                 // human_task(check_bug($bug_id)),  
 
 check_confirmation($bug_id) [|confirmed($tester,$bug_id)|]  
                          -> known($bug_id)  
                                 // human_task(fix_bug($bug_id),  
                                               write_regression($bug_id)  
                                              ),  
 
 check_confirmation($bug_id) [|not_confirmed($tester,$bug_id)|]  
                          -> true // send_not_confirmed($bug_id,$tester),  
 
 
 known($bug_id) [|  
                  fixed($developer1, $bug_id) &&  
                  added_regression($developer2,$bug_id)  
                 |]  
                          -> true // send_closed($bug_id,$developer1)  
 ),  
 FirstTop)

This example describes TermWare application in business-processes organization system. As you’ve guessed the example is software error message processing.

Here fact base (environment) can answer the questions:

And can interpret messages:

Notice, that environment data are transmitted to the system by sentential expressions in conditions. More detailed this primer is described in [1].

3.1 Hierarchical Name System

From terminal systems programming point of view it is convenient to use Hierarchical Name Mechanism resembling to idl modules, C++ namespaces or Java packages.

In TermWare such mechanism is represented by domain term. Syntax: domain(name,def1,defn), where defi is systems or subdomains definition terms.

Example:

domain(algebra,  
  System(Semigroup),  
  domain(LiGroups,  
    System ..  
  )  
)

Also automatic system definitions loading from files is implemented: while interpreting embedded conversions in any context, if full system name (for instance:x.y.z, i.e. system with z name, which is located in x/y domain) is found, then the file is automatically loaded from according location of file system relative to termware.path - Java environment property (in case of addressing to x.y.z system an attempt to read <termware.path>/x/y/z.def file will be performed).

3.2 Embedded Parsers Of Other Languages

TermWare syntax, as it is, is not always convenient for data input: sometimes we’d like to use more natural problem-oriented language for the purpose.

Toward this aim TermWare provides extension possibility: users can embed syntax parsers of their own languages by implementing verb|IParser| and IParserFactory interfaces in their Java classes and by registering the classes names in general dictionary.

4 Java API

4.1 Terms Operating

4.1.1 Term

Main TermWare entity is Term interface.

(API Description)

As you can see, ITerm is interface where the following elements are defined:

Unlike many computer algebra systems, term system is not build bottom-up, from atomic data types, but top-down, i.e. any class, that extends abstract class Term, can be declared as term.

Of course, there exists predetermined term types set (described in Formal Model). According inheritance diagram looks as follows:

 Term  
  |  
  *---AbstractPrimitiveTerm  
  |     |  
  |     *--AtomTerm  
  |     |  
  |     *--BooleanTerm  
  |     |  
  |     *--DoubleTerm  
  |     |  
  |     *--IntTerm  
  |     |  
  |     *--NILTerm  
  |     |  
  |     *--StringTerm  
  |  
  *---AbstractComplexTerm  
  |   |  
  |   *--SetTerm  
  |  
  *---XTerm  

But from programmer’s point of view it’s not necessary to use these classes: it would be better for this purpose to use TermFactory interface.

4.1.2 TermFactory

TermFactory is a class, accessible from TermWare singleton, that provides methods to create terms. (API Description)

Usage examples:

 Term term=TermWare.getInstance().getTermFactory().createAtom("qqq");

уПЪДБУФ

 TermFactory termFactory=TermWare.getInstance().getTermFactory();  
 Term term=termFactory.createComplexTerm3("f_3",  
                                  termFactory.createInt(3),  
                                  termFactory.createComplexTerm2("f",  
                                            termFactory.createAtom("a1"),  
                                            termFactory.createAtom("a2")  
                                                                 ),  
                                  termFactory.createX(1)  
                                                     );

will create term f3(3,f(a1,a2),x1) with one free variable x1.

4.1.3 ITermTransformer

It is just term converter: (API Description)

Main converter functioning is concealed in transform method, which transform input term to output in some system and with transformation context (which give us access to current substitution and so on).

Let’s consider how term converters are bound with rewriting rules: we can create according converter just by rewriting rule.

4.1.4 ITermRewritingStrategy

And at last rewriting strategy: (API Description) It’s rather difficult object, which includes rules (term converters) set and the rules application algorithm.

End user usually doesn’t work directly with rewriting strategys, but application programmers can create their own rewriting strategy by inheriting their class from AbstractTermRewritingStrategy. (API Description)

This minding of strategy come from APS [3], another approach can be found in Stratego [2].

4.1.5 IFacts

IFacts (API Description) is terminal system knowledgebase pattern, that figures environment (or oracle) of our logic.

What we can do with fact:

Naturally, knowledge base semantics is utterly defined by data domain, implementation should be created separately each for a problem and may include requests to relation database or to input/output operators.

Rule x[condition]- > y[action] is applyed to term t as follow:

  1. t is matched with pattern x.
  2. On success of previous step, we call check method of facts db with argument condition.
  3. If set return false, we belive that rule is not applicable.
  4. otherwise, we substitute output pattern y as result
  5. and call method set of db facts with action as argument.

TermWare provide implementation of Facts DB with name default in class DefaultClass (API Description)

In this class check and set methods implemented as follow: Logical and ariphmetical expressions are evaluated, if during evaluation we meet functional symbol, with name and arity wich matched name and arity of some method of own class, than this method is called. Argument and result are converted to Java types, if needed, using Java reflection API.

I. e. for calling methods of you facts database from rules just derive you facts database from class DefaultFacts.

4.1.6 IEnv

Except ’logical’ environment, defined in the logic, we have also ’program’ or ’physical’ environment, that defines:

The environment is encapsulated in IEnv interface (API Description)

4.1.7 TermSystem

Now we can define Terminal System, so: Terminal System is rewriting rules with strategies and fact data base and program environment interface totality. (API Description)

Knowing all this we can define the term conversion operations: reduce.

Also we can define methods of rules adding to system, of term reduction and so on. These methods have comparatively simple interface (programmers, who use TermWare as library should start API studying exactly from these methods).

Typical code of terminal system creating looks as follows:

   IEnv env=TermWare.getInstance().createEnv(  
             "ua.kiev.gradsoft.TermWare.envs.SystemLogEnv", envTerm  
                                  );  
 
   ITermRewritingStrategy strategy=TermWare.getInstance().createJavaStrategy(  
             "ua.kiev.gradsoft.TermWare.strategies.TopDownStrategy"  
                                                                  );  
   IFacts facts=TermWare.getInstance().createFacts(  
             "ua.kiev.gradsoft.TermWare.facts.AttributeFacts", env  
                                            );  
   ITermSystem system=new TermSystem(strategy,facts,env);

4.2 Subsidiary Classes

4.2.1 TermwareInstance

TermWareInstance (API Description) is , figuratively, a shank, that contains hierarchical domain system (see Domain class, (API Description), getDomain() method), user dictionaries of language parsers names and printers names.

Usially we have one instance in JVM, but it is possible to create and use few instances when we need few unrelated theories in one JVM (for example inside application server).

4.2.2 IParser, IParserFactory

You can define user language parsers embedding into TermWare system with the help of these interfaces.

General usage pattern looks as follows:

4.2.3 IPrinter, IPrinterFactory

These interfaces define embedding of term own output. The actions should be the same as in previous part, except instead of input stream we use output stream. API Description:

5 Changes

  1. 02.01.2008 - fixed few references to obsolete API.
  2. 28.06.2007 - added description of ’more concrete first’ policy.
  3. 28.03.2007 - reviewed and repackaged for version 2.0.0.
  4. 07.03.2004 - cosmetics.
  5. 07.02.2004 - changed description of default facts database.
  6. 12.01.2004 - first external edition.
  7. 22.01.2003 - first internal edition.
  8. 8.10.2002 - created.

References

[1]   Ruslan Shevchenko. Anatoliy Doroshenko. Managing business logic with symbolic computations. Lecture Notes in Informatics V. 30 - Proceeding of Information Systems Technology and its Applications 2003, pages 143–152, 2003.

[2]   Visser E. Stratego: A language for program transformation based on rewriting strategies. system description of stratego 0.5. Rewriting Techniques and Applications (RTA 01), 2051.:357–361, 2001.

[3]   J.V.Kapitonova A.A.Letichevsky M.S.L’vov and V.A.Volkov. Tools for solving problems in the scope of algebraic programming. LNCS, 958, 1995.