Equivalent Types in Lambek Calculus and Linear Logic

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 = x1,..., xn = y (n ≥ 1), such that xi → xi+1 or xi+1 → xi (1 ≤ i ≤ n)”. We show that this equivalence of types is decidable for directed and non-directed Lam-bek 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.).