I have found an interesting application of when/2
to compute the maximum bisimulation (congruence, better naming I think for Prolog) by method using matrix for putting x on conflicting pairs as far as possible, finally the complement is the bisimulation. It was pleasant to see it works. However, it was strange that using when/2 as in the source “NOT Work” below caused error. However, a trivial change of using when/2 as source “NORMAL” below make it work normal. Now that I recognized when/2 is really useful for elegance of programming, I wish to fix this mystery. Thanks in advance.
% ?- X = f(f(X, Y), Y), Y= f(Y, f(f(X, Y), X)),
% prepare_compare_rat([X, Y], _, Vec),
% bisim_pairs(Vec, Bisim), writeln(Bisim).
%@ [1-2,1-3,1-4,1-5,2-3,2-4,2-5,3-4,3-5,4-5]
%@ X = Y, Y = _S1, % where
%@ _S1 = f(_S1, f(f(_S2, _S1), _S2)),
%@ _S2 = f(f(_S2, _S1), _S1),
%@ Vec = v(f(5, 3), f(1, 5), f(3, 2), f(5, 3), f(4, 3)),
%@ Bisim = [1-2, 1-3, 1-4, 1-5, 2-3, 2-4, 2-5, 3-4, ... - ...|...].
bisim_pairs(FlatTermVector, BisimPairs):-
make_constraint_matrix(FlatTermVector, Matrix),
collect_bisim_pair(FlatTermVector, Matrix, BisimPairs).
%
collect_bisim_pair(V, M, Ps):-
functor(V, _, N),
findall(I-J, ( between(1, N, I),
I0 is I + 1,
between(I0, N, J),
get_matrix_elem(M,I,J,E),
var(E)
),
Ps).
%
Pulling out when(G, U = 1), the codes works normally.
Error log
% ?- X=f(X, Y), Y = f(Y, X),
% prepare_compare_rat([X, Y], _, V),
% bisim_pairs(V, Ps).
%@ ERROR: Unknown procedure: compstack:wnen/2
%@ ERROR: However, there are definitions for:
%@ ERROR: compstack:wnen0/2
%@ ERROR:
%@ ERROR: In:
%@ ERROR: [18] compstack:wnen((nonvar(_442);nonvar(_446)),_450=1)
%@ ERROR: [17] compstack:put_constraint_on_elem(f(1,2),f(1,2),_486,a(b(_510,_512),b(_516,_518))) at /Users/cantor/devel/zdd/prolog/util/compare-with-stack.pl:73
%@ ERROR: [16] compstack:conflict_constraint_rows([1,2],1,v(f(1,2),f(2,1)),a(b(_594,_596),b(_600,_602))) at /Users/cantor/devel/zdd/prolog/util/compare-with-stack.pl:61
%@ ERROR: [15] compstack:conflict_constraint_matrix([1,2],[1,2],v(f(1,2),f(2,1)),a(b(_690,_692),b(_696,_698))) at /Users/cantor/devel/zdd/prolog/util/compare-with-stack.pl:56
%@ ERROR: [13] compstack:bisim_pairs(v(f(1,2),f(2,1)),_730) at /Users/cantor/devel/zdd/prolog/util/compare-with-stack.pl:24
%@ ERROR: [11] toplevel_call('<garbage_collected>') at /Users/cantor/lib/swipl/boot/toplevel.pl:1522
%@ ERROR:
%@ ERROR: Note: some frames are missing due to last-call optimization.
%@ ERROR: Re-run your program in debug mode (:- debug.) to get more detail.
%@ Exception: (18) compstack:wnen((nonvar(_254);nonvar(_266)), _254=1) ? Unknown option (h for help)
%@ Exception: (18) compstack:wnen((nonvar(_254);nonvar(_266)), _254=1) ? Unknown option (h for help)
%@ Exception: (18) compstack:wnen((nonvar(_254);nonvar(_266)), _254=1) ? Unknown option (h for help)
%@ Exception: (18) compstack:wnen((nonvar(_254);nonvar(_266)), _254=1) ? creep
Source NOT work
put_constraint_on_elem(A, B, U, _):-
\+ ( compound(A), compound(B)), !,
( A \== B -> U = 1
; true
).
put_constraint_on_elem(A, B, U, M):-
( compare_arity(C, A, B), C\== (=) -> U=1
; A=..[_|Is],
B=..[_|Js],
maplist(get_matrix_elem(M), Is, Js, Ks),
wrap_nonvar(Ks, G),
wnen(G, U = 1)
).
Normal
put_constraint_on_elem(A, B, U, _):-
\+ ( compound(A), compound(B)), !,
( A \== B -> U = 1
; true
).
put_constraint_on_elem(A, B, U, M):-
( compare_arity(C, A, B), C\== (=) -> U=1
; A=..[_|Is],
B=..[_|Js],
maplist(get_matrix_elem(M), Is, Js, Ks),
wrap_nonvar(Ks, G),
wnen0(G, U = 1)
).
when0(A, B):- when(A, B).
