# Linear $\beta$-reduction

## TL;DR

This paper introduces a comprehensive analysis of linear beta-reduction at a distance in lambda-calculus, clarifying its syntactic structure and properties, and extends strong normalization proofs to this setting.

## Contribution

It provides a general notion of beta-reduction at a distance and linear reduction, along with their properties and relations, using a refined sigma-equivalence for better analysis.

## Key findings

- Defined a general notion of beta-reduction at a distance
- Analyzed relations and properties of linear reduction
- Extended strong normalization proof to linear reduction in simply typed case

## Abstract

Linear head reduction is a key tool for the analysis of reduction machines for lambda-calculus and for game semantics. Its definition requires a notion of redex at a distance named primary redex in the literature. Nevertheless, a clear and complete syntactic analysis of this rule is missing. We present here a general notion of beta-reduction at a distance and of linear reduction (i.e., not restricted to the head variable), and we analyse their relations and properties. This analysis rests on a variant of the so-called sigma-equivalence that is more suitable for the analysis of reduction machines, since the position along the spine of primary redexes is not permuted. We finally show that, in the simply typed case, the proof of strong normalisation of linear reduction can be obtained by a trivial tuning of Gandy's proof for strong normalisation of beta-reduction.