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 substitution calculus but has a different 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.