Classical notions of computation and the Hasegawa-Thielecke theorem

This paper introduces a novel approach to understanding classical computation through the lens of polarized effect calculi.

Significance and Innovations:
* Addresses a Fundamental Challenge: The paper tackles the difficulty of simultaneously accommodating call-by-value (CBV) and call-by-name (CBN) evaluation strategies within a denotational semantics, which often leads to a failure of associativity in composition.
* Dialogue Duploids: Introduces the notion of “dialogue duploid,” a non-associative and effectful counterpart to dialogue categories. This structure is crucial for interpreting the syntax of the polarized calculus.
* Syntactic Dialogue Duploid: Shows that the syntax of the polarized calculus can be interpreted within dialogue duploids and defines a syntactic dialogue duploid.
* Hasegawa-Thielecke Theorem: Establishes the Hasegawa-Thielecke theorem (equivalence of central and thunkable maps) within any dialogue duploid, including those derived from double negation monads on symmetric monoidal categories.
* Curry-Howard Correspondence: Positions the work within the spirit of the Curry-Howard correspondence, linking proofs and programs in the context of classical logic.

Key Prior Ingredients:
* Moggi’s Computational Effects: Builds upon Moggi’s work on computational effects and the tradition of using monads to interpret CBV and CBN expressions.
* Girard’s Linear Logic: Draws inspiration from Girard’s linear logic, particularly the distinction between positive and negative formulas.
* Duploids: Leverages the concept of “duploids,” introduced in prior work, as non-associative categories suitable for modeling effectful computations.
* Call-by-Push-Value: Makes use of call-by-push-value calculus.
* Dialogue Categories Makes use of dialouge categories.
* Classical L-calculus. Uses terms from the L-calculus.