Solving Equations Involving Sequence Variables and Sequence Functions - Artificial Intelligence and Symbolic Computation - page 159

in T ;by V ar ( T )theset IV ar ( T ) ∪SV ar ( T ); by IF un ( T )(resp.by SF un ( T ))

the set of all individual (resp. sequence) function symbols in T ;by F ix ( T )(resp.

by lex ( T )) the set of all fixed (resp. flexible) arity function symbols in T .

Definition 2. A variable binding is either a pair x

F

→ t where t ∈T Ind ( F , V )

3

and t = x , or an expression x → t 1 ,...,t n where n ≥ 0 , for all 1 ≤ i ≤ n

we have t i ∈T ( F , V ) ,andif n =1 then t 1 = x .

Definition 3. A sequence function symbol binding is an expression of the form
f → g 1 ,...,g m , where m ≥ 1 ,if m =1 then f = g 1 , and either f,g 1 ,...,g m ∈

Fix Flex

F

Seq ,with

A r ( f )= A r ( g 1 )= ··· = A r ( g m ) ,or f,g 1 ,...,g m ∈F

Seq .

Definition 4. A substitution is a finite set of bindings { x 1 → t 1 ,...,x n →

s 1 ,...,s 1 s 1 ,...,s k m g 1 ,...,g 1

t n , x 1 →

k 1

,...,x m → , f 1 →

l 1

,...,f r →

g 1 ,...,g l r }

0 , x 1 ,...,x n , x 1 ,...,x m are distinct variables and
f 1 ,...,f r are distinct sequence function symbols.
Lower case Greek letters are used to denote substitutions. The empty sub-
stitution is denoted by ε .
Definition 5. The instance of a term t with respect to a substitution σ ,denoted
tσ , is defined recursively as follows:
1. xσ = t, if x

where n, m, r ≥

→ t ∈ σ,

x, otherwise .

2. xσ = t 1 ,...,t n , if x

→ t 1 ,...,t n ∈ σ, n ≥ 0 ,

x, otherwise .
3. f ( t 1 ,...,t n ) σ = f ( t 1 σ,...,t n σ ) .
4. f ( t 1 ,...,t n ) σ =

g 1 ( t 1 σ,...,t n σ ) ,...,g m ( t 1 σ,...,t n σ ) ,

if f → g 1 ,...,g m ∈ σ,

f ( t 1 σ,...,t n σ ) , otherwise .

Example 2. Let σ = { x → a, y → f ( x ) , x → , y → a, x , g → g 1 , g 2 } . Then

f ( x, x, g ( y, g ()) , y )) σ = f ( a, g 1 ( f ( x ) , g 1 () , g 2 ()) , g 2 ( f ( x ) , g 1 () , g 2 ()) ,a,x ) .
Definition 6. The application of σ on f ,denoted fσ , is a sequence of function
symbols g 1 ,...,g m if f σ .Otherwise fσ = f .

Applying a substitution θ on a sequence of terms

→ g 1 ,...,g m ∈

t 1 ,...,t n gives a sequence

of terms .

Definition 7. Let σ be a substitution. (1) The domain of σ is the set

t 1 θ,...,t n θ

D om ( σ )=

{ l | lσ

= l

}

of variables and sequence function symbols. (2) The codomain of σ

is the set C od ( σ )= { lσ | l ∈D om ( σ ) } of terms and sequence function symbols 4 .

(3) The range of σ is the set R an ( σ )= V ar ( C od ( σ )) of variables.

3 To improve readability, we write sequences that bind sequence variables between
and .
4 Note that the codomain of a substitution is a set of terms and sequence function
symbols, not a set consisting of terms, sequences of terms, sequence function symbols,
and sequences of sequence function symbols. For instance, Cod ( {x → f ( a ) , x →

a, a, b , c → c 1 , c 2 } )= {f ( a ) ,a,b,c 1 , c 2 } .