Structurally equivalent (=@=) and numbervars/1

This is sample code created as a reference when using =@=/2 and numbervars/1 to solve structural relationship problems. This is not a tour de force of the subject but just some simple examples to be used for reference.

A simple way to think of structural problems is to think of the data structure as an abstract syntax tree (AST) (use write_canonical/1 to visualize) with the branches being the structure and the leaves being the values. For these problems all of the leaves are variables. Also list, E.g. [a,b,c], are such data structures which use syntactic sugar for the linear representation but internally are a tree structure (use write_term/2 with dotlists(true) option).

One of hidden gems of SWI-Prolog is =@=/2.

=@=/2 can be used to check if graphs (vertices and edges) are structurally equivalent. With graphs one often encounters the expression, up to isomorphism, meaning that there are sets of graphs that are isomorphic and only one of the graphs from the set will suffice for the purpose needed (think algorithm testing or writing proofs).

Now for simple graphs with a few edges the number of isomorphic graphs is none to small but for graphs with even several edges the number of isomorphic graphs grows large rather quickly. So if the set of isomorphic graphs is 40 then one only needs to use one of the 40 for the needed purpose.

Much further below is the example code. Before reading the code there are a few ideas that need to be understood, especially if one is not use to programming in Prolog, thinking in terms of structures only with unbound variables, and/or thinking of variables as containers and not caring what is in the container.

The first idea is that unique variables can be generated with length/2, E.g.

?- length(Vars,3).
Vars = [_, _, _].

I know, you are thinking the variables are not unique, ahh but they are internally, the means by which they are displayed is obfuscating the needed detail, format/2 comes to the recuse but latter we will see a better way.

?- length(Vars,3),format('~w~n',[Vars]).
[_22718,_22724,_22730]
Vars = [_, _, _].

The second idea is that of structural equality, see: Predicate =@=/2 examples.

In the sample code below graphs are used with a graph being represented as list of edges and an edge is constructed with e/2. The graphs are undirected not labeled and not rooted.

So any single edge is structurally equivalent.

?- length(Vars,2),
   nth1(1,Vars,X1),nth1(2,Vars,X2),  
   e(X1,X2) =@= e(X2,X1).
Vars = [X1, X2].

But two related edges may be structurally equivalent

?- length(Vars,4),
   nth1(1,Vars,X1),nth1(2,Vars,X2),nth1(3,Vars,X3),nth1(4,Vars,X4),  
   [e(X1,X2),e(X1,X3)] =@= [e(X3,X1),e(X3,X4)].
Vars = [X1, X2, X3, X4].

or not

?- length(Vars,4),  
   nth1(1,Vars,X1),nth1(2,Vars,X2),nth1(3,Vars,X3),nth1(4,Vars,X4),  
   [e(X1,X2),e(X1,X3)] =@= [e(X1,X2),e(X3,X4)].
false.

The third idea is that numbervar/1 comes in handy for presenting the variables in a user friendly way, IMO this is better than format/2 at times.

?- length(Vars,3),numbervars(Vars).
Vars = [A, B, C].

The caveat with numbervars/1 is that the it only changes free variables. It leaves bound variables alone.

length(Vars,3),Vars=[1,2,3],numbervars(Vars).
Vars = [1, 2, 3].

?- length(Vars,3),Vars=[1,X,e],numbervars(Vars).
Vars = [1, A, e],
X = A.

Also if one is not use to using numbervars/1, notice that it does not have 2 arguments with one being the variables coming in and one with the changed variables going out. I think of it more as a directive that passes down directly into the C level code to effect a state change.



Sample code

The first predicate is code that is redundant in all the examples so is pulled out to reduce redundency. It generates the variables and graphs used in the examples. It does not use numbervars/1 as that is used latter in the demonstrations.

graphs(Vars,G1,G2,G3) :-
    length(Vars,3),
    format('Vars: ~w~n',[Vars]),
    nth1(1,Vars,X1),
    nth1(2,Vars,X2),
    nth1(3,Vars,X3),
    G1 = [e(X1,X2),e(X1,X3)],
    G2 = [e(X2,X1),e(X2,X3)],
    G3 = [e(X1,X2)],
    format('G1: ~w~n',[G1]),
    format('G2: ~w~n',[G2]),
    format('G3: ~w~n',[G3]).

The next predicate uses =@=/2 in a separate predicate to demonstrate that the comparison works when the variables are passed to another predicate. The structural relationship is not changed when calling another predicate.

similar_structure(G1,G2) :-
    G1 =@= G2.

The next two predicates demonstrate two different ways of assigning meaningful names to the variables. The first uses numbervars/1 to assign variables to the internal variables while the second predicate binds the variables to atoms.

vars_assigned_using_numbervars(G1,G2,G3,Vars) :-
    numbervars(Vars),
    format('G1: ~w~n',[G1]),
    format('G2: ~w~n',[G2]),
    format('G3: ~w~n',[G3]).

vars_unified_with_atoms(G1,G2,G3,Vars) :-
    Vars = [a,b,c],
    format('G1: ~w~n',[G1]),
    format('G2: ~w~n',[G2]),
    format('G3: ~w~n',[G3]).

The remaining code is five different examples.


Example 1

The first example demonstrates the most typical scenario of usage, that being generating structures and checking for structural equality. The graphs are structural equivalent. numbervars/1 is not used until after the comparison to demonstrate that the comparison works on the variables generated using length/2 and that the variables can be assigned meaningful human names using numbervars/1.

