In this paper we discuss usability, and propose to take that notion as a formalisation of (un)definedness in typed lambda calculus, especially in calculi based on PCF. We discuss some important properties that make usability attractive as a formalisation of (un)definedness. 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 (weak) head normal form.
|Number of pages||15|
|Publication status||Published - 1995|
|Event||Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94) - Kazimierz, Poland|
Duration: 25 Sep 1994 → 30 Sep 1994
|Conference||Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94)|
|Period||25/09/94 → 30/09/94|
|Other||25-30 September 1994|