Jumping boxes representing lambda-calculus boxes by jumps

Abstract

Boxes are a key tool introduced by linear logic proof nets to implement lambda-calculus beta-reduction. In usual graph reduction, on the other hand, there is no need for boxes: the part of a shared graph that may be copied or erased is reconstructed on the fly when needed. Boxes however play a key role in controlling the reductions of nets and in the correspondence between nets and terms with explicit substitutions. We show that boxes can be represented in a simple and efficient way by adding a jump, i.e. an extra connection, for every explicit sharing position (exponential cut) in the graph, and we characterize our nets by a variant of Lamarche's correctness criterion for essential nets. The correspondence between explicit substitutions and jumps simplifies the already known correspondence between explicit substitutions and proof net exponential cuts. © 2009 Springer Berlin Heidelberg.