A Lambek-automaton

One of the popular frameworks in computational linguistics 
for the specifcation of natural language syntax 
and formal languages is Type-Logical Grammars (TLGs).
Type-logical grammars are lexicalized, in contrast to
rewriting grammars. They have a fixed universal
set of rules, relying on an underlying logic (syntactic calculus).
In a type-logical grammar each terminal is assigned a finite set of categories, 
and a grammatical process of derivation, reducing sequences
of categories until a specific initial category is obtained. 
This process is presented as deduction in the underlying logic.

One central logical system for obtaining deductions in these grammars is
the (associative) Lambek calculus L, 
a linear logic with directed implications without structural rules
(except associativity). Some years ago, Pentus resolved positively Chomsky's
conjecture, that the L-generated formal languages coincide with the
context-free languages.

A natural question arising is, what is the automata-theoretic
counterpart of $\bL$-grammars? In view of Pentus' result, obviously
PDAs have the right generative power. However, one might pose
a stricter requirement, of some `tight relation' between derivations
in the grammar and computations of the automaton, making them
working in a "similar way". In this sense, PDAs
are not a satisfactory solution, as there is no simple connection
between the way they accept a language and between the way an $\bL$-grammar
generates the language. In particular, there is no direct remnant to
the hypothetical reasoning (using dischargable assumptions)
employed by TLGs.

The goal of this work is to define an automaton that 
is adequate under the stricter desideratum presented above.


(Joint work with Tatyana Veksler)