Basic Concepts

  

Figure: An agent and a rewrite rule

  

Figure: One-step reduction

We need some preliminary concepts.

• A is a countable set of names of agents. To each name of an agent two arities are assigned: one is for first order terms and the other for ports. We use upper case letters A,B,...,Append,... to denote names of agents;
• F is a countable set of function symbols. Each function symbol has an arity. A 0-ary function symbol is called constant symbol. We use lower case letters a,b,...,f,g... to denote function symbols.
• An agent has the form of Figure , where A is the name of the agent and t₁,...,t_n are first order terms. The arity of A for terms must be n and that for ports must be m . The distinguished edge is called the principal port of A and the other edges auxiliary ports.
  We use Greek letters a,b,... to denote agents.
• We assume given a set of countable unification (or logical) variables
  X,Y,..., denoted by X . Then we define X^- , the set of the guarded unification variables by X^- = {X^- | X in X} .
• A net is a graph with agents as nodes.

Definition 1

An additive interaction program is a triple <A, S, R> , where

1.

A is a finite set of names of agents.

2.

The alphabet S (a subset of F) is a finite set of function symbols. We define the set Ter(S) of the first order terms over inductively:

(a)

If X is in X , then X is in Ter(S) ;

(b)

If X^- is in X^-, then X^- is in Ter(S) ;

(c)

If f is in S, f is n -ary, and t₁,...,t_n are in Ter(S) , then f (t₁,...,t_n) is in Ter(S) .

3.

R is a finite set of rewrite rules. Each rewrite rule has the form in Figure . In Figure , and are agents. N is a net. We call the left side of the arrow redex and the right side contractum. All the names of the agents in R must belong to A and all the terms of the agents in R must belong to Ter(S) .

We say that two agents A(s₁,...,s_h) and B(t₁,...,t_k) in a net without guarded unification variables are reducible if the two agents are connected by their principal ports in the net.
Let r be a rewrite rule. Reducible two agents A(s₁,...,s_h) and B(t₁,...,t_k) in a net are unifiable with r if the two agents in the redex of r have the form A(u₁,...,u_h) and B(v₁,...,v_k) and the equation E = {s₁ =^. u₁,...,s_h =^. u_h,t₁ =^. v₁,...,t_k =^. v_k} has the most general unifier .
When reducible agents A(s₁,...,s_h) and B(t₁,...,t_k) in a net N are unifiable with the rewrite rule of the left side of Figure  by q , the rewrite rule can apply to the net N . The right side of Figure  shows an application of the rule. In Figure , q^- N is the net that is obtained from N by replacing every term w in N by q^- w , where q^- is defined by q^- = [s₁/X^-₁,...,s_l/X^-_l,s₁/X₁,..., s_l/X_l] when q = [s₁/X₁,...,s_l/X_l] . In the rest of the paper, we simply call the situation a one-step reduction of two agents A(s₁,...,s_h) and B(t₁,...,t_k) in N .
From the definition of the one-step reduction, we can define a reduction relation on nets and normal forms of nets as usual.