Weak Typed Boehm Theorem on IMLL

TL;DR

This paper proves a weak typed Boehm theorem for a fragment of intuitionistic linear logic, specifically IMLL, establishing a syntactical separation result in this setting.

Contribution

It demonstrates the validity of the weak typed Boehm theorem within the multiplicative fragment of IMLL, a novel syntactical separation result for these systems.

Findings

Weak typed Boehm theorem holds in IMLL fragment

First syntactical separation result for these systems

Characterizes IMLL as linear lambda calculus without exponentials

Abstract

In the Boehm theorem workshop on Crete island, Zoran Petric called Statman's ``Typical Ambiguity theorem'' typed Boehm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus. In this paper, we study the linear version of the typed Boehm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit 1 (for short IMLL) weak typed Boehm theorem holds. The system IMLL exactly corresponds to the linear lambda calculus without exponentials, additives and logical constants. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner.