I am mildly shocked

On 7/9/2024 2:05 PM, Mild Shock wrote:

In unification with occurs check cycles in a graph
are prevented before they happen. You are such a moron.

You did not word that exactly correctly.

The "occurs check" does that. It checks V ∈ T, BEFORE
a variable V gets instantiated to T.
 

It checks for the absence of cycles and returns
false when it finds cycles.
I created Minimal Type Theory for this purpose before
I know that Prolog could to the same thing.
https://www.researchgate.net/publication/315367846_Minimal_Type_Theory_MTT

On the other hand acyclic_term/1 can figure out whether
a term as variable V instantiated to T, where V ∈ T,
AFTER a cycle allowing unification has been performed,
i.e. the ordinary (=)/2.
 You are an idiot, you confuse these predicate:
 - acyclic_term/1
 With this predicate:
 - unify_with_occurs_check/2.
 Usually unify_with_occurs_check/2 is not implemented as:
 /* not how it is done */
unify_with_occurs_check(X,Y) :-
     X = Y,
     acyclic_term(X).
 The problem is the above wouldn't allow enough fast failure.
 

Clocksin & Mellish says that it is optional because
it really slows things down. The Cyc project has to
take all kinds of short-cuts on these things to reduce
time to feasible from infeasible.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer