- Up - | Next >> |
Let's now make this intuitive algorithm a little more formal and describe it as an inference-based process. We write STRING [A1 ... Ak]
to state that we have a string of categories A1 ... Ak
. We write RULE C -> C1 ... Cn
to state that the grammar contains a rule rewriting category C
to the sequence of categories C1 ... Cn
. Now consider the backward application of a rule. It can be formalized by the inference rule (schema) below:
STRING [A1 ... Ap C1 ... Cn B1 ... Bq]
RULE C -> C1 ... Cn
--------------------------------------
STRING [A1 ... Ap C B1 ... Bq]
Above the line are the two premises, and below the line is the conclusion. Now, we turn to the case of a singleton sequence. We write RECOGNIZED C
to state that we have recognized category C
. The recognition inference rule can be formulated as follows:
STRING [C]
------------
RECOGNIZED C
Thus the question of whether the sequence of terminals T1 ... Tk
is in the language generated by the grammar can be reformulated as the question of whether, for some C
, RECOGNIZED C
is in the inferential closure of STRING [T1 ... Tk]
.
- Up - | Next >> |