Not signed in (Sign In)

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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.

    v1, current

    • 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]

    diff, v2, current

    • CommentRowNumber4.
    • CommentAuthormaxsnew
    • CommentTimeJul 14th 2022

    Palombi and Sterling’s formulation of SGDT models

    diff, v3, current

    • 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

    diff, v3, current

    • 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.

    diff, v6, current

    • 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

    diff, v7, current

    • CommentRowNumber13.
    • CommentAuthorjonsterling
    • CommentTimeJul 15th 2022

    Add link to my bibliography of guarded domain theory

    diff, v7, current

    • 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

    diff, v7, current

    • CommentRowNumber15.
    • CommentAuthormaxsnew
    • CommentTimeAug 4th 2022

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

    diff, v8, current

    • CommentRowNumber16.
    • CommentAuthormaxsnew
    • CommentTimeAug 4th 2022

    More links

    diff, v8, current

    • CommentRowNumber17.
    • CommentAuthormaxsnew
    • CommentTimeAug 4th 2022

    Add reference for the characterization of certain metric spaces as the flabby/total objects, and change from bounded to bisected to match that reference.

    diff, v8, current

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 22nd 2022

    A fairly significant update today went unrecorded.

    diff, v9, current

    • CommentRowNumber19.
    • CommentAuthormaxsnew
    • CommentTimeNov 22nd 2022

    Clarify the role of the topos of trees model.

    diff, v15, current

    • CommentRowNumber20.
    • CommentAuthormaxsnew
    • CommentTimeNov 22nd 2022

    Wow these are great updates, but maybe one of us should alert Marco that we would appreciate if he provided updates here.

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 22nd 2022

    I’ve just notified him.

    • Added intro explaining motivations of SGDT vs SDT
    • Explanation: The topos S of trees
    • Fixed-point construction in S
    • Relation with the metric spaces expanded. Showing BiCUlt is coreflective submit of S.

    Marco Paviotti

    diff, v17, current

    • CommentRowNumber23.
    • CommentAuthormaxsnew
    • CommentTimeNov 23rd 2022

    Restore the link to flabby sheaves

    diff, v19, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)