A Classical Linear $\lambda$-Calculus based on Contraposition

TL;DR

This paper introduces a new linear lambda calculus based on classical logic, featuring contra-substitution, and proves its soundness, completeness, and desirable computational properties.

Contribution

It develops a novel lambda calculus for classical MLL using contra-substitution, extending the propositions-as-types paradigm to classical linear logic.

Findings

Proves soundness and completeness of the calculus with respect to MELL

Establishes subject reduction, confluence, and strong normalization

Shows encoding of known classical logic term assignments

Abstract

We present a novel linear $\lambda$-calculus for Classical Multiplicative Exponential Linear Logic (\MELL) along the lines of the propositions-as-types paradigm. Starting from the standard term assignment for Intuitionistic Multiplicative Linear Logic (IMLL), we observe that if we incorporate linear negation, its involutive nature implies that both $A\multimap B$ and $B^\perp\multimap A^\perp$ should have the same proofs. The introduction of a linear modus tollens rule, stating that from $B^\perp\multimap A^\perp$ and $A$ we may conclude $B$, allows one to recover classical MLL. Furthermore, a term assignment for this elimination rule, {the study of proof normalization in a $\lambda$-calculus with this elimination rule} prompts us to define the novel notion of contra-substitution $t \{ a \backslash\!\backslash s \}$. Introduced alongside linear substitution, contra-substitution denotes the term that results from "grabbing" the unique occurrence of $a$ in $t$ and "pulling" from it, in order to turn the term $t$ inside out (much like a sock) and then replacing $a$ with $s$. We call the one-sided natural deduction presentation of classical MLL, the $\lambda_{\rm MLL}$-calculus. Guided by the behavior of contra-substitution in the presence of the exponentials, we extend it to a similar presentation for MELL. We prove that this calculus is sound and complete with respect to MELL and that it satisfies the standard properties of a typed programming language: subject reduction, confluence and strong normalization. Moreover, we show that several well-known term assignments for classical logic can be encoded in $\lambda_{\rm MLL}$.