Normalization and extensionality

An investigation on the interaction between β-reduction and η-expansion is provided in a labelled λ-calculus, where additional information, that is constituted by integers, can be considered as a type in an abstract sense. This leads to propose the splitting of the β-rule into two parts: a restricted β-rule (β⁺), strongly normalizing, and a reversed η-rule (η^-), which comes out to have different computational interpretations for reduction in untyped and typed calculi (static and dynamic allocation of computation resources, respectively). To motivate the opportunity of this splitting, the paper hints to new proofs of strong normalization theorems for some typed λ-calculi in Curry style