Rational Trees

Prolog unification is not a complete implementation.

For efficiency considerations, Prolog systems do not perform occur checks while unifying terms. As an example, X = a(X) will not fail but instead will create an infinite term of the form a(a(a(a(a(...))))), or rational tree.

Rational trees are now supported by default in YAP. In previous versions, this was not the default and these terms could easily lead to infinite computation. For example, X = a(X), X = X would enter an infinite loop.

The RATIONAL_TREES flag improves support for these terms. Internal primitives are now aware that these terms can exist, and will not enter infinite loops. Hence, the previous unification will succeed. Another example, X = a(X), ground(X) will succeed instead of looping. Other affected built-ins include the term comparison primitives, numbervars_51 "numbervars/3", @ref copy_term_50 @"copy_term/2", and the internal data base routines. The support does not extend to Input/Output routines or to @ref assert_49 @"assert/1" YAP does not allow directly reading rational trees, and you need to use \@ref write_depth_50 \@"write_depth/2" to avoid entering an infinite cycle when trying to write an infinite term.

Define:

1. IN_UNIFY_C:

1. HAS_CACHE_REGS:

1. tovisit_base:

1. tovisit_base:

1. UnifyAndTrailGlobalCells:

Functions:

1. int Yap_rational_tree_loop(CELL , CELL , CELL , CELL ):

1. static int OCUnify_complex(CELL , CELL , CELL *):

1. static int OCUnify(register CELL, register CELL):

1. static Int p_ocunify(USES_REGS1):

1. static int rational_tree(Term d0):

1. static Int p_cyclic(USES_REGS1):

1. bool Yap_IsAcyclicTerm(Term t):

1. static Int p_acyclic(USES_REGS1):

1. int Yap_IUnify(register CELL d0, register CELL d1):

1. static int unifiable_complex(CELL pt0, CELL pt0_end, CELL *pt1):

1. bool is_unifiable(CELL d0, CELL d1):

1. static Int unifiable(USES_REGS1):

1. int Yap_Unifiable(Term d0, Term d1):

1. void Yap_InitAbsmi(void):

1. void Yap_TrimTrail(void):