Hi,

Alain Colmerauer mentions the non-monster
instruction form here:

"By introducing intermediate variables
so that every term contains no more than
one functional symbol the check for a
greatest term is no longer necessary."
- page 236

But his haluctination of greatest term,
to archive I guess some normal form,
formalized for monster instructions,
as here in his rule:

"CONFRONTATION (CO): If x is a variable
and t1,t2 are not variables and |ti| < |t2|
then replace {x=t1,x=t2} by x=t1,t1=t2.
By |t| we denote the size oft, i.e. the number
of occurrences of elements of FuV."
- page 235

But using a greatest term is not necessary
for non-monster approach, as observed by
Alain Colmerauer himself in page 236 after

page 235, but in my opion this can be also
lifted to monster instructions, where the
equatsions are V=T, where T is not
restricted to a single function symbol.

I think Ciao Prolog uncycle_term/2 has
nowhere a term size comparision and is living
proof of my claim, that his rules are nonsense.
So mostlikely the term size has a totally

different purpose, showing the termination
of some bisimulation. But showing termination of
some bisimulation is easier with memory
adresses, since memory adresses are trivially

finite in their number, a finite set, whereas new
equation are infinitely many, an infinite set, that
could be produced, when one is not careful.

Bye

Mild Shock schrieb:

Hi,

Colmerauer 1982 writes:

The objective of this paper is to describe a
novel theoretical model of Prolog involving
infinite trees. This model corresponds to the
Prolog interpreters which do not perform the
"occur check". However, the unification
algorithm for these interpreters must be
modified so as to assure termination. The
best way to achieve this termination is an open
problem which is not discussed here.

"open" problem of that time. The Epoch/Community
change was from Graph Theory / Algorithms to
Concurrency / Process Theory. Bisimulation

is again a word not used by Colmerauer 1982, as
it was a word not used by Aho, Garey &
Ullman - 1972. But trivially unification (=)/2

for rational trees is a bisimulation problem,
the same way like syntactic equality (==)/2
for rational trees is a bisimulation problem.

But where does the compare/3 problem come from?
Well move fast forward to 1995 when the ISO
core standard was published which required

compare/3, sort/2, etc.. etc.. without
specfying a reference algorithm for compare/3
on rational trees. And so where the gates

of hell opened. Since then some exorcism
has to be applied to solutions like compare_with_stack/3,
that use bisimulation , but that do not work.

An unlearning has to be done: Hey (=)/2
and (==)/2 can be related to bisimulation,
but my skull has to digest that compare/3

cannot be implemented the same way.

Bye

Julio Di Egidio schrieb:

On 20/07/2025 19:15, Julio Di Egidio wrote:

On 20/07/2025 16:22, Julio Di Egidio wrote:

On 20/07/2025 16:15, Julio Di Egidio wrote:

On 20/07/2025 15:13, Mild Shock wrote:

