One of the fundamental problems in lambda-calculi with
inductive types is the problem of relationship between intensional and
extensional equality. It is well known that the attempt to replace all
extensional (provable) equalities by conversions leads to the systems
with bad properties (no SN, undecidable type-checking etc). Our
approach is to replace only some extensional equalities (in connection
with some concrete purpose) by conversions, in such a way that SN and
CR will hold. For example, we considered reductions corresponding to
certain isomorphisms f^{-1}f=id (extensional), or equalities between
functions on finite types. In the cases we considered it was possible
to show SN and CR. In the talk some new technics that were used to show
these properties and the problems arising in different calculi will be
discussed. |