Non-deterministic Effects in a Realizability Model
Niels Voorneveld · Electronic Notes in Theoretical Computer Science · 2018
We model non-deterministic effects for Turing computability by working in the assemblies of Kleene's first partial combinatory algebra. Two methods will be discussed, one using equivalence relations on trees and one using topological descriptions of powerdomains. We describe these models for a selection of non-deterministic paradigms: angelic, demonic, convex and probabilistic. Though the first approach has a connection to traditional non-deterministic computability, the second approach works better for combining non-determinism with recursion. We establish morphisms from the tree models to the powerdomain models, which are bijective at ground type and give isomorphisms for all but the demonic case. We also see that any of the powerdomain models can be interpreted as a sub-monad of a continuation monad.