scratch

§ Denotational Semantics in a Few Sentences

created 2021-08-25 · last edited 2021-12-26
  • We want to find a math object that reflects lambda calculus
  • Such an object must contain its own space of functions; L≃[L→L]L \simeq [L \to L]L≃[L→L].
  • This is impossible for cardinality constraints.
  • Key idea: restrict to continuous functions! L≃[L→contL]L \simeq [L \xrightarrow{\texttt{cont}} L]L≃[Lcont​L].
  • Solutions exist! Eg. space of continuous [N→N][\mathbb N \to \mathbb N][N→N] with appropriate topology is like space of "eventually stabilizing sequences", which is equinumerous to N\mathbb NN, since sequences that eventually become stable have information ∪i=0∞Ni\cup_{i=0}^\infty \mathbb N^i∪i=0∞​Ni. This has the same cardinality as N\mathbb NN.
  • For continuity in general, we need a topology .
  • OK, now that we know this is what we need, how do we exhibit a space L≃[L→L]L \simeq [L \to L]L≃[L→L]? One invokes the hammer of domain theory
  • Now that we have the space LLL, what's the right topology on it? That's worth a turing award! The Scott topology
❦
Newer ৪ Blog ৪ Older