From: Markus Triska Date: Mon, 1 Mar 2021 18:42:16 +0000 (+0100) Subject: explain the new occurs_check flag X-Git-Tag: v0.9.0~145^2 X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=b77bdabca69ec4eb892ba8d1c110327a4cfb3e85;p=scryer-prolog.git explain the new occurs_check flag --- diff --git a/README.md b/README.md index f11a4c97..3bd1e064 100644 --- a/README.md +++ b/README.md @@ -309,6 +309,53 @@ about strings. Partial strings were first proposed by Ulrich Neumerkel in issue [#95](https://github.com/mthom/scryer-prolog/issues/95). +### Occurs check and cyclic terms + +The *occurs check* is an element of algorithms that perform +syntactic unification, causing the unification to fail if a variable +is unified with a term that contains that variable as a proper +subterm. For efficiency, the *occurs check* is omitted by default +in Scryer Prolog and many other Prolog systems. + +In Scryer Prolog, performing unifications which succeed only if the +*occurs check* is omitted yield *cyclic terms*, also called +*rational trees*. For example: + +``` +?- X = f(X), Y = g(X,Y). + X = f(X), Y = g(f(X),Y). +``` + +The creation of cyclic terms often indicates a programming mistake in +the formulation of Prolog predicates, and to obtain logically sound +results it is desirable to either perform all unifications with +*occurs check* enabled, or let Prolog throw an error if enabling +the *occurs check* is necessary to prevent a unification. + +Scryer Prolog supports this via the Prolog flag `occurs_check`. It can +be set to one of the following values to obtain the desired behaviour: + +- `false` + Do not perform the *occurs check*. This is the default. +- `true` + Perform all unifications with the *occurs check* enabled. +- `error` + Yield an error if a unification is performed that the + *occurs check* would have prevented. + +Especially when starting with Prolog, we recommend to add the +following directive to the `~/.scryerrc` configuration file so that +programming mistakes in predicates that lead to the creation of cyclic +terms are indicated by errors: + +``` +:- set_prolog_flag(occurs_check, error). +``` + +Scryer Prolog implements specialized reasoning to make unifications +fast in many frequently occurring situations also if the +*occurs check* is enabled. + ### Tabling (SLG resolution) One of the foremost attractions of Prolog is that logical consequences