<p>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 <span class="math-container">$D$</span> needs to be, simplifying a bit, isomorphic to the function space <span class="math-container">$D \rightarrow D$</span> which is not possible set-theoretically, but turns out to be possible when you restrict your attention to computable functions).</p>
<p>Scott-continuity can be understood as a mathematically well-behaved approximation to computability.</p>
<p>[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.</p>
<hr />
<ol>
<li><p>B. A. Davey, H. A. Priestley, <em>Introduction to Lattices and Order</em>.</p>
</li>
<li><p>S. Abramsky, A. Jung, <em>Domain theory</em>, <a href="https://www.cs.bham.ac.uk/%7Eaxj/pub/papers/handy1.pdf" rel="nofollow noreferrer">https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf</a></p>
</li>
<li><p>G. Winskel, <em>The Formal Semantics of Programming Languages: An Introduction.</em></p>
</li>
</ol>

CC BY-SA 4.0
2022-06-08T10:27:13.107Z
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?
micrus
CC BY-SA 4.0
2022-06-10T09:00:25.640Z
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.
Martin Berger
CC BY-SA 4.0
2022-06-10T09:10:21.953Z
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."
Martin Berger
CC BY-SA 4.0
2022-06-10T09:25:26.257Z
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.
Martin Berger
CC BY-SA 4.0
2022-06-10T09:25:35.627Z
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).
Martin Berger
CC BY-SA 4.0
2022-06-10T09:25:44.257Z
In retrospect it turned out that Scott's idea was "kind-of" working
for simple cases (pure functions) but, even in 2022, failed to
generalise to complex, effectful computation (eg
parallelism). Nowadays we have much better tools for defining, and
reasoning about program (in-)equality. At the same time, it gave
programming language researchers a new but well-established tool-box
of mathematical methods such as category-theory, which to this day
deeply influences programming languages and programming in particular
through monads, and the concept of duality.
Martin Berger
CC BY-SA 4.0
2022-06-10T17:55:04.427Z
thank you very much for such a well structured and comprehensive answer. I accept as solved: the suggestions and recommended texts have given me a much clearer view. If you feel like you could add these comments to the answer for future readers, I think it is very consistent with the question. Thanks again!
micrus
CC BY-SA 4.0
2022-05-19T22:00:49.010Z
2022-06-10T09:19:10.950Z
2022-06-10T09:19:10.950Z
Martin Berger
<p>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.</p>
<p>I'm searching for paper that give -maybe- some application of Scott-topology in the computability field, as I have not find anything related.</p>
<p>Hoping for help from this great community</p>

CC BY-SA 4.0
2022-05-25T06:58:32.770Z
Scott-continuity is used in higher-order models of computation, in which the input of a program may be another program (by that I mean "uncoded" program, that is, a Turing machine taking as input a string encoding a Turing machine is *not* higher-order in this sense).  This is why you don't see any applications of it in general computability, which is all first-order: Turing machines, partial recursive functions, etc. take as input strings, numbers, etc., not programs in the "uncoded" sense (TMs with oracles are an exception, but there is no need for Scott-continuity for that).
Damiano Mazza
CC BY-SA 4.0
2022-06-08T10:30:53.807Z
Thanks, it help me a lot searching more information. Has the concept of Scott-continuity enrich in some way our knowledge of computability in an high order sense? Or it was only a tool needed to create a rigorous model of ho-computation?
micrus
CC BY-SA 4.0
2022-06-08T20:41:42.793Z
Yes, Scott continuity is definitely helpful in understanding higher-order computability.  Several theorems about the syntactic behavior of $\lambda$-terms were originally proved using Scott continuity (some examples: the so-called *genericity lemma* and *syntactic continuity*.  See Barendregt's book for details).  Sequentiality in the $\lambda$-calculus was also studied by means of "improved" Scott-continuous functions, called *stable functions*, introduced by Berry.  Refining those even further, Girard introduced *linear logic*, with many applications to HO programming languages.
Damiano Mazza
CC BY-SA 4.0
2022-06-10T09:49:33.700Z
@DamianoMazza Agreed that Scott's toolbox lead to a lot of innovation, including linear logic, but at the same time, I think it's fair to say that domain-theoretic methods have failed to capture the essence of many effects, in particular the parallel vs sequential distinction in its full generality.
Martin Berger
<computability><lambda-calculus><topology>
What are the application of Scott-Topology in theoretical computer science?
micrus
# What are the application of Scott-Topology in theoretical computer science?

(Asked by: username_0 on 2022-05-19)

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

**Tags:** computability, lambda-calculus, topology

> **Comments:**
> **username_1**: Scott-continuity is used in higher-order models of computation, in which the input of a program may be another program (by that I mean "uncoded" program, that is, a Turing machine taking as input a string encoding a Turing machine is *not* higher-order in this sense).  This is why you don't see any applications of it in general computability, which is all first-order: Turing machines, partial recursive functions, etc. take as input strings, numbers, etc., not programs in the "uncoded" sense (TMs with oracles are an exception, but there is no need for Scott-continuity for that).  
> **username_0**: Thanks, it help me a lot searching more information. Has the concept of Scott-continuity enrich in some way our knowledge of computability in an high order sense? Or it was only a tool needed to create a rigorous model of ho-computation?  
> **username_1**: Yes, Scott continuity is definitely helpful in understanding higher-order computability.  Several theorems about the syntactic behavior of $\lambda$-terms were originally proved using Scott continuity (some examples: the so-called *genericity lemma* and *syntactic continuity*.  See Barendregt's book for details).  Sequentiality in the $\lambda$-calculus was also studied by means of "improved" Scott-continuous functions, called *stable functions*, introduced by Berry.  Refining those even further, Girard introduced *linear logic*, with many applications to HO programming languages.  
> **username_2**: @DamianoMazza Agreed that Scott's toolbox lead to a lot of innovation, including linear logic, but at the same time, I think it's fair to say that domain-theoretic methods have failed to capture the essence of many effects, in particular the parallel vs sequential distinction in its full generality.  

---

## 1 answers

### Answer by username_2 on 2022-05-19. Score: 4 | Accepted answer

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](https://www.cs.bham.ac.uk/%7Eaxj/pub/papers/handy1.pdf)
3. G. Winskel, *The Formal Semantics of Programming Languages: An Introduction.*

> **Comments:**
> **username_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?  
> **username_2**: 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.  
> **username_2**: 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."  
> **username_2**: 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.  
> **username_2**: 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).  
> **username_2**: In retrospect it turned out that Scott's idea was "kind-of" working for simple cases (pure functions) but, even in 2022, failed to generalise to complex, effectful computation (eg parallelism). Nowadays we have much better tools for defining, and reasoning about program (in-)equality. At the same time, it gave programming language researchers a new but well-established tool-box of mathematical methods such as category-theory, which to this day deeply influences programming languages and programming in particular through monads, and the concept of duality.  
> **username_0**: thank you very much for such a well structured and comprehensive answer. I accept as solved: the suggestions and recommended texts have given me a much clearer view. If you feel like you could add these comments to the answer for future readers, I think it is very consistent with the question. Thanks again!  

---

