The insensitivity theorem for nonreducing reflexive types

摘要

A neat line of separation between useful and useless types in applicative languages with primitive functions of finite type is established. With reference to the concept of reducing type introduced by the authors in a previous paper, a basic syntactic result is proved (the insensitivity theorem), which implies, in particular, that all nonreducing types are useless, whenever the semantics of a well-formed piece of language is defined by its behaviour as a part of programs.