Tracking Redexes in the Lambda Calculus

Jean-Jacques Lévy

Residuals of redexes keep track of redexes along reductions in the lambda calculus. Families of redexes keep track of redexes created along these reductions. In this paper, we review these notions and their relation to a labeled λ-calculus introduced here in a systematic way. These properties may be extended to combinatory logic, term rewriting systems, process calculi and proofnets of linear logic.

https://inria.hal.science/hal-03564707/document