  We construct a geometry of interaction (GoI: dynamic modeling 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, w.r.t 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.
