Meanwhile I am going back to my tinkering with my
Prolog system, which even provides a more primitive
logic than minimal logic, pure Prolog is minimal
logic without embedded implication.
On 7/9/2024 10:14 AM, olcott wrote:
On 7/9/2024 4:04 AM, Mild Shock wrote:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
I initially thought that you would agree with me
about Prolog and not dismiss what I said out-of-hand
without review.
On 7/9/2024 11:12 AM, Mild Shock wrote:
Fuck off asshole. Prolog is irrelevant for
the minimal logic posts. I only made this
joke, but it has nothing to do with occurs check:
Meanwhile I am going back to my tinkering with my
Prolog system, which even provides a more primitive
logic than minimal logic, pure Prolog is minimal
;
logic without embedded implication.
You even don't know what the occurs check is,
and for what it is used.
It detects cycles in the directed graph of the expression's
evaluation sequence as a paraphrase of Clocksin & Mellish indicates.
If the occurs check is used, then
olcott schrieb:
On 7/9/2024 10:14 AM, olcott wrote:
On 7/9/2024 4:04 AM, Mild Shock wrote:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
I initially thought that you would agree with me
about Prolog and not dismiss what I said out-of-hand
without review.
It detects cycles in the directed graph of the expression's
evaluation sequence as a paraphrase of Clocksin & Mellish indicates.
In unification with occurs check cycles in a graph
are prevented before they happen. You are such a moron.
The "occurs check" does that. It checks V ∈ T, BEFORE
a variable V gets instantiated to T.
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.
Instead it is usually implemented as follows,
Just consult Rihcard O'Keefes File METUTL.PL :
% unify(?X, ?Y)
% Try to unify X and Y, wih occurs check.
% Further down in this file is the Occurs Check.
unify(X, Y) :-
var(X),
var(Y),
!,
X = Y. % want unify(X,X)
unify(X, Y) :-
var(X),
!,
occurs_check(Y, X), % X is not in Y
X = Y.
unify(X, Y) :-
var(Y),
!,
occurs_check(X, Y), % Y is not in X
X = Y.
unify(X, Y) :-
atomic(X),
!,
X = Y.
unify(X, Y) :-
functor(X, F, N),
functor(Y, F, N),
unify(N, X, Y).
unify(0, _, _) :- !.
unify(N, X, Y) :-
arg(N, X, Xn),
arg(N, Y, Yn),
unify(Xn, Yn),
M is N-1,
!,
unify(M, X, Y).
occurs_check(Term, Var) :-
var(Term),
!,
Term \== Var.
occurs_check(Term, Var) :-
functor(Term, _, Arity),
occurs_check(Arity, Term, Var).
occurs_check(0, _, _) :- !.
occurs_check(N, Term, Var) :-
arg(N, Term, Arg),
occurs_check(Arg, Var),
M is N-1,
!,
occurs_check(M, Term, Var).
http://www.picat-lang.org/bprolog/publib/metutl.html
Bye
olcott schrieb:
On 7/9/2024 11:12 AM, Mild Shock wrote:
Fuck off asshole. Prolog is irrelevant for
the minimal logic posts. I only made this
joke, but it has nothing to do with occurs check:
Meanwhile I am going back to my tinkering with my
Prolog system, which even provides a more primitive
logic than minimal logic, pure Prolog is minimal
;
logic without embedded implication.
You even don't know what the occurs check is,
and for what it is used.
It detects cycles in the directed graph of the expression's
evaluation sequence as a paraphrase of Clocksin & Mellish indicates.
If the occurs check is used, then
olcott schrieb:
On 7/9/2024 10:14 AM, olcott wrote:
On 7/9/2024 4:04 AM, Mild Shock wrote:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
I initially thought that you would agree with me
about Prolog and not dismiss what I said out-of-hand
without review.
Only a complete nut head can write nonsense like:
It detects cycles in the directed graph of the expression's
evaluation sequence as a paraphrase of Clocksin & Mellish indicates.
You can try yourself and see that it is a "prevent"
and not a "detect" of cyclic terms. Just go online,
and you will find:
Example 02: Website Sandbox https://www.xlog.ch/runtab/doclet/docs/04_tutor/reference/example02/package.html
And now you can try unify_with_occurs_check/2,
it will never allow a cyclic structure in memory,
if the two arguments are already acyclic,
so it does a "prevent" and not a "detect":
/* Import Richard O'Keefes METUTL */
:- ensure_loaded(library(compat)).
/* Will not detect something but prevent something */
?- unify_with_occurs_check(X, [f|X]).
fail.
On the other hand the predicate acyclic_term/1 is made to
detect something, but and doesn't prevent something.
You can try in the Website Sandbox:
/* Will not prevent something but detect something */
?- X = [f|X], \+ acyclic_term(X).
X = <cyclic term> .
Also to the best of my knowledge its not possible
to bootstrap detect from prevention. So there is
no way to define:
/* not possible derive detect from prevent */
acyclic_term(X) :-
...
/* make use of unify_with_occurs_check/2 */
...
Mild Shock schrieb:
In unification with occurs check cycles in a graph
are prevented before they happen. You are such a moron.
The "occurs check" does that. It checks V ∈ T, BEFORE
a variable V gets instantiated to T.
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.
Instead it is usually implemented as follows,
Just consult Rihcard O'Keefes File METUTL.PL :
% unify(?X, ?Y)
% Try to unify X and Y, wih occurs check.
% Further down in this file is the Occurs Check.
unify(X, Y) :-
var(X),
var(Y),
!,
X = Y. % want unify(X,X)
unify(X, Y) :-
var(X),
!,
occurs_check(Y, X), % X is not in Y
X = Y.
unify(X, Y) :-
var(Y),
!,
occurs_check(X, Y), % Y is not in X
X = Y.
unify(X, Y) :-
atomic(X),
!,
X = Y.
unify(X, Y) :-
functor(X, F, N),
functor(Y, F, N),
unify(N, X, Y).
unify(0, _, _) :- !.
unify(N, X, Y) :-
arg(N, X, Xn),
arg(N, Y, Yn),
unify(Xn, Yn),
M is N-1,
!,
unify(M, X, Y).
occurs_check(Term, Var) :-
var(Term),
!,
Term \== Var.
occurs_check(Term, Var) :-
functor(Term, _, Arity),
occurs_check(Arity, Term, Var).
occurs_check(0, _, _) :- !.
occurs_check(N, Term, Var) :-
arg(N, Term, Arg),
occurs_check(Arg, Var),
M is N-1,
!,
occurs_check(M, Term, Var).
http://www.picat-lang.org/bprolog/publib/metutl.html
Bye
olcott schrieb:
On 7/9/2024 11:12 AM, Mild Shock wrote:
Fuck off asshole. Prolog is irrelevant for
the minimal logic posts. I only made this
joke, but it has nothing to do with occurs check:
Meanwhile I am going back to my tinkering with my
Prolog system, which even provides a more primitive
logic than minimal logic, pure Prolog is minimal
;
logic without embedded implication.
You even don't know what the occurs check is,
and for what it is used.
It detects cycles in the directed graph of the expression's
evaluation sequence as a paraphrase of Clocksin & Mellish indicates.
If the occurs check is used, then
olcott schrieb:
On 7/9/2024 10:14 AM, olcott wrote:
On 7/9/2024 4:04 AM, Mild Shock wrote:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
I initially thought that you would agree with me
about Prolog and not dismiss what I said out-of-hand
without review.
Yet C&M say that this test is only performed when run
thus almost never performed because it is too expensive.
On 7/9/2024 2:30 PM, Mild Shock wrote:
You can define unify_with_occurs_check/2 in terms
of MGU Θ it finds. The definition is such that for
two acyclic terms X and Y, it finds an MGU Θ such that:
- 1. It equals the two terms X Θ = Y Θ
- 2. It is most general
- 3. The new instance X Θ is acyclic
So in the end never a cyclic graph is created in
memory. To have a cyclic graph in memory a
variable V with V ∈ T would need to be instantiated
If you didn't top post then context could be more accurate.
By top posting I am only responding to the gist of what
you said and not your exact words.
to T. This would be the edge in the graph that
participates in a cycle. But such an edge is never
created in memory when you use unify_with_occurs_check/2.
The occurs check "prevents" that, it doesn't detect that.
Mild Shock schrieb:
Only a complete nut head can write nonsense like:
You can try yourself and see that it is a "prevent"It detects cycles in the directed graph of the expression's
evaluation sequence as a paraphrase of Clocksin & Mellish indicates. >>>
and not a "detect" of cyclic terms. Just go online,
and you will find:
Example 02: Website Sandbox
https://www.xlog.ch/runtab/doclet/docs/04_tutor/reference/example02/package.html
And now you can try unify_with_occurs_check/2,
it will never allow a cyclic structure in memory,
if the two arguments are already acyclic,
so it does a "prevent" and not a "detect":
/* Import Richard O'Keefes METUTL */
:- ensure_loaded(library(compat)).
/* Will not detect something but prevent something */
?- unify_with_occurs_check(X, [f|X]).
fail.
On the other hand the predicate acyclic_term/1 is made to
detect something, but and doesn't prevent something.
You can try in the Website Sandbox:
/* Will not prevent something but detect something */
?- X = [f|X], \+ acyclic_term(X).
X = <cyclic term> .
Also to the best of my knowledge its not possible
to bootstrap detect from prevention. So there is
no way to define:
/* not possible derive detect from prevent */
acyclic_term(X) :-
...
/* make use of unify_with_occurs_check/2 */
...
Mild Shock schrieb:
In unification with occurs check cycles in a graph
are prevented before they happen. You are such a moron.
The "occurs check" does that. It checks V ∈ T, BEFORE
a variable V gets instantiated to T.
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.
Instead it is usually implemented as follows,
Just consult Rihcard O'Keefes File METUTL.PL :
% unify(?X, ?Y)
% Try to unify X and Y, wih occurs check.
% Further down in this file is the Occurs Check.
unify(X, Y) :-
var(X),
var(Y),
!,
X = Y. % want unify(X,X)
unify(X, Y) :-
var(X),
!,
occurs_check(Y, X), % X is not in Y
X = Y.
unify(X, Y) :-
var(Y),
!,
occurs_check(X, Y), % Y is not in X
X = Y.
unify(X, Y) :-
atomic(X),
!,
X = Y.
unify(X, Y) :-
functor(X, F, N),
functor(Y, F, N),
unify(N, X, Y).
unify(0, _, _) :- !.
unify(N, X, Y) :-
arg(N, X, Xn),
arg(N, Y, Yn),
unify(Xn, Yn),
M is N-1,
!,
unify(M, X, Y).
occurs_check(Term, Var) :-
var(Term),
!,
Term \== Var.
occurs_check(Term, Var) :-
functor(Term, _, Arity),
occurs_check(Arity, Term, Var).
occurs_check(0, _, _) :- !.
occurs_check(N, Term, Var) :-
arg(N, Term, Arg),
occurs_check(Arg, Var),
M is N-1,
!,
occurs_check(M, Term, Var).
http://www.picat-lang.org/bprolog/publib/metutl.html
Bye
olcott schrieb:
On 7/9/2024 11:12 AM, Mild Shock wrote:
Fuck off asshole. Prolog is irrelevant for
the minimal logic posts. I only made this
joke, but it has nothing to do with occurs check:
Meanwhile I am going back to my tinkering with my
Prolog system, which even provides a more primitive
logic than minimal logic, pure Prolog is minimal
;
logic without embedded implication.
You even don't know what the occurs check is,
and for what it is used.
It detects cycles in the directed graph of the expression's
evaluation sequence as a paraphrase of Clocksin & Mellish indicates. >>>>>
If the occurs check is used, then
olcott schrieb:
On 7/9/2024 10:14 AM, olcott wrote:
On 7/9/2024 4:04 AM, Mild Shock wrote:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
I initially thought that you would agree with me
about Prolog and not dismiss what I said out-of-hand
without review.
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
According to the formal definition of Unification,
this kind of "infinite term" should never come to exist.
Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly
as Resolution theorem provers.
Hi,
Pete Olcott is full of bullshit. He writes
nonsense like for example:
"According to the formal definition of Unification, this
kind of “infinite term” should never come to exist" https://philarchive.org/archive/OLCPDPv4
Thats not true. There are different formal definitions
of Unification. There is Unification with and without
occurs check.
There are algorithms that can make Unification without
occurs check terminate, and such an algorithm is
for example implemented in SWI-Prolog.
They were pioneered by Alain Colmerauer himself, the
co-inventor of Prolog, who even wrote a paper about
the subject:
PROLOG AND INFINITE TREES
Alain Colmerauer - 1982
Universite Aix-Marseille https://www.softwarepreservation.org/projects/prolog/marseille/doc/Colmerauer-InfTree-1982.pdf
Bye
Mild Shock schrieb:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
Hi,
Here you see SWI-Prolog deal with cyclic terms:
/* SWI-Prolog 9.3.2 */
?- X = [f,f|X], Y = [f|Y], X = Y.
X = Y, Y = [f|Y].
Clocksin & Mellish refer to the formal
definition of Unification in Resolution Theorem
proving, and not in Prolog. They write:
According to the formal definition of Unification,
this kind of "infinite term" should never come to exist.
Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly
as Resolution theorem provers.
Thats from page 254 of this Clocksin and Mellish:
Programming in Prolog - Using the ISO Standard
Fifth Edition - See PDF page 268
Clocksin & Mellish - 2003 https://athena.ecs.csus.edu/~mei/logicp/Programming_in_Prolog.pdf
Bye
Mild Shock schrieb:
Hi,
Pete Olcott is full of bullshit. He writes
nonsense like for example:
"According to the formal definition of Unification, this
kind of “infinite term” should never come to exist"
https://philarchive.org/archive/OLCPDPv4
Thats not true. There are different formal definitions
of Unification. There is Unification with and without
occurs check.
There are algorithms that can make Unification without
occurs check terminate, and such an algorithm is
for example implemented in SWI-Prolog.
They were pioneered by Alain Colmerauer himself, the
co-inventor of Prolog, who even wrote a paper about
the subject:
PROLOG AND INFINITE TREES
Alain Colmerauer - 1982
Universite Aix-Marseille
https://www.softwarepreservation.org/projects/prolog/marseille/doc/Colmerauer-InfTree-1982.pdf
Bye
Mild Shock schrieb:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
On 7/10/2024 3:55 AM, Mikko wrote:
On 2024-07-09 09:04:42 +0000, Mild Shock said:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
Is interference with communication or something similar a crime where
Olcott lives?
He doesn't like the way that I hi-jacked his thread.
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
He doesn't like the way that I hi-jacked his thread.
I could have renamed it after I took it over, next time
Fucking asshole Pete Olcott, 11.07.2024, 16:57
spamming minimal logic again?
Mild Shock schrieb:
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 487 |
| Nodes: | 16 (0 / 16) |
| Uptime: | 151:17:00 |
| Calls: | 9,660 |
| Calls today: | 2 |
| Files: | 13,709 |
| Messages: | 6,166,110 |