2.3 Avoiding Unnecessary OCCUR Checks
It is possible to significantly reduce the number
of calls to OCCUR during a resolution unification
by the following observation. If two clauses are
being resolved, they are standardized apart.
Thus, a variable from the left-hand parent will not
occur in a term from the right-hand parent unless
during this unification, there has been a binding of a
variable from the right to a term from the left.
A similar statement holds for 1eft-to-right bindings.
Once again, in structure sharing, this condition
is easy to check.
Hi,
J Strother Moore II is the Original Gangster (OG)
of program sharng. Interestingly structure sharing
meant always program sharing in the theorem
proving community back then:
COMPUTATIONAL LOGIC: STRUCTURE SHARING AND
PROOF OF PROGRAM PROPERTIES
J Strother Moore II - 1973 https://era.ed.ac.uk/bitstream/handle/1842/2245/Moore-Thesis-1973-OCR.pdf
Only the WAM community managed to intsitutionalize
the term structure sharng, as a reduced form of
program sharing, namely goal argument sharing
not using pairs of two pointers with skeleton and binding
environment anymore, to indentify a Prolog term,
but simple single pointers for a Prolog term.
Bye
Hi,
J Strother Moore II is the Original Gangster (OG)
of program sharng. Interestingly structure sharing
meant always program sharing in the theorem
proving community back then:
COMPUTATIONAL LOGIC: STRUCTURE SHARING AND
PROOF OF PROGRAM PROPERTIES
J Strother Moore II - 1973 https://era.ed.ac.uk/bitstream/handle/1842/2245/Moore-Thesis-1973-OCR.pdf
Only the WAM community managed to intsitutionalize
the term structure sharng, as a reduced form of
program sharing, namely goal argument sharing
not using pairs of two pointers with skeleton and binding
environment anymore, to indentify a Prolog term,
but simple single pointers for a Prolog term.
Bye
Hi,
Frozen Prolog terms don’t need to be traversed to know
whether they are ground. They have a GC mask information
that shows that they are program shared (PS) ground Prolog
terms, so that copy can immediately return. One can modify
the testing slightly, going from this here in frozen.pl:
test(N) :- between(1,1000,_), data(N,_), fail.
test(_).
test2(N) :- between(1,1000,_), test(N), fail.
test2(_).
To this here, unfortunately copy_term/2 not available in WebPL:
test(X) :- between(1,1000,_), copy_term(X,_), fail.
test(_).
test2(N) :- data(N,X), between(1,1000,_), test(X), fail.
test2(_).
So basically departing from testing whether a first access
to a program sharing structure is fast, into testing
whether copy_term/2 has some smarts to detect
program sharing structures.
Bye
Mild Shock schrieb:
Hi,
J Strother Moore II is the Original Gangster (OG)
of program sharng. Interestingly structure sharing
meant always program sharing in the theorem
proving community back then:
COMPUTATIONAL LOGIC: STRUCTURE SHARING AND
PROOF OF PROGRAM PROPERTIES
J Strother Moore II - 1973
https://era.ed.ac.uk/bitstream/handle/1842/2245/Moore-Thesis-1973-OCR.pdf
Only the WAM community managed to intsitutionalize
the term structure sharng, as a reduced form of
program sharing, namely goal argument sharing
not using pairs of two pointers with skeleton and binding
environment anymore, to indentify a Prolog term,
but simple single pointers for a Prolog term.
Bye
Hi,
I get for SWI-Prolog WASM, that copy is faster
than knowledge base fact access:
/* SWI-Prolog WASM, copy_term/2 testing */
?- test2(10).
(645.4ms)
?- test2(30).
(1056.5ms)
?- test2(90).
(2245.2ms)
For example copying the 90 element list takes
only 2245.2ms while acccessing the 90 element
list from facts takes 5372.3ms, see previous post.
But the copy_term/2 is nevertheless linear.
Bye
Mild Shock schrieb:
Hi,
Frozen Prolog terms don’t need to be traversed to know
whether they are ground. They have a GC mask information
that shows that they are program shared (PS) ground Prolog
terms, so that copy can immediately return. One can modify
the testing slightly, going from this here in frozen.pl:
test(N) :- between(1,1000,_), data(N,_), fail.
test(_).
test2(N) :- between(1,1000,_), test(N), fail.
test2(_).
To this here, unfortunately copy_term/2 not available in WebPL:
test(X) :- between(1,1000,_), copy_term(X,_), fail.
test(_).
test2(N) :- data(N,X), between(1,1000,_), test(X), fail.
test2(_).
So basically departing from testing whether a first access
to a program sharing structure is fast, into testing
whether copy_term/2 has some smarts to detect
program sharing structures.
Bye
Mild Shock schrieb:
Hi,
J Strother Moore II is the Original Gangster (OG)
of program sharng. Interestingly structure sharing
meant always program sharing in the theorem
proving community back then:
COMPUTATIONAL LOGIC: STRUCTURE SHARING AND
PROOF OF PROGRAM PROPERTIES
J Strother Moore II - 1973
https://era.ed.ac.uk/bitstream/handle/1842/2245/Moore-Thesis-1973-OCR.pdf >>>
Only the WAM community managed to intsitutionalize
the term structure sharng, as a reduced form of
program sharing, namely goal argument sharing
not using pairs of two pointers with skeleton and binding
environment anymore, to indentify a Prolog term,
but simple single pointers for a Prolog term.
Bye
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,064 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 146:10:42 |
| Calls: | 13,691 |
| Calls today: | 1 |
| Files: | 186,935 |
| D/L today: |
21 files (1,090K bytes) |
| Messages: | 2,410,864 |