-- LR1Items.mesa
-- last edit September 11, 1984 3:10:46 pm PDT
DIRECTORY
GrammarBasic USING[Symbol, Grammar],
LR1ItemSetsBasic USING[LR1ItemSubset];
LR1Items: CEDAR DEFINITIONS =
BEGIN OPEN GrammarBasic, LR1ItemSetsBasic;
GenKernelV1EpsilonItemSubsets: PROC[Grammar, PROC[LR1ItemSubset]];
GenKernelGoTo1ItemSubsetsFromKernelItemSubset: PROC[LR1ItemSubset, PROC[Symbol, LR1ItemSubset]];
GenCloseOfLR1ItemSubset: PROC[firstSubset: LR1ItemSubset, for: PROC[LR1ItemSubset]];
END..
-- I choose to record some claims here that are not recorded elsewhere. Some of these claims are used to support the implementation, and some will be used at a future date.
-- The first set of claims has to do with the computation of Close1(A).
-- 1) Let Xt([A←a.b, u]) = (IF u = e THEN [A←a.b, t] ELSE [A𡤊.b, u]); where t is sequence of terminals and length(t) d 1. Extend Xt to sets in the usual way: Xt(A) = *{Xt(a) | a  A}.
-- 2) Let Y(C) = {[B←.d, v] | ( A', a', b', u') ([A'←a'.Bb', u']  C and v  FIRST1(b'u') and B←d a production)}. Notice that Close1(C) = C * Y(C) * Y2(C) * ...
-- 3) Basic Claim: Xt(Y(C)) = Y(Xt(C)). Trivial if t = e, so assume t ` e.
--3A) lets prove that the right side is included in the left. Let [B←.d, v]  Y(Xt(C)). Thus we have A', a', b', u' such that [A'←a'.Bb', u']  Xt(C), v  EFF1(b'u'), and B←d a production. Let [A'←a'.Bb', u'] = Xt([A'←a'.Bb', u'']), where [A'←a'.Bb', u'']  C. The goal is to find a v' such that [B←.d, v']  Y(C) and Xt([B←.d, v']) = [B←.d, v], thus proving [B←.d, v]  Xt(Y(C)). There are several cases depending on u''.
-- i) Assume u'' = t, hence u' = t also. Since u' = t ` e, and v  EFF1(b'u'), we have v ` e. So, v' = v will suffice. That is, [B←.d, v]  Y(C) as witnessed by (A', a', b', t=u''=u'), and [B←.d, v] = Xt([B←.d, v]), so [B←.d, v]  Xt(Y(C)).
-- ii) Assume u'' = e, hence u' = t, and also [A'←a'.Bb', e]  C. As in case i, since u' = t ` e, and v  EFF1(b'u'), we have v ` e. Now we examine two sub cases, depending on whether v  EFF1(b').
-- iia) v  EFF1(b'). Hence, v  EFF1(b'e), so [B←.d, v]  Y(C) as witnessed by (A', a', b', e). Finally, v ` e implies [B←.d, v]  Xt(Y(C)).
-- iib) NOT v  EFF1(b'). Thus, because v  EFF1(b'u'), we have v = u' (= t ` e) and e  EFF1(b') = EFF1(b'e). In this case, v' = e satisifies our requirements, because [B←.d, e]  Y(C) as witnessed by (A', a', b', e). FInally, v = t implies [B←.d, v] = Xt([B←.d, e])  Xt(Y(C)).
-- iii) Assume u'' ` t and u'' ` e. Hence u' = u'', so [A'←a'.Bb', u']  C, thus [B←.d, v]  Y(C) as witnessed by (A', a', b', u'). Also, as in case i), u' = u'' ` e and v  EFF1(b'u') implies v' ` e. Thus, [B←.d, v]  Xt(Y(C)).
-- 3B) lets prove that the left side is included in the right. Let [B←.d, u]  Xt(Y(C)). Since t ` e, we have u ` e. Let [B←.d, v] be the element of Y(C), such that Xt([B←.d, v]) = [B←.d, u]. Thus, we have A', a', b', u' such that [A'←a'.Bb', u']  C, v  EFF1(b'u'), and B←d a production. There are two cases: v = e, and v ` e.
-- i) First, assume v = e implying that u = t. Also, e  EFF1(b'u'), so e  EFF1(b') and u' = e. So [A'←a'.Bb', t]  Xt(C). Also, t  EFF1(b't), so [B←.d, t]  Y(Xt(C)), as witnessed by (A', a', b', t).
-- ii) second, assume v ` e, implying that u = v. Thus, [B←.d, v] = [B←.d, u], and we shall prove [B←.d, v]  Y(Xt(C)). Now, cases on u'.
-- iia) assume u' ` e. [A'←a'.Bb', u']  C, hence [A'←a'.Bb', u']  Xt(C), and [B←.d, v]  Y(Xt(C)) as witnessed by (A', a', b', u').
-- iib) assume u' = e. Since v ` e and v  EFF1(b'e), we have v  EFF1(b't). Further, [A'←a'.Bb', e]  C, so [A'←a'.Bb', t]  Xt(C). Thus, we have [B←.d, v]  Y(Xt(C)), as witnessed by (A', a', b', t).
-- 4) Close1([A←a.b, t]) = Xt(*{Xt'(Close1([A'←.d, e]) | ( A', a', b', u') ([A'←a'.A'b', u']  C and t'  EFF1(b'u') and A'←d a production)}). Hence, I can pre-tabulate Close1([A'←.d, e]), and make good headway.
-- Proof:
-- i) Using the basic claim: Xt(Close1(C)) = Xt(C * Y(C) * Y2(C) * ...) = Xt(C) * Xt(Y(C)) * Xt(Y2(C)) * ... = Xt(C) * Y(Xt(C)) * Y2(Xt(C)) * ... = Close1(Xt(C).
-- ii) Thus: Close1([A←a.b, t]) = Close1(Xt([A←a.b, e])) = Xt(Close1([A←a.b, e])).
-- iii) Further: Close1([A←a.b, e]) = *{Close1([A'←.d, t']) | ( A', a', b', u') ([A'←a'.A'b', u']  C and t'  EFF1(b'u') and A'←d a production)} = *{Xt'(Close1([A'←.d, e]) | ( A', a', b', u') ([A'←a'.A'b', u']  C and t'  EFF1(b'u') and A'←d a production)}
-- iv) Thus: Close1([A←a.b, t]) = Xt(*{Xt'(Close1([A'←.d, e]) | ( A', a', b', u') ([A'←a'.A'b', u']  C and t'  EFF1(b'u') and A'←d a production)}).
-- 5) It is a fact that all of the sets of LR(0) items and LR(1) items occuring during the construction of the canonical LR(0) graph, the LRLR(1) graph, the canonical LR(1) graph, and the Split Node graphs, are of the form Close(InitialMembers). We choose to record only the InitialMembers, and whenever there is a need to generate the full set, we run the close algorithm. This results in elements occuring in the generation of the closure more than once, but this is no problem. (This choice is that the space savings is of more importance than the time loss.) Even for equality tests, it turns out that for the actual sets constructed, Close(InitialMembers1) = Close(InitialMembers2) IFF InitialMembers1 = InitialMembers2.