7
$\begingroup$

I read the following excerpt from nLab but I need further explanation:

The problem Scott solved is to faithfully model untyped lambda calculus; in categorical terms, the basic problem is to construct a cartesian closed category with just one object $D$ (or rather, two objects: $D$ and a terminal object $1$), so that $D$ is closed under formation of products and function spaces: $D \cong D \times D$ and $D \cong D \Rightarrow D$. Notice that in the category of sets, the only solution is to take $D \cong 1$, so that all terms are then equal (“algorithmic inconsistency”). This is not a faithful modeling of untyped lambda calculus, which has provably unequal terms.

In 1969, Dana Scott solved this problem topologically: the terms were interpreted as continuous functions on a suitable space $D$ isomorphic to its own function space. This $D$ is called a domain. Decades later, we now know many techniques for constructing such domains as suitable objects in cartesian closed categories, but Scott’s basic insight, that computability could be interpreted as continuity, continues to exert a decisive influence today.

Exactly, how does continuity resolve the issue that the category of $Set$ cannot solve? Namely, by Cantor's theorem a set cannot be equal to its power set. But I don't understand why continuity can bypass this issue... thanks.

$\endgroup$
9
  • $\begingroup$ The question in your title and the question in the body are totally different. Which question are you asking? Cartesian-closure is neither necessary nor sufficient for a category to be a model of the untyped lambda calculus. $\endgroup$ Sep 27, 2017 at 18:05
  • 1
    $\begingroup$ Cantor's theorem imlies that if a set, $X$, has at least two elements then $|X^X|\neq|X|$, but continuous functions $X\to X$ are a subset of $X^X$, so the set of continuous functions $X\to X$ can certainly have lower cardinality than $X^X$ $\endgroup$ Sep 27, 2017 at 18:10
  • 1
    $\begingroup$ Cartesian closure implies more structure than is needed to model the untyped lambda calculus. In particular, we can view the untyped lambda calculus as a simply typed lambda calculus with one type. Then we normally say the STLC is the internal language of CCCs, but this isn't quite true. Instead, the STLC with products is the internal language of CCCs. Bart Jacobs in "Simply Typed and Untyped Lambda Calculus Revisited" makes a tighter connection. That said, examples will typically be CCCs and CCCs are certainly simpler to formalize. $\endgroup$ Sep 29, 2017 at 3:43
  • 1
    $\begingroup$ $\mathbf{Top}$, the category of topological spaces and continuous functions, is not cartesian closed. My comments with regards to Cantor's theorem were simply to indicate that adding the requirements of continuity means Cantor's theorem doesn't a priori apply and that it's possible it could fail. It still takes a bit of work to find a category with a (non-degenerate) reflexive object, i.e. one with $X\cong X^X$ that supports the desired operation and equalities. $\endgroup$ Sep 29, 2017 at 3:43
  • 1
    $\begingroup$ Cartesian closed categories don't necessarily (or even usually) have a subobject classifier. CCC+subobject classifier is almost a topos (you just need to add equalizers). $\endgroup$ Sep 29, 2017 at 7:47

0

You must log in to answer this question.

Browse other questions tagged .