TY - JOUR

T1 - A MALL geometry of interaction based on indexed linear logic

AU - Hamano, Masahiro

N1 - Publisher Copyright:
©

PY - 2020/11

Y1 - 2020/11

N2 - We construct a geometry of interaction (GoI: dynamic modelling of Gentzen-style cut elimination) for multiplicative-additive linear logic (MALL) by employing Bucciarelli-Ehrhard indexed linear logic MALL(I) to handle the additives. Our construction is an extension to the additives of the Haghverdi-Scott categorical formulation (a multiplicative GoI situation in a traced monoidal category) for Girard's original GoI 1. The indices are shown to serve not only in their original denotational level, but also at a finer grained dynamic level so that the peculiarities of additive cut elimination such as superposition, erasure of subproofs, and additive (co-) contraction can be handled with the explicit use of indices. Proofs are interpreted as indexed subsets in the category Rel, but without the explicit relational composition; instead, execution formulas are run pointwise on the interpretation at each index, with respect to symmetries of cuts, in a traced monoidal category with a reflexive object and a zero morphism. The sets of indices diminish overall when an execution formula is run, corresponding to the additive cut-elimination procedure (erasure), and allowing recovery of the relational composition. The main theorem is the invariance of the execution formulas along cut elimination so that the formulas converge to the denotations of (cut-free) proofs.

AB - We construct a geometry of interaction (GoI: dynamic modelling of Gentzen-style cut elimination) for multiplicative-additive linear logic (MALL) by employing Bucciarelli-Ehrhard indexed linear logic MALL(I) to handle the additives. Our construction is an extension to the additives of the Haghverdi-Scott categorical formulation (a multiplicative GoI situation in a traced monoidal category) for Girard's original GoI 1. The indices are shown to serve not only in their original denotational level, but also at a finer grained dynamic level so that the peculiarities of additive cut elimination such as superposition, erasure of subproofs, and additive (co-) contraction can be handled with the explicit use of indices. Proofs are interpreted as indexed subsets in the category Rel, but without the explicit relational composition; instead, execution formulas are run pointwise on the interpretation at each index, with respect to symmetries of cuts, in a traced monoidal category with a reflexive object and a zero morphism. The sets of indices diminish overall when an execution formula is run, corresponding to the additive cut-elimination procedure (erasure), and allowing recovery of the relational composition. The main theorem is the invariance of the execution formulas along cut elimination so that the formulas converge to the denotations of (cut-free) proofs.

UR - http://www.scopus.com/inward/record.url?scp=85107939175&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85107939175&partnerID=8YFLogxK

U2 - 10.1017/S0960129521000062

DO - 10.1017/S0960129521000062

M3 - Article

AN - SCOPUS:85107939175

SN - 0960-1295

VL - 30

SP - 1025

EP - 1053

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

IS - 10

ER -