In this paper we discuss usability, and propose to take that notion as aformalization of (un)definedness in typed lambda calculus. Usability can be considered as a generalization of the notion of solvability, which is widely recognized as an adequate formalization of (un)definedness in the untyped lambda calculus. Some important properties that make usability attractive as a formalization of (un)definedness, are: it has a good conceptual motivation; restricting its definition to the untyped case yields solvability; for closed terms of ground type, the unusable terms are precisely the terms without a normal form; the Genericity Lemma holds for unusable terms; and all unusable terms (of the same type, of course) can be consistently identified. This identification is maximal in the sense that additionally identifying a usable term to the unusable terms makes the calculus inconsistent. There is a remarkable difference between usability and solvability: in the untyped lambda calculus the solvable terms are precisely the terms with a head normal form, whereas in typed lambda calculus the usable terms are 'between' the terms with a normal form and the terms with a head normal form.
展开▼
