Asynchronous Games 2: The True Concurrency of Innocence

摘要

In game semantics, one expresses the higher-order value passing mechanisms of the λ-calculus as sequences of atomic actions exchanged by a Player and its Opponent in the course of time. This is reminiscent of trace semantics in concurrency theory, in which a process is identified to the sequences of requests it generates. We take as working hypothesis that game semantics is, indeed, the trace semantics of the λ-calculus. This brings us to a notion of asynchronous game, inspired by Mazurkiewicz traces, which generalizes the usual notion of arena game. We then extract the true concurrency semantics of λ-terms from their interleaving semantics formulated as innocent strategies. This reveals that innocent strategies are positional strategies regulated by forward and backward interactive confluence properties. We conclude by defining a non uniform variant of the λ-calculus, whose game semantics is formulated as a trace semantics.