TY - JOUR
T1 - Geometry of interaction for mall via Hughes-van Glabbeek proof-nets
AU - Hamano, M.
N1 - Publisher Copyright:
© 2018 Association for Computing Machinery.
PY - 2018/11
Y1 - 2018/11
N2 - This article presents, for the first time, a Geometry of Interaction (GoI) interpretation inspired from Hughes-Van Glabbeek (HvG) proof-nets for multiplicative additive linear logic (MALL). Our GoI dynamically captures HvG's geometric correctness criterion-the toggling cycle condition-in terms of algebraic operators. Our new ingredient is a scalar extension of the ∗-algebra in Girard's ∗-ring of partial isometries over a Boolean polynomial ring with literals of eigenweights as indeterminates. To capture feedback arising from cuts, we construct a finer-grained execution formula. The expansion of this execution formula is longer than that for collections of slices for multiplicative GoI, hence it is harder to prove termination. Our GoI gives a dynamical, semantical account of Boolean valuations (in particular, pruning sub-proofs), conversion of weights (in particular, α-conversion), and additive (co)contraction, peculiar to additive proof-theory. Termination of our execution formula is shown to correspond to HvG's toggling criterion. The slice-wise restriction of our execution formula (by collapsing the Boolean structure) yields the well-known correspondence, explicit or implicit in previous works on multiplicative GoI, between the convergence of execution formulas and acyclicity of proof-nets. Feedback arising from the execution formula by restricting to the Boolean polynomial structure yields autonomous definability of eigenweights among cuts from the rest of the eigenweights.
AB - This article presents, for the first time, a Geometry of Interaction (GoI) interpretation inspired from Hughes-Van Glabbeek (HvG) proof-nets for multiplicative additive linear logic (MALL). Our GoI dynamically captures HvG's geometric correctness criterion-the toggling cycle condition-in terms of algebraic operators. Our new ingredient is a scalar extension of the ∗-algebra in Girard's ∗-ring of partial isometries over a Boolean polynomial ring with literals of eigenweights as indeterminates. To capture feedback arising from cuts, we construct a finer-grained execution formula. The expansion of this execution formula is longer than that for collections of slices for multiplicative GoI, hence it is harder to prove termination. Our GoI gives a dynamical, semantical account of Boolean valuations (in particular, pruning sub-proofs), conversion of weights (in particular, α-conversion), and additive (co)contraction, peculiar to additive proof-theory. Termination of our execution formula is shown to correspond to HvG's toggling criterion. The slice-wise restriction of our execution formula (by collapsing the Boolean structure) yields the well-known correspondence, explicit or implicit in previous works on multiplicative GoI, between the convergence of execution formulas and acyclicity of proof-nets. Feedback arising from the execution formula by restricting to the Boolean polynomial structure yields autonomous definability of eigenweights among cuts from the rest of the eigenweights.
UR - http://www.scopus.com/inward/record.url?scp=85057153146&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85057153146&partnerID=8YFLogxK
U2 - 10.1145/3234694
DO - 10.1145/3234694
M3 - Article
AN - SCOPUS:85057153146
SN - 1529-3785
VL - 19
JO - ACM Transactions on Computational Logic
JF - ACM Transactions on Computational Logic
IS - 4
M1 - 25
ER -