;  > Let (H, <) be the standard total oder an the
;  > Prolog finite terms. Let R be the set of rational
;  > term. H c R. Then there is total order
;  > extention (R, <') of (H, <).
;
Is the problem of a compare/3 for rational trees,
that is a extension of the compare/3 for finite aka
acyclic terms with the submodel property.

Your "discourse" implicitly assumes that the
"extension" is somewhat "trivial" and/or
"natural".  Which, in turn, I'd think is the
case (can be done) only if we can *effectively*
(and, ideally, somewhat "naturally") define
*canonical form* then *normalization* of
(Prolog's) cyclic terms...

P.S.  I have not actually investigated this, but
if "normalization" is not a problem, then I do not
see what the problem is...

Normalise this: `X = f(g(f(g(X))`

Or, even simpler: `X = f(f(X))`

(I don't think it gets essentially more complicated
than that: I might be wrong, but AFAICT, we can only
construct (rooted) terms with nested cycles...)

But we are in luck, here is the whole theory:

Prolog and Infinite Trees - A Colmerauer (1982):
<https://www.softwarepreservation.org/projects/prolog/marseille/doc/Colmerauer-InfTree-1982.pdf/view>


For bonus points, there is even an open problem
that looks like the perfect job for Coq/Rocq...

Have fun,

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

Just compare the top-level of Ciao Prolog:

/* Ciao Prolog */
?- p(X,Y).
X = f(X),
Y = f(X) ? ;

X = a(f(X,b(g(X,Y)))),
Y = b(g(a(f(X,Y)),Y)) ? ;

X = s(s(X,s(Y,X)),_A),
Y = s(Y,s(s(X,Y),_A)) ? ;

https://ciao-lang.org/playground/

With Dogelog Player:

?- p(X,Y).
X = f(f(f(X))), Y = f(f(Y));
X = a(f(X, Y)), Y = b(g(X, Y));
X = s(s(X, Y), _), Y = s(Y, X).

https://www.dogelog.ch/littab/doclet/live/07_basic/example01/package.html

So I guess I a found some Gold!

LoL

Bye

P.S.: I nowhere use term size, also I don't
use non-monster instructions permanently.

The test cases are:

p(X,Y) :- X = f(f(f(X))), Y = f(f(Y)).
p(X,Y) :- X = a(f(X,Y)), Y = b(g(X,Y)).
p(X,Y) :- X = s(s(X,Y),_), Y = s(Y,X).

Mild Shock schrieb:

Hi,

Alain Colmerauer mentions the non-monster
instruction form here:

"By introducing intermediate variables
so that every term contains no more than
one functional symbol the check for a
greatest term is no longer necessary."
- page 236

But his haluctination of greatest term,
to archive I guess some normal form,
formalized for monster instructions,
as here in his rule:

"CONFRONTATION (CO): If x is a variable
and t1,t2 are not variables and |ti| < |t2|
then replace {x=t1,x=t2} by x=t1,t1=t2.
By |t| we denote the size oft, i.e. the number
of occurrences of elements of FuV."
- page 235

But using a greatest term is not necessary
for non-monster approach, as observed by
Alain Colmerauer himself in page 236 after

page 235, but in my opion this can be also
lifted to monster instructions, where the
equatsions are V=T, where T is not
restricted to a single function symbol.

I think Ciao Prolog uncycle_term/2 has
nowhere a term size comparision and is living
proof of my claim, that his rules are nonsense.
So mostlikely the term size has a totally

different purpose, showing the termination
of some bisimulation. But showing termination of
some bisimulation is easier with memory
adresses, since memory adresses are trivially

finite in their number, a finite set, whereas new
equation are infinitely many, an infinite set, that
could be produced, when one is not careful.

Bye

Mild Shock schrieb:

Hi,

Colmerauer 1982 writes:

The objective of this paper is to describe a
novel theoretical model of Prolog involving
infinite trees. This model corresponds to the
Prolog interpreters which do not perform the
"occur check". However, the unification
algorithm for these interpreters must be
modified so as to assure termination. The
best way to achieve this termination is an open
problem which is not discussed here.

"open" problem of that time. The Epoch/Community
change was from Graph Theory / Algorithms to
Concurrency / Process Theory. Bisimulation

is again a word not used by Colmerauer 1982, as
it was a word not used by Aho, Garey &
Ullman - 1972. But trivially unification (=)/2

for rational trees is a bisimulation problem,
the same way like syntactic equality (==)/2
for rational trees is a bisimulation problem.

But where does the compare/3 problem come from?
Well move fast forward to 1995 when the ISO
core standard was published which required

compare/3, sort/2, etc.. etc.. without
specfying a reference algorithm for compare/3
on rational trees. And so where the gates

of hell opened. Since then some exorcism
has to be applied to solutions like compare_with_stack/3,
that use bisimulation , but that do not work.

An unlearning has to be done: Hey (=)/2
and (==)/2 can be related to bisimulation,
but my skull has to digest that compare/3

cannot be implemented the same way.

Bye

Julio Di Egidio schrieb:

On 20/07/2025 19:15, Julio Di Egidio wrote:

On 20/07/2025 16:22, Julio Di Egidio wrote:

On 20/07/2025 16:15, Julio Di Egidio wrote:

On 20/07/2025 15:13, Mild Shock wrote:

;  > Let (H, <) be the standard total oder an the
;  > Prolog finite terms. Let R be the set of rational
;  > term. H c R. Then there is total order
;  > extention (R, <') of (H, <).
;
Is the problem of a compare/3 for rational trees,
that is a extension of the compare/3 for finite aka
acyclic terms with the submodel property.

Your "discourse" implicitly assumes that the
"extension" is somewhat "trivial" and/or
"natural".  Which, in turn, I'd think is the
case (can be done) only if we can *effectively*
(and, ideally, somewhat "naturally") define
*canonical form* then *normalization* of
(Prolog's) cyclic terms...

P.S.  I have not actually investigated this, but
if "normalization" is not a problem, then I do not
see what the problem is...

Normalise this: `X = f(g(f(g(X))`

Or, even simpler: `X = f(f(X))`

(I don't think it gets essentially more complicated
than that: I might be wrong, but AFAICT, we can only
construct (rooted) terms with nested cycles...)

But we are in luck, here is the whole theory:

Prolog and Infinite Trees - A Colmerauer (1982):
<https://www.softwarepreservation.org/projects/prolog/marseille/doc/Colmerauer-InfTree-1982.pdf/view>


For bonus points, there is even an open problem
that looks like the perfect job for Coq/Rocq...

Have fun,

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)