Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Lambek Calculus Proofs and Tree Automata
| |
|
Lambek Calculus Proofs and Tree Automata
Hans-Joerg Tiede2 
| (2) |
Department of Mathematics and Computer Science, Illinois Wesleyan University, 2900, Bloomington, IL 61702-2900, USA |
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.
The results of this paper are contained in my dissertation (Tiede, 1999). I would like to thank my thesis advisor Larry Moss,
Johan van Benthem, Christian Retoré, and two anonymous referees for comments on this paper. All remaining errors are the author’s.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|