Directed virtual reductions

Abstract

This note defines a new graphical local calculus, directed virtual reductions. It is designed to compute Girard’s execution formula EX, an invariant of closed functional evaluation obtained from the “geometry of interaction” interpretation of A-calculus [5].The calculus is obtained by synchronizing another graphical local calculus presented in “local and asynchronous beta-reduction”: virtual reductions [4]. This synchronization makes it easier to mechanize than general virtual reductions. In undirected virtual reductions the consistency of the computation is insured by an algebraic mechanism called the bar. This mechanism in general induces correction terms of any order. The directed virtual reduction has been designed to keep those terms at order one.A further synchronization, the combustion strategy will even wipe out first order correction terms. Applied to sharing graphs, the combustion strategy yields Lamping’s optimal graphical calculus as presented in [1]. But more efficient optimal implementations of A-calculus are expected.The paper is conceived as a follow-up of [4] and supposes a familiarity with virtual reduction.