Proof Tree Automata

In this paper, we continue our investigation of the strong generative capacity of proof theoretical grammars using natural deduction proof trees as the structures that grammars assign to their languages. We review the results that were previously obtained for associative Lambek grammars and extend the methods used there to non-associative Lambek grammars. The main result of this paper is that non-associative Lambek grammars, which generate precisely the context-free string languages, can assign structures to their languages that are not local, thus more complex than the structures context-free grammars can assign. When only proof trees in normal form are considered, the tree languages assigned by non-associative Lambek grammars are always regular, thus their structures are less complex than those of associative Lambek grammars, which have been shown to be able to assign non-regular tree languages to their languages. As AB grammars (also known as categorial grammars) only assign local tree languages to their languages, we arrive at a hierarchy of proof theoretical grammars with respect to their strong generative capacity.