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.
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.
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) [<a href="https://doi.org/10.2168/LMCS-8(4:1)2012">doi:10.2168/LMCS-8(4:1)2012</a>]
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”?
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.
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.
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
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:
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$
i.e. “given a proposition in the domain whose triangleright-ification implies itself, it holds true”. But since I can’t be sure, I am not making this edit.
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.
Wow these are great updates, but maybe one of us should alert Marco that we would appreciate if he provided updates here.
I’ve just notified him.
Are the axiomatics consistent with function extensionality?
Yes, in fact the axiomatics here require an elementary topos and every elementary topos satisfies function extensionality.
If every elementary topos satisfies function extensionality then why does ETCS have a separate axiom specifically for function extensionality?
The definition on the nlab of ETCS does not have a separate axiom for funext.
Yes it does, it’s part of the characterization of ETCS as a well-pointed topos. The definition of a topos as a well-pointed topos states that
which is exactly the statement of function extensionality in a set theory like ETCS.
@Guest 29: The well-pointedness of a topos is not function extensionality (which is built in to the definition of exponential object); it states that equality of functions can be checked with global elements (i.e. closed terms in the internal language) instead of arbitrary generalized elements (i.e. terms in a non-necessarily-empty context).
1 to 31 of 31