Hi,
bisim_equals/2 is just bisimulation. You can
also implement bisim_unify/2, extremly trivial as well.
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.
Bye
From Dogelog Player, unification that can do cyclic
terms, also extremly trivial:
% bisim_unify(+Term, +Term)
bisim_unify(X, Y) :-
sys_bisim_unify(X, Y, []).
% sys_bisim_unify(+Term, +Term, +List)
sys_bisim_unify(X, Y, _) :- primitive(X), !, X = Y.
sys_bisim_unify(X, Y, _) :- primitive(Y), !, X = Y.
sys_bisim_unify(X, Y, S) :-
member(Z-T, S),
ir_object_equals(X, Z),
ir_object_equals(Y, T), !.
sys_bisim_unify(X, Y, _) :-
functor(X, F, N),
functor(Y, G, M),
F/N \== G/M, !, fail.
sys_bisim_unify(X, Y, S) :-
X =.. [_|L],
Y =.. [_|R],
sys_bisim_unify_list(L, R, [X-Y|S]).
% sys_bisim_unify_list(+List, +List, +List)
sys_bisim_unify_list([], [], _).
sys_bisim_unify_list([X|L], [Y|R], S) :-
sys_bisim_unify(X, Y, S),
sys_bisim_unify_list(L, R, S).
Mild Shock schrieb:
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
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)