Sto unification/1

From Prologstandard

Name is unintuitive.

ISO Standard

3.165 STO: Subject to occurs-check (see 7.3.3)

7.3.3 Subject to occurs-check (STO) and not subject to occurs-check (STO)

A set of equations (or two terms) is "subject to occurs-check" (STO) iff there exists a way to proceed through the steps of the Herbrand Algorithm such that 7.3.2 g happens.

7.3.2 g) If there is an equation of the form X = t such that X is a variable ant t is a non-variable term which contains this variable, then exit with failure (not unifiable, positive occurs-check).

Options:

• Keep existing name
• Add new name
• Keep and add new name

Naming:

• occurs_check/1
• cyclic_unify(fail)
• cyclic_unify(cyclic)
• cyclic_unify(unsafe)
• subject_to_occurs_check_unification/1
• unification_occurs_check/1
• unification_subj_to_occurs_check/1
• cyclic_unification/1

• occurs_check_violations(fail)
• occurs_check_violations(unsafe)
• occurs_check_violations(cyclic)