Functional Programming and Erratic Non-Determinism
Corin Pitcher, C.-H. Luke Ong, Lincoln A. Wallen · 2001
Non-deterministic programs can represent specifications, and non-determinism arises naturally in concurrent programming languages. In this dissertation, λ-calculi exhibiting erratic nondeterminism are studied in order to identify definitions and techniques that may be applicable to higher-order programming languages for specification or concurrency. The non-deterministic λ-calculi arise as fragments of an infinitary, non-deterministic λ-calculus L with countably indexed erratic choice. The operational semantics for L induces a uniform operational semantics upon each fragment, facilitating arguments that apply to different nondeterministic λ-calculi. The behaviour of programs in each fragment is abstracted to a form of labelled transition system with divergence called a typed transition system. Several applicative similarity and bisimilarity relations are defined upon the states of each typed transition system, including the fragments. Examples that distinguish the relations are constructed in a simple typed transition system S and are later shown to have analogues in non-deterministic λ-calculi. Maps that preserve and reflect the structure of typed transition systems are investigated because they reflect the finest relation, convex bisimilarity, and it is proven that there is a map to S from every typed transition system satisfying a mild condition. Using operational techniques, the lower, upper, and convex variants of similarity are shown to be compatible and to satisfy the Scott induction principle for every fragment. In addition, the other relations are compatible for a useful collection of fragments. Relative definability of non-deterministic programs is considered with respect to convex bisimilarity, and a chain of fragments is presented for which the corresponding chain of convex bisimilarity relations are related by strict inclusions, i.e., more expressive forms of erratic non-determinism distinguish terms that cannot be distinguished by less expressive forms of erratic non-determinism.