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

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

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.

B. A. Davey, H. A. Priestley,

*Introduction to Lattices and Order*.S. Abramsky, A. Jung,

*Domain theory*, https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdfG. Winskel,

*The Formal Semantics of Programming Languages: An Introduction.*

- +0 – It takes me a long time to read the resource, thanks for point me here. For what I understand the aim of Scott (and then of the domain theory) was to create a mapping from programming languages to mathematical object in order to be able to compare them in a rigorous way. Doing this with lambda calculus they found that continuity between Scott-topologies can represent the set of computable functions. Knowing this, is there some properties that can be proved using this apporoach that couldn't be prove before? Has this enrich someway our knowledge of the calculus? — Jun 08, 2022 at 10:27
- +0 – Now that I think about it, Winskel's nice introductory book
*The Formal Semantics of Programming Languages: An Introduction*introduces Scott's approach to continuity, maybe that's the easiest way to get into the subject. — Jun 10, 2022 at 09:00 - +0 – Regarding "represent the set of computable functions", that's not quite right. Continuity is an
*approximation*to computability. "In other words, for most purposes to detect whether some construction is computationally feasible it is*sufficient*to check that it is continuous; while continuity is an algebraic condition, which is much easier to handle than computability." — Jun 10, 2022 at 09:10 - +0 – Yes, domain theory emerged as an attempt to make the mathematics of reasoning about programs, and in particular, program equality, rigorous. At the time, rather than inventing new mathematics
*ab ovo*, mapping to existing, well-understood mathematics was considered the most promising path towards mastering computing with higher-order functions. Basically, it was difficult at the time to define a canonical notion of program equality for untyped lambda-calculus (the mathematical model Scott was working with). There were many prima facie reasonable choices of equality, none of them compelling. — Jun 10, 2022 at 09:25 - +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

External links referenced by this document: