Refining Reduction in the Lambda Calculus

Abstract

Abstract We introduce a λ-calculus notation which enables us to detect in a term, more β-redexes than in the usual notation. On this basis, we define an extended β-reduction which is yet a subrelation of conversion. The Church Rosser property holds for this extended reduction. Moreover, we show that we can transform generalised redexes into usual ones by a process called ‘term reshuffling’.