Proof that locality is sufficient in showing two graphs are isomorphic

Question

Using the graph representation with (node, [list of neighbours]), to show that two graphs are isomorphic it is sufficient to:

• show that the vertices have the same degree and
• for every pair of vertices with the same degree, the degrees of the nodes in their adjacency list must be the same.

The last point was a bit ambiguous, in the sense that in two graphs many vertices could have the same degree, but between two isomorphic graphs their is a bijective function (an exact one to one mapping) between them such that their adjacency list maps correctly.

My question is what's the proof behind this? Why is this sufficient? For me, this is not clear at all, because this is, overall, a local property and I can't understand how this generalizes to the whole graph.

If it's easier to track what I said on code...Prolog it's pretty verbose at this part.

:- dynamic p/2.
graph1([n(1,[2,3,4]),n(2,[1,3]),n(3,[1,2,4]),n(4,[1,3])]).
graph2([n(a,[b,d]),n(b,[a,d,c]),n(c,[d,b]),n(d,[a,b,c])]).
eq_perm([H1|T1],L2,EQ):-
    delete(H2,L2,T2), % we generate a solution here
    P = ..[EQ, H1, H2],
    P,
    eq_perm(T1,T2,EQ).
eq_node(N1,N2):-
    p(N1,N2).
eq_node(N1,_):-
    p(N1,_), !, fail.
eq_node(_,N2):-
    p(_,N2), !, fail.
eq_node(N1,N2):-
    asserta(p(N1,N2)).
eq_node(N1,N2):-
    retract(p(N1,N2)).
iso_graph(G1,G2):-
    eq_perm(G1,G2,eq_neighb).
eq_neighb(n(N1,L1),n(N2,L2)):-
    eq_node(N1,N2),
    eq_perm(L1,L2,eq_node).

Answer 1

This method fails on regular graphs. For example, it fails on the following two graphs: the hexagon, and two disconnected triangles.

More generally, if you continue to explore neighbors' neighbors and so on, you get the 1-dimensional Weisfeiler–Lehman method. If you start with $k$-tuples of vertices, you get the $k$-dimensional Weisfeiler–Lehman method. Cai, Fürer and Immerman proved in An optimal lower bound on the number of variables for graph identification that there exist non-isomorphic graphs on $n$ vertices which fail to be distinguished by the $k$-dimensional Weisfeiler–Lehman method unless $k = \Omega(n)$. Since the running time of the method in the worst case is asymptotically $n^{k+1}$, this shows that the Weisfeiler–Lehman method doesn't yield a subexponential time algorithm for graph isomorphism.

For more on the Weisfeiler–Lehman method, check a paper of Douglas, or the recent work of Neuen and Schweitzer.