Operational Semantics and Extensionality

Simona Ronchi Della Rocca

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000


In this paper the notion of extensionality is studied, for theories of variants of lambda-calculus which arise from operational semantics. A new definition of extensionality is introduced, parameterized with respect to the particular operational semantics we want to study, and it is proved that to be extensional is equivalent to be closed under a generalized eta-reduction rule. This allows to treat in an uniform way very different paradigms of computations. The examples show that this general method allows to rediscover as particular applications well known results in the literature.