Some publications of Mati Pentus

Papers in English

Equivalent Types in Lambek Calculus and Linear Logic

Mati Pentus

Abstract

In 1958 J. Lambek introduced a calculus L of syntactic types and defined an equivalence relation on types: "x~y means that there exists a sequence x=x₁,...,x_n=y (n>0), such that x_i->x_i+1 or x_i+1->x_i (0<i<n)". We show that this equivalence of types is decidable for directed and non-directed Lambek calculi and for multiplicative fragments of ordinary and non-commutative linear logics. Moreover, we characterize equivalent types in these calculi in terms of simple derivability invariants (primitive type counts, balance, etc.).

Lambek grammars are context free

Mati Pentus

Abstract

In this paper the Chomsky Conjecture is proved: all languages recognized by the Lambek calculus are context free.

The conjoinability relation in Lambek calculus and linear logic

Mati Pentus

Abstract

In 1958 J. Lambek introduced a calculus L of syntactic types and defined an equivalence relation on types: "x~y means that there exists a sequence x=x₁,...,x_n=y (n>0), such that x_i->x_i+1 or x_i+1->x_i (0<i<n)". He pointed out that x~y if and only if there is join z such that x->z and y->z.

This paper gives an effective characterization of this equivalence for the Lambek calculi L and LP, and for the multiplicative fragments of Girard's and Yetter's linear logics. Moreover, for the non-directed Lambek calculus LP and the multiplicative fragment of Girard's linear logic, we present linear time algorithms deciding whether two types are equal, and finding a join for them if they are.

Models for the Lambek calculus

Mati Pentus

Abstract

We prove that the Lambek calculus is complete w.r.t. L-models, i.e., free semigroup models. We also prove the completeness w.r.t. relativized relational models over the natural linear order of integers.

Product-free Lambek calculus and context-free grammars

Mati Pentus

Abstract

In this paper we prove the Chomsky Conjecture (all languages recognized by the Lambek calculus are context-free) for both the full Lambek calculus and its product-free fragment. For the latter case we present a construction of context-free grammars involving only product-free types.

Free monoid completeness of the Lambek calculus allowing empty premises

Mati Pentus

Abstract

We prove that the Lambek syntactic calculus allowing empty premises is complete with respect to the class of all free monoid models (i. e., the class of all string models, allowing the empty string).

Lambek Calculus and Formal Grammars

Mati Pentus

Abstract

We prove context-freeness of languages generated by categorial grammars based on any of the following calculi: the Lambek calculus, the Lambek calculus allowing empty premises, the Lambek calculus with the unit, the multiplicative fragment of cyclic linear logic.

We prove that all elementary fragments of the Lambek calculus have the Craig interpolation property.

We prove that the conjoinability relation (on syntactic types) is decidable and that it is complete with respect to the free group interpretation.

This is the English translation of the Ph.D. thesis of Mati Pentus.

Lambek calculus is NP-complete

Mati Pentus

Abstract

We prove that for both the Lambek calculus L and the Lambek calculus allowing empty premises L* the derivability problem is NP-complete. It follows that also for the multiplicative fragments of cyclic linear logic and noncommutative linear logic the derivability problem is NP-complete.