Skip to main content
Contribution to Book
Lambek Calculus Proofs and Tree Automata
Logical Aspects of Computational Linguistics (2001)
  • Hans Joerg Tiede, Illinois Wesleyan University
Abstract
We investigate natural deduction proofs of the Lambek calculus from the point of view of tree automata. The main result is that the set of proofs of the Lambek calculus cannot be accepted by a finite tree automaton. The proof is extended to cover the proofs used by grammars based on the Lambek calculus, which typically use only a subset of the set of all proofs. While Lambek grammars can assign regular tree languages as structural descriptions, there exist Lambek grammars that assign non-regular structural descriptions, both when considering normal and non-normal proof trees. Combining the results of Pentus (1993) and Thatcher (1967), we can conclude that Lambek grammars, although generating only context-free languages, can extend the strong generative capacity of context-free grammars. Furthermore, we show that structural descriptions that disregard the use of introduction rules cannot be used for a compositional semantics following the Curry-Howard isomorphism.
Disciplines
Publication Date
2001
Editor
Moortgat, Michael
Publisher
Springer
Series
Lecture Notes in Computer Science
ISBN
978-3-540-42251-8
Citation Information
Hans Joerg Tiede. "Lambek Calculus Proofs and Tree Automata" Berlin / HeidelbergLogical Aspects of Computational Linguistics (2001)
Available at: http://works.bepress.com/htiede/1/