Lassen Sie uns zuerst ein Gefühl für und Nachher ( β ) bekommen . Betrachten Sie einen Ableitungsbaum, der β enthält . "enthält" bedeutet hier, dass Sie Teilbäume wegschneiden können, sodass β ein Teilwort der Baumfront ist. Dann sind die Vorher- (Nachher-) Mengen alle möglichen Fronten des Baumteils links (rechts) von β :Before(β)After(β)βββ
[ Quelle ]
Wir müssen also eine Grammatik für den horizontal (vertikal) gesäumten Teil des Baumes erstellen. Das scheint einfach zu sein, da wir bereits eine Grammatik für den gesamten Baum haben. wir müssen nur sicherstellen, dass alle sententialen Formen Wörter sind (ändern Sie die Alphabete), diejenigen herausfiltern, die kein enthalten (das ist eine reguläre Eigenschaft, da β festgelegt ist) und alles nach (vor) β wegschneiden , einschließlich β . Dieses Schneiden sollte auch möglich sein.ββββ
Nun zu einem formellen Beweis. Wir werden die Grammatik wie beschrieben transformieren und die Verschlusseigenschaften von , um das Filtern und Schneiden durchzuführen, dh wir führen einen nicht konstruktiven Beweis durch.CFL
Sei eine kontextfreie Grammatik. Es ist leicht zu erkennen, dass SF ( G ) kontextfrei ist. konstruiere G ' = ( N ' , T ' , δ ' , N S ) wie folgt:G=(N,T,δ,S)SF(G)G′=(N′,T′,δ′,NS)
- N′={NA∣A∈N}
- T′=N∪T
- δ′={α(A)→α(β)∣A→β∈δ}∪{NA→A∣A∈N}
mit für alle t ∈ T und α ( A ) = N A für alle einer ∈ N . Es ist klar, dass L ( G ' ) = SF ( G ) ; Daher sind die entsprechenden Präfix- Abschlüsse Pref ( SF ( G ) ) und Suffix -Abschlüsse Suff ( SF ( G ) ) auch kontextfrei¹.α(t)=tt∈Tα(A)=NAa∈NL(G′)=SF(G)Pref(SF(G))Suff(SF(G))
Nun, für jeden sind L ( β ( N ∪ T ) * ) und L ( ( N ∪ T ) * β ) reguläre Sprachen. Als C F L unter Schnitt geschlossen und rechts / links Quotienten mit regulären Sprachen, erhalten wirβ∈(N∪T)∗L(β(N∪T)∗)L((N∪T)∗β)CFL
Before(β)=(Pref(SF(G)) ∩ L((N∪T)∗β))/β∈CFL
und
.After(β)=(Suff(SF(G)) ∩ L(β(N∪T)∗))∖β∈CFL
¹ CFL is closed under right (and left) quotient; Pref(L)=L/Σ∗ and similar for Suff yield prefix resp. suffix closure.
and
are CF.
Proof? ForBefore(L,β) construct a non-deterministic finite-state transducer Tβ that scans a string, outputting every input symbol it sees and simultaneously searches non-deterministically for β . Whenever Tβ sees the first symbol of β it forks non-deterministically and ceases outputting symbols until either it finishes seeing β or it sees sees a symbol that deviates from β , stopping in either case. If Tβ sees β in full, it accepts upon stopping, which is the only way it accepts. If it sees a deviation from β , it rejects.
The lemma can be jiggered to handle cases whereβ could overlap with itself (like abab -- keep looking for β even while in the midst of scanning for a prior β ) or appears multiple times (actually, the original non-determinisic forking already handles that).
It's fairly clear thatTβ(L)=Before(L,β) , and since the CFLs are closed under finite-state transduction, Before(L,β) is therefore CF.
A similar argument goes forAfter(L,β) , or it could be done with string reversals from Before(L,β) , CFLs also being closed under reversal:
Actually, now that I see the reversal argument, it would be even easier to start withAfter(L,β) , since the transducer for that is simpler to describe and verify -- it outputs the empty string while looking for a β . When it finds β it forks non-deterministically, one fork continuing to look for further copies of β , the other fork copying all subsequent characters verbatim from input to output, accepting all the while.
What remains is to make this work for sentential forms as well as CFLs. But that is pretty straightforward, since the language of sentential forms of a CFG is itself a CFL. You can show that by replacing every non-terminalX throughout G by say X′ , declaring X to be a terminal, and adding all productions X′→X to the grammar.
I'll have to think about your question on unambiguity.
quelle