5.2.1 Recognition as Inferential Closure

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].


Denys Duchier, Claire Gardent and Joachim Niehren
Version 1.3.99 (20050412)