Syntactic analysis of ?-expansions in Pure Type Systems
By a detailed analysis of the interaction between ?-reduction ?? and ?-expansion in the simply typed ?-calculus, a modular and purely syntactic proof method is devised in order to derive strong normalization of the combined reduction from that of ?? and . It is shown how this technique extends to ?-normalizing functional Pure Type Systems with Barthes formulation of ?-expansion.
?-expansion pure type systems strong normalization