Normalization by Evaluation for the Lambek Calculus

TL;DR

This paper develops a normalization by evaluation (NbE) method for the Lambek calculus, enabling derivation normalization through semantic evaluation in Kripke models, with potential applications to related substructural logics.

Contribution

It introduces a novel NbE-based normalization technique for Lambek calculus derivations, extending to related substructural logics with a semantic Kripke model approach.

Findings

NbE algorithm effectively normalizes Lambek calculus derivations.

Implementation requires a strong monad in Kripke semantics.

Method extends to MILL and DILL substructural logics.

Abstract

The syntactic calculus of Lambek is a deductive system for the multiplicative fragment of intuitionistic non-commutative linear logic. As a fine-grained calculus of resources, it has many applications, mostly in formal computational investigations of natural languages. This paper introduces a calculus of beta-eta-long normal forms for derivations in the Lambek calculus with multiplicative unit and conjunction among its logical connectives. Reduction to normal form follows the normalization by evaluation (NbE) strategy: (i) evaluate a derivation in a Kripke model of Lambek calculus; (ii) extract normal forms from the obtained semantic values. The implementation of the NbE algorithm requires the presence of a strong monad in the Kripke interpretation of positive formulae, in analogy with the extension of intuitionistic propositional logic with falsity and disjunction. The NbE algorithm can also be instantiated with minor variations to calculi for related substructural logics, such as multiplicative and dual intuitionistic linear logic (MILL and DILL).