Call-by-name, Call-by-need, and McCarthy's Amb

This dissertation examines the behaviour of McCarthy's amb in both a call-by-name and call-by-need context. Instead of following the usual denotational approach, we choose to explore the operational alternative. The languages involved are higher-order, and contain algebraic datatypes. For both call-by-name and call-by-need we follow a simple programme:<p /> 1. Develop a number of equivalent operational semantics; one that is "obviously correct", and others that are more abstract and better suited to reasoning.<p /> 2. Define notions of cost relative to the abstract operational semantics, and use the cost-decorated operational relations to define approximation and equivalence.<p /> 3. Develop an operational theory for the approximation and equivalence.<p /> The call-by-name operational theory contains not only the expected equational laws, but also proof rules for proving properties of recursive programs containing McCarthy's amb: the cost equivalence theorem and cost equivalence induction. The theory is applied to many non-trivial examples, including stream processors, the combinators that form the basis of Fudgets. The programme is repeated for a call-by-need language containing McCarthy's amb, culminating in a context lemma for the convergent behaviour of McCarthy's amb in a call-by-need context