Analysis as deduction

Reading

Shieber et al. (1995) on parsing as deduction and Kallmeyer (2013) on the LCFRS inference rules used in the final project.

CKY and Earley appear to be different algorithms because their charts contain different objects and their loops follow different orders. So what do they have in common? Both can be specified as a set of inference rules over partial analyses. This is the analysis-as-deduction framework (Shieber et al. 1995).

Four components

A deductive parser specifies four objects:

Items represent partial analyses.
Axioms are items licensed without antecedent items.
Inference rules derive a consequent item from antecedent items.
A goal item represents a complete analysis of the input.

For CKY, an item $[A,i,j]$ states that $A$ spans $[i,j]$. The lexical axioms are $[A,i,i+1]$ when $A\rightarrow\sigma_i$ is a rule, and the binary inference is

\[ \frac{[B,i,k]\qquad[C,k,j]} {[A,i,j]} \quad A\rightarrow BC\in R. \]

The goal is $[S,0,n]$.

For Earley, an item is a dotted rule $[A\rightarrow\alpha\bullet\beta,i,j]$. Prediction, scanning, and completion are its inference rules, and a completed start item over $[0,n]$ is the goal. Thus, the two parsers differ in their logic, not in the general notion of deduction.

Agenda-based control

An agenda-based parser separates the inference rules from the order in which they are applied. It maintains an agenda of newly licensed items and a chart of items already processed.

put every axiom on the agenda
while the agenda is not empty:
    remove an item together with one proposed backpointer
    if the item's core is already in the chart:
        merge the proposed backpointer into that chart entry
        continue
    add the item and its backpointer set to the chart
    apply every inference rule involving the new item
    put each consequent and proposed backpointer on the agenda

The chart prevents duplicate logical work. Its entries must nevertheless merge backpointers from later proofs of the same core item; discarding those backpointers would preserve recognition but lose parses. The accumulated backpointers record which antecedents licensed an item, allowing the parser to reconstruct proofs after deduction terminates.

Why agenda order does not change the result

Why should changing the agenda order leave the final chart unchanged? For a fixed input and grammar, suppose the deductive system has finitely many possible items. Let $C^*$ be the smallest set that contains every axiom and is closed under the inference rules. This set is the logical chart that any exhaustive control strategy should compute.

First, every item placed on the agenda belongs to $C^*$. The initial agenda contains only axioms. Later items are consequents of rules whose antecedents were already licensed, and closure thus puts those consequents in $C^*$. By induction on the time at which an item is enqueued, the computed chart cannot contain anything outside $C^*$.

For the reverse direction, consider any item in $C^*$. It has a finite proof from axioms. We induct on the height of that proof. A height-zero item is an axiom and begins on the agenda. For a taller proof, every antecedent has a shorter proof, so the induction hypothesis says that the exhaustive algorithm eventually processes each antecedent. When the last required antecedent is processed, the algorithm applies the inference rule and enqueues the consequent. Thus, every item in $C^*$ eventually enters the chart.

The two inclusions show that any exhaustive FIFO, LIFO, or priority agenda computes exactly $C^*$. Order may change when an item is found and how much unproductive work occurs first, but it does not change the completed logical chart.

Question

If we replace the FIFO agenda with a priority queue, have we changed the grammar or the deductive logic?

Answer

No. We have changed the control strategy—the order in which licensed items are processed. If both strategies run to completion, they derive the same chart. A priority queue may nevertheless find a preferred goal earlier.

The final project keeps this control structure and replaces CFG items with MCFG items that contain tuples of spans. The main implementation problem is thus to encode the MCFG inference rules and their span constraints without building a new parser loop for each grammar.

References

Kallmeyer, Laura. 2013. “Linear Context-Free Rewriting Systems.” Language and Linguistics Compass 7 (1): 22–38. https://doi.org/10.1002/lnc3.359.

