A semantic account of strong normalization in Linear Logic

TL;DR

This paper presents a semantic method using relational interpretations to determine strong normalization and compute maximal reduction lengths for cut-free nets in Linear Logic.

Contribution

It introduces a novel semantic approach to analyze strong normalization and reduction lengths in Linear Logic nets, providing both decision and quantitative tools.

Findings

Can determine strong normalization of combined nets

Can compute maximal reduction length when normalized

Provides a semantic framework for analysis

Abstract

We prove that given two cut free nets of linear logic, by means of their relational interpretations one can: 1) first determine whether or not the net obtained by cutting the two nets is strongly normalizable 2) then (in case it is strongly normalizable) compute the maximal length of the reduction sequences starting from that net.