17
$\begingroup$

I wondered whether continuations, used in computer science, occur as natural and interesting mathematical structures, perhaps as algebraic (in the theory of monoids?), model-theoretic or type theoretic structures, of some kind.

Continuations as I understand them are monads (which in turn are monoids). More precisely, suppose that our monad maps types of some kind to other types. Let $\alpha, \beta$ be types and $\rightarrow$ be a mapping between types, and let $a : \alpha \hspace{0.2cm}$ (or $b: \beta)$ indicate that $a\hspace{0.2cm}$ (or $b$) is an expression of type $\alpha \hspace{0.2cm}$ (or $\beta)$. Then a continuation monad is a structure $\thinspace(\mathbb{M}, \eta, ⋆)\thinspace$, with $\eta$ the unit and ⋆ the binary operation of the monoid) such that:

$$\mathbb{M} \thinspace α = (α → ω) → ω, \hspace{1cm} ∀α$$ $$η(a) = λc. c(a) : \mathbb{M} \thinspace α \hspace{1cm} ∀a : α $$ $$m ⋆ k = λc. m (λa. k(a)(c)): \mathbb{M}\thinspace β \hspace{1cm} ∀m : \mathbb{M}\thinspace α, k : α → \mathbb{M}\thinspace β . $$

Continuation monads have been used to effect a mapping that is available in full second order logic (discussed in two previous questions on this site: Principal ultrafilters and The existence of a function between the individuals of the domain and the set of all subsets of the domain in SOL) from an individual in a domain to the principle ultrafilter containing that individual (see for example https://arxiv.org/abs/cs/0205026). In type theoretic terms we thus map an individual of type $e$ (the type of individuals) to something of type $(e → t) → t$ (the type of sets of sets), matching the original treatment of English quantification by Montague (1974).

However, I wondered whether the particular type of monad that continuations exemplify occurs in mathematical structures that mathematicians study. Perhaps there are interesting structures, for example involving ultrafilters that are examples of continuations.

The following link discusses the relation between continuations and the Yoneda embedding:

https://reperiendi.wordpress.com/2007/12/19/the-continuation-passing-transform-and-the-yoneda-embedding/

However, I would be particularly interested in examples of mathematical structures that act like continuations in fields such as algebra (perhaps in the theory of monoids?), set theory or model theory (and outside of category theory).

$\endgroup$
5
  • 2
    $\begingroup$ In any symmetric monoidally closed category, you have the adjunction $[-,R]^{op}\dashv [-,R]$ natural in $R$. The monad this induces is the "continuation" monad. For example, the category of vector spaces over a field $k$ (and generally modules over a commutative ring) is a symmetric monoidally closed category. So the above monad in the category of vector spaces over $k$ in the case where $R=k$ is the double dual monad. $\endgroup$
    – Derek Elkins left SE
    Jul 6, 2017 at 6:29
  • $\begingroup$ It would be tremendously useful to me if you could show how the vector spaces over a field k satisfy the axioms of the continuation monad. $\endgroup$
    – user65526
    Jul 6, 2017 at 7:23
  • $\begingroup$ Also, does the continuation monad with $\omega$ in the above as $\bot$ act as the embedding of classical propositional logic in to intuitionistic propositional logic? $\endgroup$
    – user65526
    Jul 6, 2017 at 15:47
  • $\begingroup$ The double negation topology is an important tool in topos theory. It yields the smallest dense subtopos of a topos, which is the "best" booleanization of a topos. In the case of a presheaf topos, the double negation topology is precisely the dense topology. In the topos-theoretic encoding of Cohen's forcing (which is used to prove the independence of the continuum hypothesis), booleanization is a key step. C.f. ncatlab.org/nlab/show/double+negation $\endgroup$
    – sclv
    Mar 17, 2018 at 0:48
  • $\begingroup$ Perhaps you could take a well-known source of values, like a natural numbers object, and dualize it? $\endgroup$
    – fhyve
    Jul 26, 2018 at 7:11

1 Answer 1

Reset to default
5
$\begingroup$

I think I've found an example. The double negation translation from the implicational fragment of Intuitionistic logic (with $\{\neg, \rightarrow\}$ as connectives) to classical logic seems to satisfy the axioms for a continuation monad.

We have

$\mathbb{M}\alpha = (a \rightarrow \bot) \rightarrow \bot$

$ \eta(a) = \lambda c_{(\alpha \rightarrow \bot) \rightarrow \bot}. c(a)$

$m * k = \lambda c. m (\lambda a. k(a)(c))$

$\eta$ maps formulas to their double negations. '*' Maps $\neg \neg A$ and $\neg \neg A \rightarrow \neg \neg B)$ to $\neg \neg B$

Still, I would prefer to have some examples outside of logic and from other parts of mathematics

$\endgroup$
2
  • 1
    $\begingroup$ This is accurate. There are a couple of such "double negation" encodings corresponding, via the Curry-Howard isomorphism, to different continuation-passing style transforms, e.g. Kolmogorov's corresponds to the call-by-name CPS transform. Which transform this leads to depends on whether you do a call-by-value or call-by-name monadic style translation. $\endgroup$
    – Derek Elkins left SE
    Jul 6, 2017 at 23:57
  • $\begingroup$ I don't fully however understand the significance of $m * k$ in the proposed translation. Could you explain it? $\endgroup$
    – user65526
    Jul 7, 2017 at 7:31

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .