Information Technology Reference
In-Depth Information
if
s
≈
E
tσ
. Substitutivity in this
form requires that
sσ
and
tσ
must be single terms, not arbitrary sequences of
terms. The set
≈
E
t
and
sσ, tσ
∈T
(
F
,
V
)forsome
σ
,then
sσ
≈
E
is called an
equational theory
defined by
E
.Inthesequel,
we will also call the set
E
an equational theory, or
E
-theory. The
signature
of
E
is the set
un
(
E
). Solving equations in an
E
-theory
is called
E
-unification
. The fact that the equation
s
S
ig
(
E
)=
IF
un
(
E
)
∪SF
≈
t
hastobesolvedinan
?
E
E
-theory is written as
s
≈
t
.
Definition 10.
Let
E
be an equational theory with
S
ig
(
E
)
⊆F
.An
E
-unifi-
?
E
?
E
cation problem
over
F
is a finite multiset
Γ
=
{
s
1
≈
t
1
,...,s
n
≈
t
n
}
of
equations over
F
and
V
.An
E
-unifier
of
Γ
is a substitution
σ
such that
σ
is
linearizing away from
SF
un
(
Γ
)
and for all
1
≤
i
≤
n
,
s
i
σ
≈
E
t
i
σ.
The set of
all
E
-unifiers of
Γ
is denoted by
U
E
(
Γ
)
,and
Γ
is
E
-unifiable
iff
U
E
(
Γ
)
=
∅
.
If
{
s
1
≈
?
E
t
1
,...,s
n
≈
?
E
t
n
}
is a unification problem, then
s
i
,t
i
∈T
Ind
(
F
,
V
)
for all 1
≤
i
≤
n
.
?
∅
Example 4.
Let
Γ
=
{
f
(
g
(
x, y, a
))
≈
f
(
g
(
c, b, x
))
}
.Then
{
x
→
c
1
, y
→
c
2
,b
,
x
→
a, c
→
c
1
, c
2
}∈U
∅
(
Γ
).
?
∅
. If we did not require
the
E
-unifiers of a unification problem to be linearizing away from the sequence
function symbol set of the problem, then
Γ
would have
Let
Γ
=
{
f
(
g
(
x, y, a
))
≈
f
(
h
(
c, x
))
}
.Then
U
∅
(
Γ
)=
∅
∅
-unifiers, e.g.,
{
x
→
c
1
, y
→
c
2
,b
,x
→
a, g
→
h, c
→
c
1
, c
2
}
would be one of them.
In the sequel, if not otherwise stated,
E
stands for an equational theory,
X
for a finite set of variables, and
Q
for a finite set of sequence function symbols.
Definition 11.
A substitution
σ
is called
erasing
on
X
modulo
E
iff either
f
(
v
)
σ
≈
E
f
()
for some
f
∈S
ig
(
E
)
and
v
∈X
,or
x
→
∈
σ
for some
x
∈X
.
We call
σ
non-erasing
on
X
modulo
E
iff
σ
is not erasing on
X
modulo
E
.
Example 5.
Any substitution containing
x
→
is erasing modulo
E
=
∅
on
any
that contains
x
.
Let
E
=
X
{
f
(
x, f
(
y
)
, z
)
≈
f
(
x, y, z
)
}
and
X
=
{
x, x
}
. Then any substitution
that contains
x
→
f
(), or
x
→
,or
x
→
t
1
,...,t
n
with
n
≥
1and
t
1
=
···
=
t
n
=
f
(), is erasing on
X
modulo
E
. For instance, the substitutions
{
x
→
f
()
}
,
{
x
→
f
()
}
,
{
x
→
}
,
{
x
→
f
()
,f
()
,f
()
,f
()
}
are erasing on
X
modulo
E
.
Definition 12.
A substitution
σ
agrees
with a substitution
ϑ
on
X
and
Q
mod-
ulo
E
,denoted
σ
=
X,Q
E
ϑ
,iff(1)forall
x
∈X
,
xσ
≈
E
xϑ
;(2)forall
f
∈Q
,
fσ
=
fϑ
;(3)forall
x
∈X
,thereexist
t
1
,...,t
n
,s
1
,...,s
n
∈T
(
F
,
V
)
,
n
≥
0
,
such that
xσ
=
t
1
,...,t
n
,
xϑ
=
s
1
,...,s
n
and
t
i
≈
E
s
i
for each
1
≤
i
≤
n
.
Example 6.
Let
σ
=
{
x
→
a
}
,
ϑ
=
{
x
→
b, c
, a
→
b, c
}
,and
ϕ
=
{
x
→
.Then
σϕ
=
X,Q
E
b, c
, a
→
b, c
}
.Letalso
X
=
{
x
}
,
Q
=
{
a
}
,and
E
=
∅
ϑ
.
Definition 13.
A substitution
σ
is
more general
(resp.
strongly more general
)
than
ϑ
on
≤
X,Q
E
X,Q
E
ϑ
), iff
σϕ
=
X,Q
E
X
and
Q
modulo
E
,denoted
σ
ϑ
(resp.
σ
ϑ
for some substitution (resp. substitution non-erasing on
X
modulo
E
)
ϕ
.
Search WWH ::
Custom Search