Denotational semantics driven simplicial homology?

TL;DR

This paper explores a novel geometric perspective on Linear Logic proofs using simplicial homology, investigating how proof interpretations form complex spaces and how their homological properties relate to logical invariance and transformations.

Contribution

It introduces a new approach to interpreting Linear Logic proofs as simplicial complexes and examines the invariance of their homology under certain transformations, linking geometry with logic.

Findings

Proof interpretations form abstract simplicial complexes.

Homology invariance depends on the type of transformations considered.

Using a monad-based approach alters the homology of the space, raising questions about invariance.

Abstract

We look at the proofs of a fragment of Linear Logic as a whole: in fact, Linear Logic's coherent semantics interprets the proofs of a given formula $A$ as faces of an abstract simplicial complex, thus allowing us to see the set of the (interpretations of the) proofs of $A$ as a geometrical space, not just a set. This point of view has never been really investigated. For a ``webbed'' denotational semantics -- say the relational one --, it suffices to down-close the set of (the interpretations of the) proofs of $A$ in order to give rise to an abstract simplicial complex whose faces do correspond to proofs of $A$. Since this space comes triangulated by construction, a natural geometrical property to consider is its homology. However, we immediately stumble on a problem: if we want the homology to be invariant w.r.t. to some notion of type-isomorphism, we are naturally led to consider the homology functor acting, at the level of morphisms, on ``simplicial relations'' rather than simplicial maps as one does in topology. The task of defining the homology functor on this modified category can be achieved by considering a very simple monad, which is almost the same as the power-set monad; but, doing so, we end up considering not anymore the homology of the original space, but rather of its transformation under the action of the monad. Does this transformation keep the homology invariant ? Is this transformation meaningful from a geometrical or logical/computational point of view ?