Relational type-checking for MELL proof-structures. Part 1: Multiplicatives

TL;DR

This paper introduces a linear-time algorithm for relational type-checking of proof-structures in the multiplicative fragment of linear logic, with potential extensions to larger fragments including lambda calculus.

Contribution

It presents the first linear-time decision procedure for relational type-checking in multiplicative linear logic proof-structures, advancing the understanding of semantic analysis in linear logic.

Findings

Decidable type-checking in linear time for multiplicative proof-structures

Algorithm can be extended to larger fragments with lambda calculus

Provides a semantic-based approach to proof-structure validation

Abstract

Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered. An element of the relational interpretation of a proof-structure R with conclusion $\Gamma$ acts thus as a type (refining $\Gamma$) having R as an inhabitant. We are interested in the following type-checking question: given a proof-structure R, a list of formulae $\Gamma$, and a point x in the relational interpretation of $\Gamma$, is x in the interpretation of R? This question is decidable. We present here an algorithm that decides it in time linear in the size of R, if R is a proof-structure in the multiplicative fragment of linear logic. This algorithm can be extended to larger fragments of multiplicative-exponential linear logic containing $\lambda$-calculus.