Abstract

In 1958 J. Lambek introduced a calculusL of syntactic types and defined an equivalence relation on types: x y means that there exists a sequence x=x1,...,xn=y (n 1), such thatx i x i+1 or xi+ x i (1 i n). He pointed out thatx y if and only if there is joinz such thatx z andy z. This paper gives an effective characterization of this equivalence for the Lambeck calculiL andLP, and for the multiplicative fragments of Girard's and Yetter's linear logics. Moreover, for the non-directed Lambek calculusLP 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.