非表示:
キーワード:
-
要旨:
For efficiency reasons, most Prolog implementations do not include an occur
check in their unification algorithms and thus do not conform to the semantic
model of first-order logic. We present a simple test which guarantees that
unification without occur check is sound in programs satisfying the conditions
of the test. We designate each argument position of every predicate as either
an input or an output position and then describe a sufficient condition in
terms of this designation for unification without occur check to be sound.
Unification with occur check can be performed in places in the program where
this condition is not satisfied. Two algorithms for implementing this test are
described and compared.
