# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthormaxsnew
• CommentTimeJul 14th 2022

Init page on synthetic guarded domain theory. Hope to fill this in more as I learn more about the field.

• CommentRowNumber2.
• CommentAuthormaxsnew
• CommentTimeJul 14th 2022

I’ve got an issue because the doi link has parentheses in it:

https://doi.org/10.2168/LMCS-8(4:1)2012

I tried escaping with backslashes but it doesn’t seem to work on the nlab.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJul 14th 2022

Myself, for typesetting such doi-s I fall back to using the HTML <a href=-tag:

  * [[Lars Birkedal]], Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring, _First steps in synthetic guarded domain theory: step-indexing in the topos of trees_.  Logical Methods in Computer Science **8** 4 (2012)   &lbrack;<a href="https://doi.org/10.2168/LMCS-8(4:1)2012">doi:10.2168/LMCS-8(4:1)2012</a>&rbrack;

• Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring, First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8 4 (2012) [doi:10.2168/LMCS-8(4:1)2012]
• CommentRowNumber4.
• CommentAuthormaxsnew
• CommentTimeJul 14th 2022

Palombi and Sterling’s formulation of SGDT models

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeJul 14th 2022

Is there a field called “guarded domain theory”?

If yes, it would be good to have an entry on that before going to its synthetic version.

If not, it might be better to speak of “guarded synthetic domain theory”?

• CommentRowNumber6.
• CommentAuthormaxsnew
• CommentTimeJul 14th 2022

Some type theoretic presentations

• CommentRowNumber7.
• CommentAuthormaxsnew
• CommentTimeJul 14th 2022

That’s a good question, Urs. I don’t think anyone says they do “guarded domain theory” outside of the synthetic setting. Instead, many researchers in program semantics (myself included) use the technique of “step-indexing” which would be the analytic version of the field. So if we were to make a page it would be for that.

An alternate name for the field might be “synthetic step-indexing” but SGDT is a pretty established name at this point. The name emphasizes the very similar flavor to domain theory in that it allows us to construct fixed points for recursive definitions and there are analogous constructions such as the lift monad.

• CommentRowNumber8.
• CommentAuthorjonsterling
• CommentTimeJul 14th 2022

The term to look for is “metric domain theory”, which i often refer to as guarded domain theory. I have a bibliography of this topic on my website.

• CommentRowNumber9.
• CommentAuthorjonsterling
• CommentTimeJul 14th 2022
• (edited Jul 14th 2022)

Here is an incomplete bibliography of “guarded domain theory”, which i take to include both “metric domain theory” and “synthetic guarded domain theory”. https://www.jonmsterling.com/gdt-bibliography.html

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeJul 15th 2022

Thanks for the info. Maybe you could expand the Idea-section slightly to reflect this.

Meanwhile, I have touched the entry, making some trivial edits, such as hyperlinking more of the technical terms.

This string in the entry is currently not well typeset:

$\phi : \Omega|\triangleright \phi \Rightarrow \phi \vdash \phi$

For proper scoping, there ought to be more whitespace arond the turnstile. And if the vertical bar is meant as a separator of contexts, then this too ought to have more whitespace to either context than the symbols for each context have to each other.

I am guessing that what is intended is something like

$\phi \colon \Omega \;\;|\; (\!\triangleright \phi) \Rightarrow \phi \;\;\;\;\;\vdash\;\;\;\;\; \phi$

  $\phi \colon \Omega \;\;|\; (\!\triangleright \phi) \Rightarrow \phi \;\;\;\;\;\vdash\;\;\;\;\; \phi$


i.e. “given a proposition $\phi$ in the domain whose triangleright-ification implies itself, it holds true”. But since I can’t be sure, I am not making this edit.

• CommentRowNumber11.
• CommentAuthorjonsterling
• CommentTimeJul 15th 2022

yes, you have interpreted that expression correctly. But usually the triangle thing is taken to bind tightly enough that parentheses are not required.

at some point when i have time, i can add a little more motivation to the idea section, if max doesn’t get around to it.

• CommentRowNumber12.
• CommentAuthorjonsterling
• CommentTimeJul 15th 2022

Add some more motivation and comparison with synthetic domain theory

• CommentRowNumber13.
• CommentAuthorjonsterling
• CommentTimeJul 15th 2022

• CommentRowNumber14.
• CommentAuthorjonsterling
• CommentTimeJul 15th 2022

Describe relationship between SGDT and metric spaces: flabby sheaves in the topos of trees are exactly the complete bounded ultrametric spaces

• CommentRowNumber15.
• CommentAuthormaxsnew
• CommentTime7 days ago

Change flabby sheaf to flabby object, since it’s a little confusing to mix sheaf/presheaf terminology.

• CommentRowNumber16.
• CommentAuthormaxsnew
• CommentTime7 days ago