Information Technology Reference
In-Depth Information
then = λ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