7
$\begingroup$

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

Improve this question
$\endgroup$
4
  • $\begingroup$ 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). $\endgroup$
    – Damiano Mazza
    May 25, 2022 at 6:58
  • $\begingroup$ 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? $\endgroup$
    – micrus
    Jun 8, 2022 at 10:30
  • $\begingroup$ 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. $\endgroup$
    – Damiano Mazza
    Jun 8, 2022 at 20:41
  • $\begingroup$ @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. $\endgroup$
    – Martin Berger
    Jun 10, 2022 at 9:49

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
7
  • $\begingroup$ 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? $\endgroup$
    – micrus
    Jun 8, 2022 at 10:27
  • $\begingroup$ 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. $\endgroup$
    – Martin Berger
    Jun 10, 2022 at 9:00
  • $\begingroup$ 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." $\endgroup$
    – Martin Berger
    Jun 10, 2022 at 9:10
  • $\begingroup$ 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. $\endgroup$
    – Martin Berger
    Jun 10, 2022 at 9:25
  • $\begingroup$ 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). $\endgroup$
    – Martin Berger
    Jun 10, 2022 at 9:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.