Classical notions of computation and the Hasegawa-Thielecke theorem (extended version)
Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni
TL;DR
The authors address the challenge of giving a denotational and syntactic account of classical logic with involutive negation by developing a polarised, non-associative framework based on duploids and dialogue chiralities. They build a linear L-calculus to model call-by-push-value semantics, extend it with involutive negation to obtain a linear classical L-calculus, and prove the Hasegawa-Thielecke theorem both semantically and syntactically within this setting. Central to the work is the identification of thunkable (pure/value-like) and linear maps, and the result that thunkability coincides with centrality in dialogue duploids, which ties together purity, evaluation order, and duality. The framework unifies monadic and comonadic effects, provides a semantic account of LC, and offers a robust syntactic apparatus (the syntactic dialogue duploid) for reasoning about classical notions of computation, with potential extensions to linearly distributive structures and richer control operators.
Abstract
In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear classical L-calculus. A main challenge in designing a denotational semantics for the calculus is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. In order to tackle this issue, we define a notion of adjunction between graph morphisms on non-associative categories, which we use to formulate polarized and non-associative notions of symmetric monoidal closed duploid and of dialogue duploid. We show that they provide a direct style counterpart to adjunction models: linear effect adjunctions for the (linear) call-by-push-value calculus and dialogue chiralities for linear continuations, respectively. In particular, we show that the syntax of the linear classical L-calculus can be interpreted in any dialogue duploid, and that it defines in fact a syntactic dialogue duploid. As an application, we establish, by semantic as well as syntactic means, the Hasegawa-Thielecke theorem, which states that the notions of central map and of thunkable map coincide in any dialogue duploid (in particular, for any double negation monad on a symmetric monoidal category).