example(1) :-
    graphs(Vars,G1,G2,G3),
    (
        similar_structure(G1,G2)
    ->
        ansi_format([fg(green)],'G1 and G2 similar~n',[])
    ;
        ansi_format([fg(red)],'G1 and G2 NOT similar~n',[])
    ),
    vars_assigned_using_numbervars(G1,G2,G3,Vars).

Example 1 run:

?- example(1).
Vars: [_9078,_9084,_9090]
G1: [e(_9078,_9084),e(_9078,_9090)]
G2: [e(_9084,_9078),e(_9084,_9090)]
G3: [e(_9078,_9084)]
G1 and G2 similar
G1: [e(A,B),e(A,C)]
G2: [e(B,A),e(B,C)]
G3: [e(A,B)]
true.

Example 2

The second example does not use numbervars/1 but binds the variables to atoms.This example is for comparison with examples 3 and 4. In the third example numbervars/1 will be used before binding the variables to atoms and in the forth example the reverse is done, variables will be bound to atoms before using numbervars/1.

example(2) :-
    graphs(Vars,G1,G2,G3),
    (
        similar_structure(G1,G2)
    ->
        ansi_format([fg(green)],'G1 and G2 similar~n',[])
    ;
        ansi_format([fg(red)],'G1 and G2 NOT similar~n',[])
    ),
    vars_unified_with_atoms(G1,G2,G3,Vars).

Example 2 run:

?- example(2).
Vars: [_13808,_13814,_13820]
G1: [e(_13808,_13814),e(_13808,_13820)]
G2: [e(_13814,_13808),e(_13814,_13820)]
G3: [e(_13808,_13814)]
G1 and G2 similar
G1: [e(a,b),e(a,c)]
G2: [e(b,a),e(b,c)]
G3: [e(a,b)]
true.

Example 3

In the third example numbervars is used before binding the variables to atoms.

example(3) :-
    graphs(Vars,G1,G2,G3),
    (
        similar_structure(G1,G2)
    ->
        ansi_format([fg(green)],'G1 and G2 similar~n',[])
    ;
        ansi_format([fg(red)],'G1 and G2 NOT similar~n',[])
    ),
    vars_assigned_using_numbervars(G1,G2,G3,Vars),
    vars_unified_with_atoms(G1,G2,G3,Vars).

Example 3 run:

?- example(3).
Vars: [_3480,_3486,_3492]
G1: [e(_3480,_3486),e(_3480,_3492)]
G2: [e(_3486,_3480),e(_3486,_3492)]
G3: [e(_3480,_3486)]
G1 and G2 similar
G1: [e(A,B),e(A,C)]
G2: [e(B,A),e(B,C)]
G3: [e(A,B)]
false.

Notice that the result is false. AFAIK this is because one can not use numbervars/1 and then bind the variables, or until Jan W. shows me something else that I don’t know.


Example 4

example(4) :-
    graphs(Vars,G1,G2,G3),
    (
        similar_structure(G1,G2)
    ->
        ansi_format([fg(green)],'G1 and G2 similar~n',[])
    ;
        ansi_format([fg(red)],'G1 and G2 NOT similar~n',[])
    ),
    vars_unified_with_atoms(G1,G2,G3,Vars),
    vars_assigned_using_numbervars(G1,G2,G3,Vars).

Example 4 run:

?- example(4).
Vars: [_10722,_10728,_10734]
G1: [e(_10722,_10728),e(_10722,_10734)]
G2: [e(_10728,_10722),e(_10728,_10734)]
G3: [e(_10722,_10728)]
G1 and G2 similar
G1: [e(a,b),e(a,c)]
G2: [e(b,a),e(b,c)]
G3: [e(a,b)]
G1: [e(a,b),e(a,c)]
G2: [e(b,a),e(b,c)]
G3: [e(a,b)]
true.

Notice that one can call numbervars/1 after binding the variables but numbervars/1 will only assign a variable name to an unbound variable so in this case numbervars/1 had no effect.


Example 5

The fifth and last example demonstrates graphs that are not structural equivalent. numbervars/1 is not used until after the comparison to demonstrate that the comparison works on the variables generated using length/2 and that the variables can be assigned meaningful human names using numbervars/1.

example(5) :-
    graphs(Vars,G1,G2,G3),
    (
        similar_structure(G1,G3)
    ->
        ansi_format([fg(green)],'G1 and G3 similar~n',[])
    ;
        ansi_format([fg(red)],'G1 and G3 NOT similar~n',[])
    ),
    vars_assigned_using_numbervars(G1,G2,G3,Vars).

Example 5 run:

?- example(5).
Vars: [_15470,_15476,_15482]
G1: [e(_15470,_15476),e(_15470,_15482)]
G2: [e(_15476,_15470),e(_15476,_15482)]
G3: [e(_15470,_15476)]
G1 and G3 NOT similar
G1: [e(A,B),e(A,C)]
G2: [e(B,A),e(B,C)]
G3: [e(A,B)]
true.


Notes:

If one thinks this code is similar to some constraint satisfaction problems they would not be wrong, but if one tries to use this to understand constraints they would only be seeing a very small part of constraint stratification solving so please do not use this code as a springboard to learning constraints.

1 Like