Proofs as Terms, Terms as Graphs

Abstract

. Starting from an encoding of untyped λ -terms with sharing, defined using synthetic inference rules based on a focused proof system for Gentzen’s LJ , we introduce the positive λ -calculus, a call-by-value calculus with explicit substitutions. This calculus is closely related to Accattoli and Paolini’s value sub-stitution calculus but has a di ff erent style of reduction rules that provides a good notion of sharing along the reduction. We also propose a graphical representation in order to capture the structural equivalence on terms that can be described using rule permutations. On one hand, this graphical representation provides a way to remove redundancy in the syntax, and on the other hand, it allows implementing basic operations such as substitution and reduction in a straightforward way.