Stars and Constellations
Rays
The language of stellar resolution extends the notion of terms with the concept of rays. A ray is a term where function symbols are polarized with:
+
(positive polarity);-
(negative polarity);- nothing (neutral polarity or absence of polarity).
The compatibility of rays follows the same rules as term unification, except:
- instead of requiring equality
f = g
of function symbols whenf(t1, ..., tn)
is confronted withg(u1, ..., un)
, we requiref
andg
to have opposite polarities (+
versus-
); symbols without polarity cannot interact.
For example:
+f(X)
and-f(h(a))
are compatible with{X:=h(a)}
;f(X)
andf(h(a))
are incompatible;+f(X)
and+f(h(a))
are incompatible;+f(+h(X))
and-f(-h(a))
are compatible with{X:=a}
;+f(+h(X))
and-f(-h(+a))
are compatible with{X:=+a}
.
Stars
With rays, we can form stars. These are unordered collections of rays:
+f(X) -f(h(a)) +f(+h(X))
The empty star is denoted as []
.
Constellations
Constellations are unordered sequences of stars separated by the ;
symbol and
ending with a .
:
+f(X) X; +f(+h(X) a f(b)).
The empty constellation is denoted as {}
.
Constellations are, in fact, the smallest objects we can manipulate. They are the ones that can be executed in the same way programs are executed.