Stack Overflow
Stack Overflow

Questions tagged [occurs-check]

The occurs-check is a part of algorithms for syntactic unification. Prolog implementations usually omit the occurs-check for reasons of efficiency, which can lead to circular data structures and looping. But an implementation specific Prolog flag might enable occurs check and a variety of optimizations can render it feasible for common cases.

16 questions
38
votes
5 answers

Unification with STO detection

In ISO Prolog unification is defined only for those cases that are NSTO (not subject to occurs-check). The idea behind is to cover those cases of unifications that are mostly used in programs and that are actually supported by all Prolog systems.…
false
  • 10,264
  • 13
  • 101
  • 209
7
votes
3 answers

Does Prolog need GC when the occurs check is globally enabled?

As far as I can tell, with sound unification, SLD resolution should not create cyclic data structures (Is this correct?) If so, one could, in theory, implement Prolog in such a way that it wouldn't need garbage collection (GC). But then again, one…
MWB
  • 11,740
  • 6
  • 46
  • 91
7
votes
2 answers

What does Prolog do if you X = f(X)?

What does it mean in Prolog comparing a predicate to an unbound variable?
Pedro Montoto García
  • 1,672
  • 2
  • 18
  • 38
6
votes
2 answers

What occurs-check optimizations is SWI Prolog using?

To quote the SICStus Prolog manual: The usual mathematical theory behind Logic Programming forbids the creation of cyclic terms, dictating that an occurs-check should be done each time a variable is unified with a term. Unfortunately,…
MWB
  • 11,740
  • 6
  • 46
  • 91
6
votes
2 answers

Prolog matching vs miniKanren unification

In Prolog - Programming for Artificial Intelligence, Bratko says the following on page 58. "Matching in Prolog corresponds to what is called unification in logic. However, we avoid the word unification because matching, for for efficiency reasons in…
user3139545
  • 6,882
  • 13
  • 44
  • 87
5
votes
3 answers

How can Prolog derive nonsense results such as 3 < 2?

A paper I'm reading says the following: Plaisted [3] showed that it is possible to write formally correct PROLOG programs using first-order predicate-calculus semantics and yet derive nonsense results such as 3 < 2. It is referring to the fact…
MWB
  • 11,740
  • 6
  • 46
  • 91
5
votes
1 answer

How to enable the occurs check in all unifications in SWI-Prolog?

According to Wikipedia: Implementations offering sound unification for all unifications are Qu-Prolog and Strawberry Prolog and (optionally, via a runtime flag): XSB, SWI-Prolog and Tau Prolog. However, when I do apropos(occur) it only finds…
MWB
  • 11,740
  • 6
  • 46
  • 91
5
votes
2 answers

dif with occurs check

Is there a dif with occurs check? This here works: Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7) ?- set_prolog_flag(occurs_check, true). true. ?- dif(X,f(Y)), X = Y. X = Y. But the above is not feasible, since occurs check is a global…
user502187
4
votes
3 answers

Pure Prolog Scheme Quine

There is this paper: William E. Byrd, Eric Holk, Daniel P. Friedman, 2012 miniKanren, Live and Untagged Quine Generation via Relational Interpreters http://webyrd.net/quines/quines.pdf Which uses logic programming to find a Scheme Quine.…
user502187
3
votes
1 answer

Why `f(a)=a` fails but `f(X)=X` succeeds in prolog?

I came across following: ?- f(X) = X. X = f(X). ?- f(a) = a. false. Why unification works for f(X) = X, but not for f(a) = a? Is it because first simply says name return value of f(X) as X, whereas second tries to check if return value of f(a) is…
Rnj
  • 1,067
  • 1
  • 8
  • 23
3
votes
2 answers

Proper unify_with_occurs_check/2 in SWI-Prolog?

Got this strange behaviour. I was running these test cases: s1 :- Q=[[lambda,symbol(_3026),[cons,[quote,_3434], [quote,_3514]]],[quote,_3206]], P=[_3434|_3514], freeze(_3434, (write(foo), nl)), unify_with_occurs_check(P, Q). s2 :- …
user502187
3
votes
3 answers

Do modern Prolog compilers optimize away the occurs check automatically, when it's safe?

Edit: This question assumes you enabled the occurs check. It's not about setting Prolog flags. There was a bunch of papers 30 years ago about optimizing away the occurs check automatically, when it's safe (about 90% of predicates, in typical…
MWB
  • 11,740
  • 6
  • 46
  • 91
2
votes
2 answers

What is a simple worst case for occurs check in Prolog?

Many papers do note that an equational unification problem such as below, might run in exponential time, when occurs_check=true. There is no stipulation that this is a top-level query or a clause body, its just the equational unification problem: …
user502187
1
vote
1 answer

How to safely temporarily change the occurs check flag?

I am using the following code to temporarily change the occurs check flag, where G is a goal that doesn't create any delayed goals: with_occurs_check(G) :- current_prolog_flag(occurs_check, F), setup_call_cleanup( …
user502187
1
vote
1 answer

Simulating occurs_check=error in SICStus Prolog

It turns out that SICStus Prolog doesn't have an occurs_check Prolog flag. At least we couldn't find one, and this here gives an error message: /* SICStus 4.6.0 (x86_64-win32-nt-4) */ ?- set_prolog_flag(occurs_check, true). Domain error in argument…
user502187
1
2