REALIZABILITY AND PARTIALITY IN CONSTRUCTIVE SET THEARIES

Ali A. HAMIE

The notion of realizability is associated with constructive mathematics which was original­ly developed to provide a precise constructive meaning to the logical constants. This notion has proved to be a useful technique in the area of constructive functional programming, since it can be used to extract programs from constructive proofs of their specifications.

This thesis seeks to introduce and investigate various notions of realizability in constructive theories of partiality. These theories are developed in the setting of the lambda calculus and based on different computational models reflecting different paradigms of functional pro­gramming. The logical framework of these theories is based on Beeson's (intuitionistic) logic of partial terms (LPT), Scott's (intuitionistic) logic of partial elements (LPE) and the ordinary intuitionistic predicate logic (IPL). These theories are compared and contrasted from the perspective of program development.

Variants of the realizability notion are introduced for extracting natural and elegant pro­grams, and their relationship with the ordinary notion are established by two mappings μ and σ which map the respective realizers. These mappings capture the notion of informa­tion loss from programs in a precise way. Also, we investigate the formal relationship between strict, lazy and extensional notions of realizability. The main conclusion drawn from this comparison is that the same programs are extracted from proofs.

The topic of lazy types is studied in the lazy theories of partiality. In particular, we formu­late and compare three different approaches for dealing with lazy types which may contain infinite data objects such as infinite lists.