Algebraic totality, towards completeness

TL;DR

This paper develops a categorical model of Linear Logic using finiteness spaces and introduces an algebraic notion of totality candidates, leading to a completeness result for a typed lambda calculus with booleans and conditionals.

Contribution

It introduces an algebraic framework for totality in finiteness spaces and demonstrates completeness of a lambda calculus model based on this framework.

Findings

Finiteness spaces form a categorical model of Linear Logic.

Totality candidates are characterized as closed affine subspaces not containing 0.

The model achieves completeness for a typed lambda calculus with booleans and conditionals.

Abstract

Finiteness spaces constitute a categorical model of Linear Logic (LL) whose objects can be seen as linearly topologised spaces, (a class of topological vector spaces introduced by Lefschetz in 1942) and morphisms as continuous linear maps. First, we recall definitions of finiteness spaces and describe their basic properties deduced from the general theory of linearly topologised spaces. Then we give an interpretation of LL based on linear algebra. Second, thanks to separation properties, we can introduce an algebraic notion of totality candidate in the framework of linearly topologised spaces: a totality candidate is a closed affine subspace which does not contain 0. We show that finiteness spaces with totality candidates constitute a model of classical LL. Finally, we give a barycentric simply typed lambda-calculus, with booleans ${\mathcal{B}}$ and a conditional operator, which can be interpreted in this model. We prove completeness at type ${\mathcal{B}}^n\to{\mathcal{B}}$ for every n by an algebraic method.