Tracking Redexes in the Lambda Calculus

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 chapter, we review these notions and their relation to a labeled \(\lambda \) -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.