Prologs with Occurs Check constantly on?
Jan Burse
Are there any Prologs with Occurs Check
constantly on?
Looking at some program examples and
oportunities that are present when code
is generated. I have the feeling that
Prologs with Occurs Check on should run
in similar time as Prologs with Occurs
Check off.
Despite the theoretical limitations to
make it fast and despite the known
worst-cases.
For example if I look at append/3:
append([],X,X).
append([X|Y],Z,[X|T]) :- append(Y,Z,T).
I generate the following trivial code:
append([], X, X).
1 unify_atomic _0, []
2 unify_term _1, _2
append([X | Y], Z, [X | T]) :-
append(Y, Z, T).
3 unify_compound _0, [X | Y]
4 unify_compound _2, [X | T]
5 unify_var _1, Z
6 last_goal append(Y, Z, T)
7 last_cont
For occurs check constantly on, I would
only need to replace the following lines:
2' unify_term_with_occurs_check _1, _2
4' unify_compound_with_occurs_check _2, [X | T]
So the code already reduced the number
of needed unification with occurs checks.
4' could profit from unraveling the unification
and we would end up with:
4'' unify_term_with_occurs_check _2', _0'
But question is whether the two remaining
unify_term_with_occurs_check could be further
speed up with some runtime annotations
in the terms.
I have the feeling something could be done
with a ref count annotation. If Var has
ref count=0, then checking Var occurs in Term
is futil. Unfortunately all my Vars have
initially ref count=1.
Hm...
Best Regards
Paulo Moura
> Dear All,
>
> Are there any Prologs with Occurs Check
> constantly on?
> Looking at some program examples and
I think that's the case with Qu-Prolog.
Cheers,
Paulo
Peter Robinson
As Paulo says Qu-Prolog does have occurs check turned on for all
unifications (in principle).
Many years ago we added what seemed to be a simple optimization that
turns out to be very effective in practice. The data structure for
variables takes up two words - one is a pointer and the other is for a
collection of flags (as bits). One of those flags is set when the
variable first appears in a structure.
When a variable is unified with a term that flag is checked - if it is
not set then occurs checking is avoided.
The append example is one in which this trick does not work because the
T in the second clause gets flagged and when the bottom of the recursion
is hit then the unification is done with occurs check.
That makes the complexity of append (as joining) proportional to the
length of the first list + size of the second list.
(In your step 3 occurs checking is not needed because these are new
variables (that haven't been in a structure yet).)
Peter
Jan Wielemaker
> Dear All,
>
> Are there any Prologs with Occurs Check
> constantly on?
set_prolog_flag(occurs_check, true).
I do not know whether anyone uses this. Surely some programs rely on
rational trees. I've used the value `error' a few times, which
performs the Occurs Check, but throws an exception rather than
failing if it detects that a unification would create a cycle.
Surely, the overhead is acceptable on a wide range of programs
(a few percent).
Cheers --- Jan
Ulrich Neumerkel
>Dear All,
>
>Are there any Prologs with Occurs Check
>constantly on?
>
>Looking at some program examples and
>oportunities that are present when code
>is generated. I have the feeling that
>Prologs with Occurs Check on should run
>in similar time as Prologs with Occurs
>Check off.
> append([],X,X).
> append([X|Y],Z,[X|T]) :- append(Y,Z,T).
>For occurs check constantly on, I would
>only need to replace the following lines:
>
> 2' unify_term_with_occurs_check _1, _2
>
> 4' unify_compound_with_occurs_check _2, [X | T]
>
>So the code already reduced the number
>of needed unification with occurs checks.
>4' could profit from unraveling the unification
>and we would end up with:
>
> 4'' unify_term_with_occurs_check _2', _0'
Any Prolog which distinguishes local variables not occuring in structures
from heap variables can do your optimizations without any adaptation
of the intermediate code.
E.g., in SWI for 2', there is one occurs-check in the head of the fact,
but only if neither the 2nd nor 3rd argument is a local variable.
4'' will always be occurs-checked, because the heads of the
lists will always be allocated on the heap.
Since append([], X,s(X)) and append([X],[],[s(X)]) require the
occurs-check, an optimization in that place would need to take
goals like them into account.
>I have the feeling something could be done
>with a ref count annotation. ...
Possible. One argument against reference counting has been its
inability to detect cycles. But if the occurs-check is always on,
there are no cyclic structures. Not sure if this leads to anything
useful. There are many kinds of reference counting schemes like one bit,
weighted ...
Ulrich Neumerkel
>On 2011-10-09, Jan Burse <janb...@fastmail.fm> wrote:
>> Dear All,
>>
>> Are there any Prologs with Occurs Check
>> constantly on?
>
>SWI-Prolog after
>
> set_prolog_flag(occurs_check, true).
>
Do you remember Geoff Sutcliffe and TPTP ... ? That was one of the
reasons why he used SWI.
Jan Wielemaker
I recognise it has some value in both theorem proving (true) and
warn novices against X = X+1 misconceptions (error mode).
Cheers --- Jan
Ulrich Neumerkel
>All I remember is that we discussed this. It didn't seem hard and
>I recognise it has some value in both theorem proving (true) and
>warn novices against X = X+1 misconceptions (error mode).
The error mode is definitely the more helpful one. In particular, when
debugging programs.
Jan Burse
> Any Prolog which distinguishes local variables not occuring
> in structures from heap variables can do your optimizations
> without any adaptation of the intermediate code.
> E.g., in SWI for 2', there is one occurs-check in the head of the fact,
> but only if neither the 2nd nor 3rd argument is a local variable.
thoughs, since have first to check out what a
classification of arguments into local and heap
variables would mean in a molec implementation
where this information is not readily available.
Not sure whether a counterpart can be found. Sniff.
Something else: Could it be that any optimization that
avoids unify_term_with_occurs_check would be also useful
for cyclic term unification? Instead that we place into
the code:
unify_term_with_occurs_check (1)
We would place into the code:
unify_term_with_existing_or_newly_resulting_cycles (2)
So all other places would use a slightly faster simple
unification. But eventually the heuristics for (1) and (2)
will be not exactly the same.
Bye
Jan Burse
> SWI-Prolog after
>
> set_prolog_flag(occurs_check, true).
Something else: I was thinking of a compile time
based occurs_check on/off thing, because it could be
applied selectively to code.
So instead of a flag that would affect the runtime,
if we had a flag that would affect the compile time,
we could for example compile certain modules without
occurs check and others with occurs check.
:- set_prolog_flag(clause_unify_checked, on).
/*
code where we want to have occurs check on
goes here.
*/
:- set_prolog_flag(clause_unify_checked, off).
Jan Wielemaker
clear :-(
As Ulrich pointed out, the world of unification with occurs-check
combines poorly with the world of cyclic terms. This was the main
conclusion from a debate whether A=f(A), unify_with_occurs_check(A,_)
should succeed or fail.
Just making part of the code emit safe unification instructions is a
neat idea, but will only make sense if the control-flow can guarantee
that the terms entering this code are cycle-free and that the safe
code does not call unsafe code somewhere. That requires much than
simply emitting different unification instructions.
Cheers --- Jan
Jan Burse
> combines poorly with the world of cyclic terms. This was the main
> conclusion from a debate whether A=f(A), unify_with_occurs_check(A,_)
> should succeed or fail.
> That requires much than simply emitting different
> unification instructions.
In a first round, the burden would be on the
end-user to guarantee that his mix and match
does work.
The problem is that when you have the occurs
check off and no cyclic terms, your Prolog
system is anyway not safe in the first place.
I probably don't need to give you examples,
but here is one:
?- X=f(X), Y=f(Y), X=Y.
I guess it will hang in 75% of the Prolog
systems, or is it 95%?
Something else: In the above example, the
Prolog system might infinitely hang, even not
throwing a stack overflow error or some heap
overflow, when unification is implemented with
tail recursion.
Any Prolog system still reacting on signals or
somesuch? Is it possible to interrupt the current
thread? I guess killing is always possible, right?
Bye
Jan Wielemaker
>> As Ulrich pointed out, the world of unification with occurs-check
>> combines poorly with the world of cyclic terms. This was the main
>> conclusion from a debate whether A=f(A), unify_with_occurs_check(A,_)
>> should succeed or fail.
>
> Yes, remember something.
>
>> That requires much than simply emitting different
> > unification instructions.
>
> Agreed!
>
> In a first round, the burden would be on the
> end-user to guarantee that his mix and match
> does work.
That smells a lot as trying to mix type-checked and non-type-checked
code as Tom did in his demo type-checker. Complicated stuff and I'd
rather do something with typing :-)
> The problem is that when you have the occurs
> check off and no cyclic terms, your Prolog
> system is anyway not safe in the first place.
>
> I probably don't need to give you examples,
> but here is one:
>
> ?- X=f(X), Y=f(Y), X=Y.
>
> I guess it will hang in 75% of the Prolog
> systems, or is it 95%?
I may hope not. On this example, hanging or crashing systems are ISO
compliant, but I sincerely hope we left this era behind us.
Cheers --- Jan
Jan Burse
> I may hope not. On this example, hanging or crashing systems are ISO
> compliant, but I sincerely hope we left this era behind us.
>
> Cheers --- Jan
Goody, goody. Made a little test, running Prolog systems
in default mode (so not explicitly fidling with the occurs
check flag):
?- X=f(X), Y=f(Y), X=Y.
SWI: Succeeds
SICStus: Succeeds
YAP: Succeeds
GNU: Hangs, reacts on ^C
B-Prolog: Hangs, does not react on ^C
Ciao: Memory allocation failed
50% in new era?
All 3 prologs that succeed show the resulting
cyclic terms in a different way...
Bye
Ulrich Neumerkel
>Jan Wielemaker schrieb:
>> SWI-Prolog after
>>
>> set_prolog_flag(occurs_check, true).
>
>Something else: I was thinking of a compile time
>based occurs_check on/off thing, because it could be
>applied selectively to code.
Eclipse-Prolog did this. But they removed this recently,
since version 6.
It seems that managing such differences can be very tricky
in larger systems.
Ulrich Neumerkel
>Jan Wielemaker schrieb:
>> As Ulrich pointed out, the world of unification with occurs-check
>> combines poorly with the world of cyclic terms. This was the main
>> conclusion from a debate whether A=f(A), unify_with_occurs_check(A,_)
>> should succeed or fail.
But in the meantime since 2011-04 or so SWI has a very nice and new
definition failing only for "new cycles". There are some cases still
awaiting perfection, but its seems really the best way to go.
...
>I probably don't need to give you examples,
>but here is one:
>
> ?- X=f(X), Y=f(Y), X=Y.
>
>I guess it will hang in 75% of the Prolog
>systems, or is it 95%?
Lets look at X=f(X), Y=f(Y), X\=Y. instead, to avoid
issues with printing the answer.
IF, SWI, YAP, SICStus, Ciao, Eclipse all fail finitely
B, GNU, XSB loop
bart demoen
> Lets look at X=f(X), Y=f(Y), X\=Y. instead, to avoid issues with
> printing the answer.
>
> IF, SWI, YAP, SICStus, Ciao, Eclipse all fail finitely
And so does hProlog (also for the original query), again lowering the
% of systems not dealing with it :-)
There is a difference (as Ulrich knows of course) between
unification supports cyclic terms
and
every builtin supports cyclic terms
Lots of systems (perhaps all) are somewhere in between those two.
Cheers
Bart Demoen
--- Posted via news://freenews.netfront.net/ - Complaints to ne...@netfront.net ---