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.
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...
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...
-Julio
Strange this little Prolog code snippet,
that creates a polish notation with sharing
out of a Prolog term, either acyclic or cyclic,
works for me to compare terms (that do not contain ‘$VAR’/1):
polish(X, L, T) :-
sys_polish_term(X, [], H, T),
sys_strip_reverse(H, [], L).
Here the test cases from the top-level ticket:
?- p(X,Y), polish(p(X,Y),L,T).
L = [A=p(B, B), B=f(B)],
L = [A=p(B, D), B=a(C), C=f(B, D), D=b(E), E=g(B, D)],
L = [A=p(B, D), B=s(C, _A), C=s(B, D), D=s(D, B)],
The description “Polish” refers to the nationality
of logician Jan Łukasiewicz who invented Polish notation
in 1924. In the above I am more doing what is called
reverse polish notation, known from pocket calculators
such as HP-41C, the perfect toy for, boring math classes
during school. You can imagine the sharing happens
by pressing the memory store and recall keys of a HP-41C.
Defining a comparison as:
compare2(C,X,Y) :- polish(X,L,T), polish(Y,R,S),
compare(C,L-T,R-S).
Has the following properties:
- It is conservative:
For acyclic terms compare2/3 and compare/3 agree.
- It is a total order:
Because compare2/3 falls back to compare/3, and polish
is injective versus (==)/2, it has all desired properties.
https://www.hpmuseum.org/hp41.htm
Julio Di Egidio schrieb:
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...
-Julio
% polish(+Term, -List, -Term)
polish(X, L, T) :-
sys_polish_term(X, [], H, T),
sys_strip_reverse(H, [], L).
% sys_polish_term(+Term, +List, -List, -Term)
sys_polish_term(T, L, L, T) :- (var(T); atomic(T)), !.
sys_polish_term(T, L, L, V) :-
member(v(S,V,_), L),
S == T, !.
sys_polish_term(T, L, R, V) :-
length(L, N),
V = '$VAR'(N),
T =.. [F|P],
sys_polish_terms(P, [v(T,V,S)|L], R, Q),
S =.. [F|Q].
% sys_polish_terms(+List, +List, -List, -List)
sys_polish_terms([], L, L, []).
sys_polish_terms([X|P], L, R, [Y|Q]) :-
sys_polish_term(X, L, H, Y),
sys_polish_terms(P, H, R, Q).
% sys_strip_reverse(+List, +List, -List)
sys_strip_reverse([], L, L).
sys_strip_reverse([v(_,V,T)|L], R, S) :-
sys_strip_reverse(L, [V=T|R], S).
Mild Shock schrieb:
Strange this little Prolog code snippet,
that creates a polish notation with sharing
out of a Prolog term, either acyclic or cyclic,
works for me to compare terms (that do not contain ‘$VAR’/1):
polish(X, L, T) :-
sys_polish_term(X, [], H, T),
sys_strip_reverse(H, [], L).
Here the test cases from the top-level ticket:
?- p(X,Y), polish(p(X,Y),L,T).
L = [A=p(B, B), B=f(B)],
L = [A=p(B, D), B=a(C), C=f(B, D), D=b(E), E=g(B, D)],
L = [A=p(B, D), B=s(C, _A), C=s(B, D), D=s(D, B)],
The description “Polish” refers to the nationality
of logician Jan Łukasiewicz who invented Polish notation
in 1924. In the above I am more doing what is called
reverse polish notation, known from pocket calculators
such as HP-41C, the perfect toy for, boring math classes
during school. You can imagine the sharing happens
by pressing the memory store and recall keys of a HP-41C.
Defining a comparison as:
compare2(C,X,Y) :- polish(X,L,T), polish(Y,R,S),
compare(C,L-T,R-S).
Has the following properties:
- It is conservative:
For acyclic terms compare2/3 and compare/3 agree.
- It is a total order:
Because compare2/3 falls back to compare/3, and polish
is injective versus (==)/2, it has all desired properties.
https://www.hpmuseum.org/hp41.htm
Julio Di Egidio schrieb:
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...
-Julio
BTW: Its essentially the same code like
here from 2023, a little “polished”:
Cheap compare for cyclic terms [injective collation keys] https://swi-prolog.discourse.group/t/cheap-compare-for-cyclic-terms-injective-collation-keys/6427
But I have removed my old file rep2.p,
since I wanted a more didactic presentation.
Mild Shock schrieb:
% polish(+Term, -List, -Term)
polish(X, L, T) :-
sys_polish_term(X, [], H, T),
sys_strip_reverse(H, [], L).
% sys_polish_term(+Term, +List, -List, -Term)
sys_polish_term(T, L, L, T) :- (var(T); atomic(T)), !.
sys_polish_term(T, L, L, V) :-
member(v(S,V,_), L),
S == T, !.
sys_polish_term(T, L, R, V) :-
length(L, N),
V = '$VAR'(N),
T =.. [F|P],
sys_polish_terms(P, [v(T,V,S)|L], R, Q),
S =.. [F|Q].
% sys_polish_terms(+List, +List, -List, -List)
sys_polish_terms([], L, L, []).
sys_polish_terms([X|P], L, R, [Y|Q]) :-
sys_polish_term(X, L, H, Y),
sys_polish_terms(P, H, R, Q).
% sys_strip_reverse(+List, +List, -List)
sys_strip_reverse([], L, L).
sys_strip_reverse([v(_,V,T)|L], R, S) :-
sys_strip_reverse(L, [V=T|R], S).
Mild Shock schrieb:
Strange this little Prolog code snippet,
that creates a polish notation with sharing
out of a Prolog term, either acyclic or cyclic,
works for me to compare terms (that do not contain ‘$VAR’/1):
polish(X, L, T) :-
sys_polish_term(X, [], H, T),
sys_strip_reverse(H, [], L).
Here the test cases from the top-level ticket:
?- p(X,Y), polish(p(X,Y),L,T).
L = [A=p(B, B), B=f(B)],
L = [A=p(B, D), B=a(C), C=f(B, D), D=b(E), E=g(B, D)],
L = [A=p(B, D), B=s(C, _A), C=s(B, D), D=s(D, B)],
The description “Polish” refers to the nationality
of logician Jan Łukasiewicz who invented Polish notation
in 1924. In the above I am more doing what is called
reverse polish notation, known from pocket calculators
such as HP-41C, the perfect toy for, boring math classes
during school. You can imagine the sharing happens
by pressing the memory store and recall keys of a HP-41C.
Defining a comparison as:
compare2(C,X,Y) :- polish(X,L,T), polish(Y,R,S),
compare(C,L-T,R-S).
Has the following properties:
- It is conservative:
For acyclic terms compare2/3 and compare/3 agree.
- It is a total order:
Because compare2/3 falls back to compare/3, and polish
is injective versus (==)/2, it has all desired properties.
https://www.hpmuseum.org/hp41.htm
Julio Di Egidio schrieb:
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...
-Julio
Hi,
The Stargate Project is a new company which intends
to invest $500 billion over the next four years
building new AI infrastructure for OpenAI in
the United States. SoftBank having financial
responsibility and OpenAI having operational
responsibility. Masayoshi Son will be the chairman.
https://openai.com/index/announcing-the-stargate-project/
What a shame no, solution from USA or Japan
for decades? Ok, maybe my solution doesn't work
either. Don't know yet, so far I am using
my intuition. Which tells me if a polish
prefix is equivalent then the corresponding
subterm is equivalent. And where the polish
prefix diagrees for the first time, one
has found a conflict which is anyways the
typical f/n versus g/n conflict, or otherwise
different arguments used, in this case the algorithm
will make a choice based on the primtitives and
the '$VAR'/1 in the compounds. But for acyclic
terms the '$VAR'/1 values are kind of normed,
and their appearance indicates a non-primitive.
Bye
Mild Shock schrieb:
BTW: Its essentially the same code like
here from 2023, a little “polished”:
Cheap compare for cyclic terms [injective collation keys]
https://swi-prolog.discourse.group/t/cheap-compare-for-cyclic-terms-injective-collation-keys/6427
But I have removed my old file rep2.p,
since I wanted a more didactic presentation.
Mild Shock schrieb:
% polish(+Term, -List, -Term)
polish(X, L, T) :-
sys_polish_term(X, [], H, T),
sys_strip_reverse(H, [], L).
% sys_polish_term(+Term, +List, -List, -Term)
sys_polish_term(T, L, L, T) :- (var(T); atomic(T)), !.
sys_polish_term(T, L, L, V) :-
member(v(S,V,_), L),
S == T, !.
sys_polish_term(T, L, R, V) :-
length(L, N),
V = '$VAR'(N),
T =.. [F|P],
sys_polish_terms(P, [v(T,V,S)|L], R, Q),
S =.. [F|Q].
% sys_polish_terms(+List, +List, -List, -List)
sys_polish_terms([], L, L, []).
sys_polish_terms([X|P], L, R, [Y|Q]) :-
sys_polish_term(X, L, H, Y),
sys_polish_terms(P, H, R, Q).
% sys_strip_reverse(+List, +List, -List)
sys_strip_reverse([], L, L).
sys_strip_reverse([v(_,V,T)|L], R, S) :-
sys_strip_reverse(L, [V=T|R], S).
Mild Shock schrieb:
Strange this little Prolog code snippet,
that creates a polish notation with sharing
out of a Prolog term, either acyclic or cyclic,
works for me to compare terms (that do not contain ‘$VAR’/1):
polish(X, L, T) :-
sys_polish_term(X, [], H, T),
sys_strip_reverse(H, [], L).
Here the test cases from the top-level ticket:
?- p(X,Y), polish(p(X,Y),L,T).
L = [A=p(B, B), B=f(B)],
L = [A=p(B, D), B=a(C), C=f(B, D), D=b(E), E=g(B, D)],
L = [A=p(B, D), B=s(C, _A), C=s(B, D), D=s(D, B)],
The description “Polish” refers to the nationality
of logician Jan Łukasiewicz who invented Polish notation
in 1924. In the above I am more doing what is called
reverse polish notation, known from pocket calculators
such as HP-41C, the perfect toy for, boring math classes
during school. You can imagine the sharing happens
by pressing the memory store and recall keys of a HP-41C.
Defining a comparison as:
compare2(C,X,Y) :- polish(X,L,T), polish(Y,R,S),
compare(C,L-T,R-S).
Has the following properties:
- It is conservative:
For acyclic terms compare2/3 and compare/3 agree.
- It is a total order:
Because compare2/3 falls back to compare/3, and polish
is injective versus (==)/2, it has all desired properties.
https://www.hpmuseum.org/hp41.htm
Julio Di Egidio schrieb:
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...
-Julio
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...
-Julio
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...
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...)
-Julio
compare/2 doesn't cover only (==)/2.
It also covers (@<)/2 and (@>)/2.
Julio Di Egidio schrieb:
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...)
-Julio
Hi,
Reverse Polish Notation has nice Stack Machine Proofs.
You could finally show some muscles, and use Coq or
Rocq for a good deed. I suspect there is the following
lemma now, for a Reverse Polish Notation string:
Let P1 and P2 be two strings:
P1 = Prefix1 Suffix1
P2 = Prefix2 Suffix2
If Prefix1 = Prefix2 then the evaluation P1 up
respectively P2 to the length |Prefix1| = |Prefix2|
has a stack result of the form:
[Value1, .., Valuen]
With identical values for both P1 and P2. Question is
iwhat happens with the first instruction of Suffix1
respectively Suffix2, can we use it for compare/3.
I have now changed what I originally wrote to:
- Open question whether it is conservative:
I have mixed feelings whether it is conservative,
i.e. whether compare2/3 and compare/3 agree on acyclic terms.
Mostlikely not. You can mittigate the problem, by
creating monster instructions inside the P1 and P2.
And then I guess the above proposition holds.
I am currently creating monster instructions during
printing, but was completely busy with printing, didn't
really look yet into comparison and especially having
a cheap way of conservativity.
Bye
Julio Di Egidio schrieb:
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...
-Julio
From Dogelog Player:
% bisim_equals(+Term, +Term)
bisim_equals(X, Y) :-
sys_bisim_equals(X, Y, []).
% sys_bisim_equals(+Term, +Term, +List)
sys_bisim_equals(X, Y, _) :- primitive(X), !, X == Y.
sys_bisim_equals(X, Y, _) :- primitive(Y), !, X == Y.
sys_bisim_equals(X, Y, S) :-
member(Z-T, S),
ir_object_equals(X, Z),
ir_object_equals(Y, T), !.
sys_bisim_equals(X, Y, _) :-
functor(X, F, N),
functor(Y, G, M),
F/N \== G/M, !, fail.
sys_bisim_equals(X, Y, S) :-
X =.. [_|L],
Y =.. [_|R],
sys_bisim_equals_list(L, R, [X-Y|S]).
% sys_bisim_equals_list(+List, +List, +List)
sys_bisim_equals_list([], [], _).
sys_bisim_equals_list([X|L], [Y|R], S) :-
sys_bisim_equals(X, Y, S),
sys_bisim_equals_list(L, R, S).
Mild Shock schrieb:
compare/2 doesn't cover only (==)/2.
It also covers (@<)/2 and (@>)/2.
Julio Di Egidio schrieb:
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...)
-Julio
compare/2 doesn't cover only (==)/2.
It also covers (@<)/2 and (@>)/2.
But all attempts to translate the idea to
compare_with_stack/3 have failed so far. SWI
Prolog discourse is full of failed attempts,
and missing insights as well, why it fails.
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 on
But all attempts to translate the idea to
compare_with_stack/3 have failed so far. SWI
Prolog discourse is full of failed attempts,
and missing insights as well, why it fails.
On 20/07/2025 19:46, Mild Shock wrote:
compare/2 doesn't cover only (==)/2.
It also covers (@<)/2 and (@>)/2.
Which must be the reason you keep posting code,
and inscrutable one at that, on bisimulation...
you complete asshole.
But all attempts to translate the idea to
compare_with_stack/3 have failed so far. SWI
Prolog discourse is full of failed attempts,
and missing insights as well, why it fails.
Don't underestimate your own contribution...
*Plonk*
-Julio
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...)
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.
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
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
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
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,064 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 152:49:16 |
| Calls: | 13,691 |
| Calls today: | 1 |
| Files: | 186,936 |
| D/L today: |
2,525 files (731M bytes) |
| Messages: | 2,411,051 |