Information Technology Reference
In-Depth Information
then
fσ
=
λx
1
....x
n
.
g
1
(
x
1
,...,x
n
)
,...,g
m
(
x
1
,...,x
n
)
,where
m>
1and
g
1
,...,g
m
are fresh variables of the same sort as
f
.
Hence, syntactic sequence unification can be considered as order-sorted se-
cond-order AU-unification with additional restrictions. Order-sorted higher-or-
der syntactic unification was investigated in [9], but we are not aware of any
work done on order-sorted higher-order equational unification.
5 Unification Procedure
In the sequel we assume that
Γ
, maybe with indices, and
Γ
denote syntactic
sequence unification problems. A
system
is either the symbol
⊥
(representing
failure), or a pair
consists of the transformation
rules on systems listed below. The function symbol
g
Γ
;
σ
. The inference system
U
Flex
Ind
intherulePD2is
new. In the Splitting rule
f
1
and
f
2
are new sequence function symbols of the
same arity as
f
in the same rule. We assume that the indices
n, m, k, l
∈F
≥
0.
Projection (P):
Γ
;
σ
=
⇒Γϑ
;
σϑ,
where
ϑ
=
ε, Dom
(
ϑ
)
⊆SVar
(
Γ
)and
Cod
(
ϑ
)=
∅.
Trivial (T):
{s ≈
s}∪Γ
;
σ
=
⇒Γ
;
σ.
Orient 1 (O1):
{
?
∅
?
∅
Γ
;
σ
?
∅
Γ
;
σ
s
≈
x
}∪
=
⇒{
x
≈
s
}∪
,
if
s/
∈V
Ind
.
Orient 2 (O2):
{f
(
s, s
1
,...,s
n
)
≈
?
∅
f
(
x, t
1
,...,t
m
)
}∪Γ
;
σ
=
⇒
?
∅
f
(
s, s
1
,...,s
n
)
}∪Γ
;
σ,
{f
(
x, t
1
,...,t
m
)
≈
if
s∈V
Seq
.
Solve (S):
{
?
∅
Γ
;
σ
Γ
ϑ
;
σϑ
x
≈
t
}∪
=
⇒
,
if
x/
∈IV
ar
(
t
)and
ϑ
=
{
x
→
t
}
.
Total Decomposition (TD):
{f
(
s
1
,...,s
n
)
≈
?
∅
f
(
t
1
,...,t
n
)
}∪Γ
;
σ
=
⇒
t
n
}∪Γ
;
σ
if
f
(
s
1
,...,s
n
) =
f
(
t
1
,...,t
n
)
,
and
s
i
,t
i
∈T
Ind
(
F, V
) for all 1
≤ i ≤ n.
Partial Decomposition 1 (PD1):
{f
(
s
1
,...,s
n
)
≈
?
∅
?
∅
{s
1
≈
t
1
,...,s
n
≈
?
∅
f
(
t
1
,...,t
m
)
}∪Γ
;
σ
=
⇒
f
(
t
k
,...,t
m
)
}∪Γ
;
σ
if
f
(
s
1
,...,s
n
) =
f
(
t
1
,...,t
m
)
,
for some 1
<k≤ min
(
n, m
)
,
s
k
∈T
Seq
(
F, V
)or
t
k
∈T
Seq
(
F, V
)
,
and
s
i
,t
i
∈T
Ind
(
F, V
) for all 1
≤ i<k.
Partial Decomposition 2 (PD2):
{f
(
f
(
r
1
,...,r
k
)
,s
1
,...,s
n
)
≈
?
∅
?
∅
?
∅
{s
1
≈
t
1
,...,s
k−
1
≈
t
k−
1
,f
(
s
k
,...,s
n
)
≈
?
∅
f
(
f
(
q
1
,...,q
l
)
,t
1
,...,t
m
)
}∪Γ
;
σ
=
⇒
f
(
t
1
,...,t
m
)
}∪Γ
;
σ.
if
f
(
f
(
r
1
,...,r
k
)
,s
1
,...,s
n
) =
f
(
f
(
q
1
,...,q
l
)
,t
1
,...,t
m
)
.
Sequence Variable Elimination 1 (SVE1):
{f
(
x, s
1
,...,s
n
)
≈
?
∅
?
∅
{g
(
r
1
,...,r
k
)
≈
g
(
q
1
,...,q
l
)
,f
(
s
1
,...,s
n
)
≈
?
∅
f
(
x, t
1
,...,t
m
)
}∪Γ
;
σ
=
⇒
f
(
t
1
,...,t
m
)
}∪Γ
;
σ
if
f
(
x, s
1
,...,s
n
) =
f
(
x, t
1
,...,t
m
)
.
?
∅
{f
(
s
1
,...,s
n
)
≈
Search WWH ::
Custom Search