In this talk, I present an overview of my recent work on an intersection between algebra, logic and topology: definability and full abstraction for algebraic theories in the sense of universal algebra combined with a wellknown formal calculus for higherorder computation.
The formal calculus, known as PCF, is an extension of the simplytyped lambdacalculus, and it is Turing complete due to recursion. From the viewpoint of algebra, the combination of algebraic theories and PCF, known as algebraic effects with recursion, is of interest as it furnishes algebraic theories naturally with higherorder types/terms, (Scott) topology as well as a computational equivalence between terms. From the angle of theoretical computer science, algebraic effects (with recursion) are intriguing because they cover a large class of computational effects, e.g., partiality, nondeterminism, probability, states, and so on, systematically in terms of Lawvere theories and monads.
On the other hand, (mathematical) semantics is said to be definable if its morphisms are all the interpretations of terms in the syntax, and fully abstract if the equality between morphisms coincides with the computational equality between terms. Definability and full abstraction for algebraic effects with recursion have been wellknown open problems. My aim is to understand algebraic effects with recursion mathematically (not syntactically) by establishing definable, fully abstract semantics of them. (By the way, the present work also clarifies how arguments and proofs in mathematics, which are total, deterministic, stateless computations, can even describe theories containing partial, nondeterministic or stateful objects. I will also explain this foundational aspect if time permits.)
To this end, I employ game semantics, which is definable and fully abstract for PCF due to its unique intensionality. For extending game semantics to algebraic theories, however, the intensionality conflicts with the extensionality of algebraic theories. I overcome this dilemma by a novel categorical (and grouptheoretic) construction of topologicallyenriched monads and establish the first definability and full abstraction results for algebraic effects with recursion. The construction generalises the wellknown correspondence between Lawvere theories and finitary settheoretic monads.
