Type-logical grammars

What if we treat a syntactic analysis as a proof? In a type-logical grammar, a lexical item receives a type, and a sentence is licensed when the sequence of lexical types proves a designated sentence type (Lambek 1958).

Reading

Read Moortgat (1997) on the Lambek calculus and its grammatical interpretation.

Application

The two elimination rules state these combinations directly:

\[ \frac{X/Y \qquad Y}{X} \quad /E \qquad\qquad \frac{Y \qquad X\backslash Y}{X} \quad \backslash E \]

These are directional forms of function application. The order of the premises matters because the calculus does not freely exchange hypotheses.

Question

Derive greyhounds run from $NP$ and $S\backslash NP$.

Answer

Backward application matches $Y=NP$ and $X=S$:

\[ \frac{NP \qquad S\backslash NP}{S} \quad \backslash E \]

Proof search

Parsing a string $w_1\ldots w_n$ means selecting one category $C_i$ for each word and proving

\[C_1,\ldots,C_n \vdash S.\]

This is an instance of deductive parsing: lexical assignments are axioms, logical rules are inference rules, and a proof of the goal is a parse. A chart can store proved categories over spans so that the same subproof need not be reconstructed.

Resource sensitivity

The Lambek calculus is substructural. In its basic form, it lacks three rules available in classical logic (Morrill 2011):

no exchange: word order cannot be rearranged freely;
no weakening: a lexical resource cannot be ignored; and
no contraction: a lexical resource cannot be used twice.

These restrictions connect proofs to strings. Each word occurs in an ordered position and contributes exactly once to the derivation.

We can verify that claim by induction on proofs in the application fragment. A lexical axiom contains one ordered resource and uses it once. Now suppose two smaller proofs use each of their lexical resources exactly once and preserve the order within their spans. Forward application combines an $X/Y$ proof immediately followed by a $Y$ proof; backward application combines a $Y$ proof immediately followed by an $X\backslash Y$ proof. In either case, the conclusion uses the union of the two disjoint resource sequences, in their original order, and neither premise is duplicated or discarded. Thus, every application proof uses every word in its span exactly once and in order.

Exchange, weakening, or contraction would break one part of this invariant. Exchange could reverse resources, weakening could omit one, and contraction could reuse one. Their absence is thus what gives the logical proof its string interpretation.

With semantic terms attached to lexical categories, proofs may also determine modes of semantic composition through the Curry–Howard correspondence (Carpenter 1997). The correspondence does not by itself choose a lexical meaning or resolve ambiguity; it states how a selected proof composes the meanings assigned to its premises.

Combinatory categorial grammar retains these directional categories but replaces unrestricted logical proof search with an explicitly chosen inventory of combinators.

References

Carpenter, Bob. 1997. Type-Logical Semantics. MIT Press.

Lambek, Joachim. 1958. “The Mathematics of Sentence Structure.” The American Mathematical Monthly 65 (3): 154–70.

Moortgat, Michael. 1997. “Categorial Type Logics.” In Handbook of Logic and Language. Elsevier.

Morrill, Glyn. 2011. Categorial Grammar: Logical Syntax, Semantics, and Processing. Oxford University Press.

--- title: Type-logical grammars bibliography: ../../references.bib --- What if we treat a syntactic analysis as a proof? In a type-logical grammar, a lexical item receives a type, and a sentence is licensed when the sequence of lexical types proves a designated sentence type [@lambek1958mathematics]. ::: {.callout-note title="Reading"} Read @moortgat1997categorial on the Lambek calculus and its grammatical interpretation. ::: ## Categories Let $S$, $NP$, and $N$ be atomic categories. Complex categories are built with two directional slashes: - $X/Y$ requires a $Y$ immediately to its right and returns an $X$. - $X\backslash Y$ requires a $Y$ immediately to its left and returns an $X$. Under this convention, an intransitive verb has category $S\backslash NP$, and a transitive verb has category $(S\backslash NP)/NP$. For *greyhounds chase rabbits*, the lexical sequence is $$NP \qquad (S\backslash NP)/NP \qquad NP.$$ The complete proof is $$ \frac{ NP \qquad \displaystyle \frac{(S\backslash NP)/NP\qquad NP} {S\backslash NP}\;/E }{S}\;\backslash E. $$ Read it from the lexical items upward. The verb first consumes the $NP$ on its right and returns $S\backslash NP$. That result then consumes the $NP$ on its left and returns $S$. Every lexical category appears once as a premise, and the left-to-right order of the three premises is unchanged. ## Application The two elimination rules state these combinations directly: $$ \frac{X/Y \qquad Y}{X} \quad /E \qquad\qquad \frac{Y \qquad X\backslash Y}{X} \quad \backslash E $$ These are directional forms of function application. The order of the premises matters because the calculus does not freely exchange hypotheses. ::: {.callout-note collapse="true" title="Question"} Derive *greyhounds run* from $NP$ and $S\backslash NP$. ::: {.callout-tip collapse="true" title="Answer"} Backward application matches $Y=NP$ and $X=S$: $$ \frac{NP \qquad S\backslash NP}{S} \quad \backslash E $$ ::: ::: ## Proof search Parsing a string $w_1\ldots w_n$ means selecting one category $C_i$ for each word and proving $$C_1,\ldots,C_n \vdash S.$$ This is an instance of [deductive parsing](../deductive-parsing.qmd): lexical assignments are axioms, logical rules are inference rules, and a proof of the goal is a parse. A chart can store proved categories over spans so that the same subproof need not be reconstructed. ## Resource sensitivity The Lambek calculus is *substructural*. In its basic form, it lacks three rules available in classical logic [@morrill2011categorial]: - no exchange: word order cannot be rearranged freely; - no weakening: a lexical resource cannot be ignored; and - no contraction: a lexical resource cannot be used twice. These restrictions connect proofs to strings. Each word occurs in an ordered position and contributes exactly once to the derivation. We can verify that claim by induction on proofs in the application fragment. A lexical axiom contains one ordered resource and uses it once. Now suppose two smaller proofs use each of their lexical resources exactly once and preserve the order within their spans. Forward application combines an $X/Y$ proof immediately followed by a $Y$ proof; backward application combines a $Y$ proof immediately followed by an $X\backslash Y$ proof. In either case, the conclusion uses the union of the two disjoint resource sequences, in their original order, and neither premise is duplicated or discarded. Thus, every application proof uses every word in its span exactly once and in order. Exchange, weakening, or contraction would break one part of this invariant. Exchange could reverse resources, weakening could omit one, and contraction could reuse one. Their absence is thus what gives the logical proof its string interpretation. With semantic terms attached to lexical categories, proofs may also determine modes of semantic composition through the Curry–Howard correspondence [@carpenter1997type]. The correspondence does not by itself choose a lexical meaning or resolve ambiguity; it states how a selected proof composes the meanings assigned to its premises. [Combinatory categorial grammar](combinatory-categorial-grammars.qmd) retains these directional categories but replaces unrestricted logical proof search with an explicitly chosen inventory of combinators.