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
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: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
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...
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
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.
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
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 716 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 52:12:21 |
| Calls: | 12,115 |
| Calls today: | 6 |
| Files: | 15,010 |
| Messages: | 6,518,584 |
| Posted today: | 1 |