Non-deterministic, probabilistic, and quantum effects through the lens of event structures (Technical report)

TL;DR

This paper explores event structures as a direct model for program execution traces, demonstrating their natural ability to handle non-deterministic, probabilistic, and quantum effects within an operational semantics framework.

Contribution

It introduces an imperative operational framework for event structures and establishes soundness and adequacy results, highlighting their applicability as a semantics for complex effects.

Findings

Event structures can model execution traces with non-deterministic effects

Probabilistic and quantum effects are naturally represented within event structures

Soundness and adequacy results validate event structures as a semantics for programs

Abstract

In this paper, we consider event structures and their probabilistic and quantum extensions as originally defined by Winskel. If these structures have already been part of sophisticated computational models, they have rarely been directly studied as an immediate model of execution traces of programs. This paper offers such an analysis. We propose a simple imperative operational framework and show how to derive soundness and adequacy results with event structures considered as a semantics. We show how event structures naturally handle non-deterministic, probabilistic and quantum effects.