The Length of Joins in Lambek Calculus / Sorokin A.A. // Vestnik Moskovskogo Universiteta. Seriya 1. Matematika. Mekhanika. 2011. ? 3. P. 10-14 [Moscow Univ. Math. Bulletin. Vol. 66, N 3, 2011.].

In 1992, M. Pentus established a criterion for the existence of a type C such that for given types A and B the sequents A → C and B → C are derivable in the Lambek calculus. In this paper we give an algorithm for construction of such a type C (provided it exists) and prove a quadratic upper bound for its length.

Key words: Lambek calculus, free group interpretation, conjoinability, join.