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