explain the new occurs_check flag

diff --git a/README.md b/README.md
index f11a4c97cc1aacd73bb7815e4a74690cbb616aba..3bd1e0642157eda7ed55e65e9256baa68219b5f8 100644 (file)
--- 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