Not signed in (Sign In)

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 comma 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 finite foundation foundations functional-analysis functor 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 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-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 stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft 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

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeJan 17th 2023

    There might be room for argument about whether zero belongs to \mathbb{N}, but I think everyone should agree that it does belong to ω\omega.

    diff, v20, current

    • CommentRowNumber25.
    • CommentAuthorGuest
    • CommentTimeJan 17th 2023

    Are the axiomatics consistent with function extensionality?

    • CommentRowNumber26.
    • CommentAuthormaxsnew
    • CommentTimeJan 17th 2023

    Yes, in fact the axiomatics here require an elementary topos and every elementary topos satisfies function extensionality.

    • CommentRowNumber27.
    • CommentAuthorGuest
    • CommentTimeJan 17th 2023

    If every elementary topos satisfies function extensionality then why does ETCS have a separate axiom specifically for function extensionality?

    • CommentRowNumber28.
    • CommentAuthormaxsnew
    • CommentTimeJan 17th 2023

    The definition on the nlab of ETCS does not have a separate axiom for funext.

    • CommentRowNumber29.
    • CommentAuthorGuest
    • CommentTimeJan 18th 2023

    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

    • if f,g:abf, g: a \to b are morphisms such that fx=gxf x = g x for all global elements x:1ax:1 \to a, then f=gf = g;

    which is exactly the statement of function extensionality in a set theory like ETCS.

    • CommentRowNumber30.
    • CommentAuthorGuest
    • CommentTimeJan 18th 2023

    @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 1X1\to X (i.e. closed terms in the internal language) instead of arbitrary generalized elements TXT\to X (i.e. terms in a non-necessarily-empty context).

    • CommentRowNumber31.
    • CommentAuthorjonsterling
    • CommentTimeJul 19th 2023

    Fix a link to my bibliography of guarded domain theory, which I moved

    diff, v21, current