Talk:Occurs check

I replaced the dangling link "logical variable" by a link into "First-order logic#Terms" in introduction section.

I have suggestions regarding the following points of the article:

• In section "Algorithm", the shown algorithm does not provide much new insight as it just defines "occurscheck(x,t)" by "x occurs in t". I'd suggest to omit the algorithm box. Alternatively, a recursive Prolog (or Ml) definition of the predicate (or boolean function) that test whether x occurs in t could be given.
• The goal of syntactic unification in general should be restated in this article. Thereafter, it'd be easier to explain that e.g. $X=f(X)$ has no solution among finite terms, but has one among infinite terms. I'll try to draw a picture showing the introduction of a cycle in this case, if occurs check is omitted.

Meanwhile, I added an example picture; resulting in a poor overall page layout, however. If the picture shall be kept, somebody should improve the page layout. Jochen Burghardt (talk) 23:02, 15 May 2013 (UTC)

• In section "Application in theorem proving", the conclusion that $X=f(X)$ "is only valid if $f$ is the identity", seems at least misleading in the Prolog context, where a solution of $\exists X:X=f(X)$ is sought rather than trying to prove $\forall X:X=f(X)$. While the latter property is in fact valid only if $f$ is the identity, the former is valid if $f$ has any fixpoint. For example $\exists X:X=sqrt(X)$ has two solutions, viz. $X=0$ and $X=1$.
• In section "Prolog implementation", I suggest to write more precisely "some Prolog implementations omit the occurs check ... ", "most ...", or "all current ..."; I don't have the appropriate information, however.
• As far as I know, Colmerauer released Prolog II in the 1980ies, which could handle infinite trees; a related article reference could be I have this reference, but not the article itself.

Jochen Burghardt (talk) 07:54, 15 May 2013 (UTC)

complexity without occur check

There is a funny error in the statement on complexity of unification without occur check. The error has been there in many Prolog manuals for more than 30 years. The following statement (now at the page) is plainly incorrect.

By not performing the occurs check, the worst case complexity of unifying a term $t_{1}$ with term $t_{2}$ is reduced from $O({\text{size}}(t_{1})+{\text{size}}(t_{2}))$ to $O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})))$;

It implies that arbitrarily big terms can be compared in constant time, by unifying eq(t1,t2) with eq(X,X).

I am going to change it by adding "in many cases", and abandoning the reference to a Prolog manual: F. Pereira, D. Warren, D. Bowen, L. Byrd, L. Pereira (1983). C-Prolog's User's Manual Version 1.2 (Technical report). SRI International. Retrieved 21 June 2013.{{cite tech report}}: CS1 maint: multiple names: authors list (link)

--Wlodr (talk) 20:17, 24 October 2015 (UTC)