**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.