Refining reduction in the lambda calculus

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’.