| Description: |
The least general generalization of terms is inductively defined as follows:
- Let X be a variable and t be an arbitrary term, different
from X.
Then LGG (X, t) = Y, for a variable Y, not appearing in
t.
- Let f and g be different function symbols and
t1, ..., tn, u1, ...,
un be arbitrary terms.
Then
- LGG( f(t1, ..., tn),
f(u1, ..., un) )
:= f( LGG( t1, u1), ...,
LGG( tn, un) ).
- LGG( f(t1), g(u1) ) = Y,
where Y is a variable not appearing in
t1 or u1.
- If t, u and v are terms and LGG(t, u) = v then
LGG(u, t) = v.
It has the following properties:
If t1 and t2 are terms and tlgg =
LGG(t1, t2) is their least general
generalization, then
-
there exist substitutions θ1 and
θ2, such that
-
tlggθ1 = t1 and
-
tlggθ2 = t2.
-
for every term tgen with substitutions
θ1 and θ2, such that
-
tgenθ1 = t1
and
-
tgenθ2 = t2,
there exists a substitution ρ, such that
tgenρ = tlgg.
In other terms, there is no more specific generalization of
t1 and t2 than their LGG.
Further properties: For all terms t1, t2 and
t2 the following equations hold.
-
LGG(t1, t2) = LGG (t2,
t1)
-
LGG( LGG(t1, t2), t3)
= LGG( t1, LGG(t2, t3))
-
LGG(t1, t1) = t1
|
