Hi Johan:

Thank you for your exploration.

For related viewgraphs see:

/home/lieber/.www/com3362/lectures/trav-theory-aoos.PDF

around viewgraph 37.

-- Karl
=======================

>From johan@ccs.neu.edu Tue Jun 23 01:02:49 1998
>To: Karl Lieberherr <lieber@ccs.neu.edu>
>cc: johan@ccs.neu.edu, dougo@ccs.neu.edu, mira@ccs.neu.edu
>Subject: Re: proving a theorem 
>From: Johan Ovlinger <johan@ccs.neu.edu>
>
>Well. I belive what you meant to say, I think. I just don't understand
>your notation well enough to reach a conclusion. See the line ***
>
>anyway, we forge ahead

Good idea.

>
>A Strategy (S) is equivalent to a Regular Expression, ie it defines a

I like that statement and it is one which we have not yet
fully explored. One way to read your statement is to
think of the examples:

"from A to B" corresponds to the regular expression "A any* B".
"from A via C to B" corresponds to the regular expression "A any* C any* B".

The general question: what is a general algorithm to map strategy graphs
into equivalent regular expressions?
Even more useful is:
what is a general algorithm to map strategy graphs
into an equivalent NDFA?

>language defined over the classes in the strategy = L(S)

>
>An aside: 
>    If we define substrategy as let inclusion over the

That is the intuition.

>    languages generated by two strategies, then we are done with our
>    discussion s1 substrat s2 == L(s1) <= L(s2). I show (kinda) below
>    that this is a reasonable definition. Can we pull any tricks to
>    compute this quickly?

I think so. I think the traversal graph algorithm will help.

>
>A ClassGraph CG is also equivalent to a Regular expression, and it also
>defines a language over the set of classes in the classgraph = L(CG)

Right. How do you translate a class graph into a regular expression?

>
>I understand pathset to be defined: PathSet[G](S) ==  L(G) intersect L(S)

Right. But L(G) is defined wrt S. cannot commute G and S.

>*** I don't know what you mean by PathSet[S1](S2). 

We view S1 as a class graph. This is just graph theory.
Both class graphs and strategy graphs are graphs and the same graph
may be viewed two ways.

>I'll just ignore my
>poor understanding and continue using blind substitution.  Beware!
>
>I'll write intersect as /\, and union \/..
>
>Now we reformulate the definition of substrategy
>
> given strategies s1 and s2 
> s1 is a substrategy of s2, if 
> for all class graphs G:
>  PathSet[G](s1) is a subset of PathSet[G](s2) ==
>  L(G) /\ L(s1) <= L(G) /\ L(s2)
>
>Theorem: s1 substrat s2 iff PathSet[s1](s2) not empty
>              ==
>         s1 substrat s2 iff L(s1) /\ L(s2) not empty
>
>Well. This makes no sense. Since a intersect b == b intersect a, our
>defintion as I have interpreted it is reflexive.  So either my
>understanding of PathSet is wrong or the theorem is wrong.
>

Yes, the theorem is wrong. What is missing?

>
>However, we can probably start from
>
> s1 substrat s2 
>    iff for all G,  L(G) /\ L(s1) <= L(G) /\ L(s2)
>      
>and simplify this to something more tractable. I'm not certain that
>the removing of L(G) is legal...
>
>    L(G) /\ L(s1) <= L(G) /\ L(s1) ->  (complement both sides)
>    _____________    _____________
>    L(G) /\ L(s1) => L(G) /\ L(s1) ->  (whathisface equality)
>    ____    _____    ____    _____
>    L(G) \/ L(s1) => L(G) \/ L(s2) ->  subtract L(G) from both sides

This is incorrect!
(X union P) subset (X union Q) does not imply P subset Q
counterexample: choose X a big set.

>    _____            _____             (is this allowed?)
>    L(s1)         => L(s2)         ->                 
>    
>    L(s1)         <= L(s2)
>
>which brings us back to the aside above.
>
>The question remains as to how to figure out this quickly. Maybe the
>key is to pass along a token set as when we execute the strategy, and
>thus try to determine subset inclusion.
>
>Johan
>
>

Now we need an efficient algorithm to check whether L(s1) is a subset
of L(s2).