Theoretical Computer Science
computability lambda-calculus topology
Updated Thu, 23 Jun 2022 17:19:57 GMT

What are the application of Scott-Topology in theoretical computer science?

During a work I came across the Scott-Topology and I see that Scott-continuous functions show up in the study of models for lambda calculi. What I cannot understand is how this enrich the lambda-calculus as we know.

I'm searching for paper that give -maybe- some application of Scott-topology in the computability field, as I have not find anything related.

Hoping for help from this great community

Solution

Scott-continuity emerged when Dana Scott build the first model of untyped -calculus, while trying to prove that no such model can exist (since any such model $$D$$ needs to be, simplifying a bit, isomorphic to the function space $$D \rightarrow D$$ which is not possible set-theoretically, but turns out to be possible when you restrict your attention to computable functions).

Scott-continuity can be understood as a mathematically well-behaved approximation to computability.

[1] is a gentle introduction to the general area of order theory that Scott continuity emerged out of, and [2] is a reference article. [3] has a bit on domain-theory and Scott-continuity and might be the easiest introduction for computer scientists.

1. B. A. Davey, H. A. Priestley, Introduction to Lattices and Order.

2. S. Abramsky, A. Jung, Domain theory, https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf

3. G. Winskel, The Formal Semantics of Programming Languages: An Introduction.

• +0 – As to "what could not be proved before". I would say that in some sense nothing could be proven at the time, because the right definitions were missing. We could not prove/disprove that two $\lambda$-terms were equal, because we had no compelling definition of this equality. Scott's model of the $\lambda$-calculus gave his definitions legitimacy, because they proved stable in a highly non-trivial use case. In a different tradition, there was of course Hoare-logic, but in the 1960s it was unknown how to extend it to $\lambda$-calculi (this was only settled in the early 2000s). — Jun 10, 2022 at 09:25