Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added pointer to:
Transplanted the following comment:
Martín Escardó writes on the nForum:
The usual practice of domain theory papers and talks is to start by defining “domain” for the purposes of the paper or talk. It is a reusable word. Usually only compound words using the word “domain” have a fixed meaning, such as Scott domain (bounded complete algebraic dcpo), continuous Scott domain (bounded complete continuous dcpo), FS domain, SFP domain, L-domain. I wouldn’t use the plain word “domain” in a paper without first explicitly defining it, as it has been used with so many different meanings in the domain theory literature. Also the terminological conventions vary a bit depending on whether domain theory is used for the purposes of computation (e.g., programming language semantics, and theory of computability) or topology and algebra. For example, in programming language semantics papers one often encounters posets that have sups of ascending sequences, rather than directed sets, and a least element, because all the authors are interested in is the existence of (least) fixed point of continuous endo-functions, and these assumptions are enough for this purpose. Such posets are often called domains in such papers. But for applications of domain theory to topology, directed completeness is what one needs in general, and often we have more (even all sups — for example, a topological space is exponentiable if its lattice of open sets is a continuous dcpo — but this dcpo has all sups and moreover is a distributive lattice, and the continuous distributive lattices are precisely the topologies of exponentiable spaces, up to isomorphism). Because these applications and communities are so diverse, it is natural to see a divergence of terminology, even if many of the techniques are the same.
Also, the other comment by Martín Escardó should be incorporated in the article, but I leave this to somebody more knowledgeable.
Question: Isn’t it striking that
domain theory is about regarding types as -categories;
homotopy type theory is about regarding types as -categories
?
Does anyone expand on this parallelism?
Incorporated Martin Escado’s old comment here by further expanding the lead-in paragraph (here) and adding this reference:
polished up this reference item:
touched hyperlinking and wording (here)
(We should hyperlink “intensionality” so that we know what is meant. We do have intensional type theory but I suppose this does not help in the present case.)
added publication data for this item:
1 to 12 of 12