Yuan (Jack) Wang: MSc, Sept. 2001.
Semantics of Non-Deterministic Programs and the Universal Function Theorem over Abstract Algebras.

Abstract. Data types containing infinite data, such as the real numbers, functions, and bit streams, can be modeled by abstract many-sorted algebras over suitable signatures. The computability theory for deterministic programs over such algebras has been studied extensively; as a complementary investigation, we study the formal semantics and computability theory for various non-deterministic languages.

The ND programming language studied in this thesis combines the While programming language extended with random assignment, and the Guarded Command Language GC of Dijkstra. A semantic theory for ND is developed following algebraic operational semantics, using semantic computation trees labeled with states instead of the computation sequences used in the deterministic case. The semantics of an ND procedure is then the set of states at all leaves of its tree, together with '↑' (the divergence symbol) if the tree has an infinite path.

Since GC has (i) finite non-determinism (i.e. the semantic computation tree for a GC statement is finitely branching), and (ii) localization of computation (i.e., the output is always in the subalgebra generated by the input), the whole computation procedure can be represented using Gödel numbering. Hence (assuming a "term evaluation property" for the given algebra) we can prove a Universal Function Theorem for GC. This technique fails for the full ND language with its infinite non-determinism and failure of localization of computation.