The formal calculus, known as PCF, is an extension of the simply-typed lambda-calculus, 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 higher-order 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 well-known 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 group-theoretic) construction of topologically-enriched monads and establish the first definability and full abstraction results for algebraic effects with recursion. The construction generalises the well-known correspondence between Lawvere theories and finitary set-theoretic monads.