Abstract

We present a categorical/denotational semantics for the Lambek Syntactic Calculus, indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product corresponds to a noncommutative bi-endofunctor into a category, which encloses all categories of such hierarchical structure. A soundness theorem for LSC is shown with respect to this semantical framework.