Hi Paul:

can your approach  to language preserving program transformations
take a program for S2 and produce a program for S so that 
for sentences in L(S) the two programs produce the same behavior?

Did you get the proofs for your paper?

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

From qualifying examination 1997 in programming languages:

Consider the two languages defined by S and S2 in the class dictionary below.

Prove that one of the languages is a proper subset of the other.

Example = S S2 *EOF*.
S : A | B.
A = "(a" I_NList [B] ")".
B = "(b" S_NList ")".

I_NList ~ I {I}.
S_NList ~ S {S}.
S2_NList ~ S2 {S2}.

I = "i".

S2 : I | C.
C = "(" Op S2_NList ")".
Op : M | N.
M = "a".
N = "b".

Solution: (from best student solutions)

L(S2) is different from L(S) since L(S2) contains sentence "i"
while L(S) does not.

Prove that L(S) is a subset of L(S2).
Do a proof by rewriting and restricting the grammar for S2:

Rewrite without changing language:

S2 : I | W.
W : P | Q.
P = "(" "a" S2_NList ")".
Q = "(" "b" S2_NList ")".

Restrict language:

S2 : I | W.
W : P | Q.
P = "(" "a" I_NList [S2] ")". // since S2 derives I
Q = "(" "b" W_NList ")".     //  since S2 derives W
W_NList ~ {W}.

L(Q) is a subset of L(W) which is a subset of L(S2).
Therefore, we restrict the language further:

P = "(" "a" I_NList [Q] ")". // 

Next we substitute: W by S, P by A and Q by B and we get:

S : A | B.
A = "(" "a" I_NList [B] ")". 
B = "(" "b" S_NList ")".     
S_NList ~ {S}.

This grammar for S is now the same as the  original grammar for S.
Therefore, L(S) has a more restrictive definition than L(S2)
and therefore L(S) is a subset of L(S2).

-------------

Alternatively, an induction proof works but it has less of
a constructive flavor as the grammar restriction proof above.

Induction hypothesis IH(n):
For all sentences in L(S2) of length <= n we have: s in L(S) implies
s in L(S2).

IH(0) is vacuously true because the empty string is not in L(S).
Assume IH(n) is true and let s be a string of length n+1 that is generated
by S. Distinguish two cases:

1. S -> A is the first production in the derivation of s.
2. S -> B is the first production in the derivation of s.

1. 
s has the shape: A = "(" "a" I_NList [B] ")".
Since S2 : I | W  the I_NList part is generated by S2_NList.
The optional B part must have a size <= n and therefore by IH(n)
it can also be generated by S2. Thus the I_NList [B] part
can be generated by S2 {S2} [S2] = S2 {S2}.
S2 -> "(a" S2_NList ")" -> s.  Therefore s in L(S2).

2.
s has the shape: B = "(" "b" S_NList ")".
Since the length of the S_NList part is <= n, by IH(n),
it can be derived from S2. Since S2 -> "(b" S2_NList ")" we know
that s in L(S2).
qed.