Shieber, Stuart M., Yves Schabes, and Fernando C. N. Pereira. 1995. “Principles and Implementation of Deductive Parsing.” The Journal of Logic Programming, Computational Linguistics and Logic Programming, vol. 24 (1): 3–36. https://doi.org/10.1016/0743-1066(95)00035-I.

--- title: Analysis as deduction bibliography: ../references.bib --- ::: {.callout-tip} ## Reading @shieber_principles_1995 on parsing as deduction and @kallmeyer_linear_2013 on the LCFRS inference rules used in the final project. ::: CKY and Earley appear to be different algorithms because their charts contain different objects and their loops follow different orders. So what do they have in common? Both can be specified as a set of inference rules over partial analyses. This is the **analysis-as-deduction framework** [@shieber_principles_1995]. ## Four components A deductive parser specifies four objects: 1. **Items** represent partial analyses. 2. **Axioms** are items licensed without antecedent items. 3. **Inference rules** derive a consequent item from antecedent items. 4. A **goal item** represents a complete analysis of the input. For CKY, an item $[A,i,j]$ states that $A$ spans $[i,j]$. The lexical axioms are $[A,i,i+1]$ when $A\rightarrow\sigma_i$ is a rule, and the binary inference is $$ \frac{[B,i,k]\qquad[C,k,j]} {[A,i,j]} \quad A\rightarrow BC\in R. $$ The goal is $[S,0,n]$. For Earley, an item is a dotted rule $[A\rightarrow\alpha\bullet\beta,i,j]$. Prediction, scanning, and completion are its inference rules, and a completed start item over $[0,n]$ is the goal. Thus, the two parsers differ in their logic, not in the general notion of deduction. ## Agenda-based control An **agenda-based parser** separates the inference rules from the order in which they are applied. It maintains an agenda of newly licensed items and a chart of items already processed. ```text put every axiom on the agenda while the agenda is not empty: remove an item together with one proposed backpointer if the item's core is already in the chart: merge the proposed backpointer into that chart entry continue add the item and its backpointer set to the chart apply every inference rule involving the new item put each consequent and proposed backpointer on the agenda ``` The chart prevents duplicate logical work. Its entries must nevertheless merge backpointers from later proofs of the same core item; discarding those backpointers would preserve recognition but lose parses. The accumulated backpointers record which antecedents licensed an item, allowing the parser to reconstruct proofs after deduction terminates. ## Why agenda order does not change the result Why should changing the agenda order leave the final chart unchanged? For a fixed input and grammar, suppose the deductive system has finitely many possible items. Let $C^*$ be the smallest set that contains every axiom and is closed under the inference rules. This set is the logical chart that any exhaustive control strategy should compute. First, every item placed on the agenda belongs to $C^*$. The initial agenda contains only axioms. Later items are consequents of rules whose antecedents were already licensed, and closure thus puts those consequents in $C^*$. By induction on the time at which an item is enqueued, the computed chart cannot contain anything outside $C^*$. For the reverse direction, consider any item in $C^*$. It has a finite proof from axioms. We induct on the height of that proof. A height-zero item is an axiom and begins on the agenda. For a taller proof, every antecedent has a shorter proof, so the induction hypothesis says that the exhaustive algorithm eventually processes each antecedent. When the last required antecedent is processed, the algorithm applies the inference rule and enqueues the consequent. Thus, every item in $C^*$ eventually enters the chart. The two inclusions show that any exhaustive FIFO, LIFO, or priority agenda computes exactly $C^*$. Order may change when an item is found and how much unproductive work occurs first, but it does not change the completed logical chart. ::: {.callout-caution} ## Question If we replace the FIFO agenda with a priority queue, have we changed the grammar or the deductive logic? ::: ::: {.callout-tip collapse=true} ## Answer No. We have changed the control strategy—the order in which licensed items are processed. If both strategies run to completion, they derive the same chart. A priority queue may nevertheless find a preferred goal earlier. ::: The final project keeps this control structure and replaces CFG items with MCFG items that contain tuples of spans. The main implementation problem is thus to encode the MCFG inference rules and their span constraints without building a new parser loop for each grammar.