Classical realizability as a classifier for nondeterminism

TL;DR

This paper uses classical realizability to classify different levels of nondeterminism in computational models, establishing a hierarchy and duality with Boolean algebra structures.

Contribution

It introduces an abstract multi-evaluation relation to describe nondeterministic behaviors and links the degree of nondeterminism to Boolean algebra properties in realizability models.

Findings

Defines a hierarchy of nondeterministic computational models

Establishes a duality between Boolean algebra structure and nondeterminism

Provides a framework to classify nondeterminism using realizability

Abstract

We show how the language of Krivine's classical realizability may be used to specify various forms of nondeterminism and relate them with properties of realizability models. More specifically, we introduce an abstract notion of multi-evaluation relation which allows us to finely describe various nondeterministic behaviours. This defines a hierarchy of computational models, ordered by their degree of nondeterminism, similar to Sazonov's degrees of parallelism. What we show is a duality between the structure of the characteristic Boolean algebra of a realizability model and the degree of nondeterminism in its underlying computational model. ACM Reference Format: Guillaume Geoffroy. 2018. Classical realizability as a classifier for nondeter-minism.