hello everybody:

I want to implement an algorithm for depth first searching(DFS) to a graph. so I give  the following "toy" theory (from a book written by Lawrence C. Paulson).

I don't know how to give the measure function for the function "depthf" despite  the lemma "dfb" can be proved by (grind) simply, that is to say, this function to this test is terminated.
I think the recursive fucntion "depthf" should be terminated because of the finity of the graph represented by list[[T,T]].

And another question, if the graph is very large,  how about DFS's  efficiency?

who can help me?  thank you very much.

t: THEORY
BEGIN

T: TYPE = {a, b, c, d, e, f, g}

TL : TYPE = list[T]

G: TYPE = list[[T,T]]

graph1:  G =
(: (a, b), (a, c), (a, d), (b, e), (c, f), (d, e), (e, f), (e, g) :)

%   /----->b--------\
%  |                      |
%  |                     \/
%  a -> c -> f <-- e --> g
%  |                     /\
%  |                     |
%  \- ---->d-------/

%      graph1

nexts(a: T, l: G): RECURSIVE TL =   CASES l
OF null: (: :),
cons(hd, tl):
IF a = hd`1 THEN cons(hd`2, nexts(a, tl)) ELSE nexts(a, tl) ENDIF
ENDCASES
MEASURE  length(l);

depthf(l: TL, g: G, vis: TL): RECURSIVE TL =
CASES l
OF null: reverse(vis),
cons(hd, tl):
IF member(hd, vis) THEN depthf(tl, g, vis)
ELSE depthf(append(nexts(hd, g), tl), g, cons(hd, vis))
ENDIF
ENDCASES
MEASURE ......;

dfb: LEMMA
depthf((: b :), cons((f, d), graph1), (: :)) = (: b, e, f, d, g :)

END t

Q.G.,  XU
2006-04-04