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

Definition 8. Let σ and ϑ be two substitutions:

s 1 ,...,s 1 s 1 ,...,s k m σ = { x 1 → t 1 ,...,x n → t n , x 1 →

k 1

,...,x m → ,

f 1 → f 1 ,...,f 1

l 1

,...,f r → f 1 ,...,f l r } ,

q m
1

,...,q m q 1 ,...,q 1 ϑ = { y 1 → r 1 ,...,y n → r n , y 1 →

k 1

,...,y m →

k m

,

g 1 ,...,g 1 g r 1 ,...,g r

g 1 →

l 1

,...,g r →

l r }

.

Then the composition of σ and ϑ , σϑ , is the substitution obtained from the set

s 1 ϑ,...,s 1 s 1 ϑ,...,s k m ϑ { x 1 → t 1 ϑ,...,x n → t n ϑ, x 1 → ϑ ,...,x m → ,

k 1

f 1 ϑ,...,f 1 f 1 ϑ,...,f l r ϑ

f 1 → ϑ ,...,f r → ,

l 1

q 1 ,...,q 1 q m 1 ,...,q m y 1 → r 1 ,...,y n → r n , y 1 →

k 1

,...,y m →

k m

,

g 1 → g 1 ,...,g 1

l 1

,...,g r → g r 1 ,...,g r

l r }

by deleting

1. all the bindings x i → t i ϑ ( 1 ≤ i ≤ n )forwhich x i = t i ϑ ,

s 1 ϑ,...,s i k i ϑ

2. all the bindings x i → ( 1 ≤ i ≤ m ) for which the sequence

s 1 ϑ,...,s i k i ϑ consists of a single term x i ,
3. all the sequence function symbol bindings f i →

r )
such that the sequence f 1 ϑ,...,f l r ϑ consists of a single function symbol f i ,
4. all the bindings y i →

f 1 ϑ,...,f l i ϑ ≤ i ≤

( 1

n ) such that y i ∈{ r i ( 1 ≤ i ≤ x 1 ,...,x n } ,

q 1 , ..., q k i m )with y i ∈{

5. all the bindings y i → ( 1 ≤ i ≤ x 1 ,...,x m } ,

g 1 , ..., g l i r )

6. all the sequence function symbol bindings g i → ( 1 ≤ i ≤

such that g i ∈{

f 1 ,...,f r } .

Example 3. Let σ = { x → y, x → y, x , y → f ( a, b ) ,y,g ( x ) , f → g, h }

and ϑ = { y → x, y → x, x → , g → g 1 , g 2 } be two substitutions. Then

σϑ = { y → x, y → f ( a, b ) ,x,g 1 () , g 2 () , f → g 1 , g 2 , h , g → g 1 , g 2 } .

Definition 9. A substitution σ is called linearizing away from a finite set of
sequence function symbols Q iff the following three conditions hold: (1) C od ( σ ) ∩

Q = ∅ .(2)Forall f,g ∈D om ( σ ) ∩Q ,if f = g ,then { fσ }∩{ gσ } = ∅ .(3)If

f → g 1 ...,g n ∈ σ and f ∈Q ,then g i = g j for all 1 ≤ i<j ≤ n .

Intuitively, a substitution linearizing away from Q either leaves a sequence

function symbol in , binding it with

a sequence of distinct sequence function symbols that do not occur in

Q “unchanged”, or “moves it away from” Q

Q ,and

maps different sequence function symbols to disjoint sequences.
Let E be a set of equations over

F and V .By ≈ E we denote the least con-

gruence relation on T ( F , V ) that is closed under substitution application and

contains E . More precisely, ≈ E contains E , satisfies reflexivity, symmetry, tran-

sitivity, congruence, and a special form of substitutivity: For all s, t ∈T ( F , V ),