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-categories 2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology combinatorics complex-geometry computable-mathematics computer-science connection constructive constructive-mathematics cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality education elliptic-cohomology enriched fibration foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus graph graphs gravity grothendieck 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 kan lie lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories newpage noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar 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-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.
    • CommentAuthorMike Shulman
    • CommentTimeNov 30th 2012

    I wrote something at meaning explanation, but I didn’t add any links to it yet because I’m hoping to get some feedback from type theorists as to its correctness (or lack thereof).

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 30th 2012

    After you get feedback from the experts, I hope you can sprinkle some sugar on the section on natural numbers. I have trouble understanding what the first sentence is about.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeNov 30th 2012

    It’s expressing an assumption about the untyped computational objects with which we began. I’m not sure how to clarify it, can you suggest something?

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 30th 2012

    Let me reproduce it so that I can refer to it:

    Suppose that we have terms NN, 00, and s(x)s(x), along with a recursor rec(n,z 0,xr.z s)rec(n,z_0,x r. z_s) such that

    rec(0,z 0,xr.z s)z 0rec(0,z_0,x r.z_s) \Rightarrow z_0

    and

    rec(s(n),z 0,xr.z s)z s[n/x,rec(n,z 0,xr.z s)/r].rec(s(n),z_0,x r. z_s) \Rightarrow z_s[n/x,rec(n,z_0,x r.z_s)/r].

    In plain English, can you explain what this recursor is supposed to mean? I don’t know what xrx r or z sz_s, or recrec for that matter, signify. (Sorry, I do realize it’s probably a dumb question.)

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeNov 30th 2012
    • (edited Dec 3rd 2012)

    In rec(n,z 0,xr.z s)rec(n,z_0,x r. z_s), nn is a term for a natural number, z 0z_0 is a term of some type ZZ, and z sz_s is a term of type ZZ with a free variable xx for a natural number and a free variable rr of type ZZ (where for some reason1 the presence of these free variables is indicated by writing xr.z sx r. z_s instead of just z sz_s). Then rec(n,z 0,xr.z s)rec(n,z_0,x r. z_s) is also a term of type ZZ.

    In categorial semantics, think of nn as a generalised element of a natural-numbers type NN, so a map ΓN\Gamma \to N. Then z 0:ΓZz_0\colon \Gamma \to Z and z s:Γ×N×ZZz_s\colon \Gamma \times N \times Z \to Z, and rec(n,z 0,xr.z s):ΓZrec(n,z_0,x r. z_s)\colon \Gamma \to Z. Supposing that the term nn is a canonical numeral m̲\underline{m}, we may express the first few rec(n,z 0,xr.z s):ΓZrec(n,z_0,x r. z_s)\colon \Gamma \to Z as follows:

    • rec(0̲,z 0,xr.z s)(g)z 0(g)rec(\underline{0},z_0,x r. z_s)(g) \coloneqq z_0(g),
    • rec(1̲,z 0,xr.z s)(g)z s(g,0̲,z 0)rec(\underline{1},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{0},z_0),
    • rec(2̲,z 0,xr.z s)(g)z s(g,1̲,z s(g,0̲,z 0))rec(\underline{2},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{1},z_s(g,\underline{0},z_0)),
    • rec(3̲,z 0,xr.z s)(g)z s(g,2̲,z s(g,1̲,z s(g,0̲,z 0)))rec(\underline{3},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{2},z_s(g,\underline{1},z_s(g,\underline{0},z_0))),
    • etc.

    After the first line, these follow from a general rule:

    • rec(m+1̲,z 0,xr.z s)(g)z s(g,m̲,rec(m̲,z 0,xr.z s)(g))rec(\underline{m+1},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{m},rec(\underline{m},z_0,x r. z_s)(g)).

    Of course, 0̲\underline{0} is what Mike is simply calling 00, and then m+1̲\underline{m+1} is s(m̲)s(\underline{m}). So writing these two rules properly in type theory as beta-reductions, we have these rules of Mike’s:

    • rec(0,z 0,xr.z s)z 0rec(0,z_0,x r.z_s) \Rightarrow z_0 and
    • rec(s(n),z 0,xr.z s)z s[n/x,rec(n,z 0,xr.z s)/r]rec(s(n),z_0,x r. z_s) \Rightarrow z_s[n/x,rec(n,z_0,x r.z_s)/r]

    (where for some reason2 reduction is written as \Rightarrow instead of as \rightsquigarrow).


    1. I write this before reading Mike's article, so there might be a good reason. 

    2. I doubt that there’s a good reason for this; \Rightarrow is overloaded enough as it is. 

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 1st 2012

    Ah, thanks Toby! That makes it very clear.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeDec 1st 2012

    Thanks very much, Toby. The only caveat I would add is that in the context of the meaning explanation, phrases like “of some type Z” should be omitted. My understanding is that in this case, we start with some raw untyped notion of computation and then consider how we might assign types to its objects.

    Re: your first footnote, I think it’s important to denote all variable bindings somehow. If you just write (say) rec(0,4,r+s)rec(0,4,r+s) then how do you know whether rr or ss (or neither) is the free variable denoting the recursive call? The notation rec(0,4,xr.r+s)rec(0,4,x r.r+s) makes it clear.

    Re: your second footnote, I was just copying what Peter Dybjer used in his talk today. Feel free to change it to \rightsquigarrow if you prefer.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeDec 2nd 2012
    • (edited Dec 2nd 2012)

    Hm, looking at the entry meaning explanation, I get away with the impression that all it says is that

    “If something computes to something that behaves like a certain type, then it is of that certain type”.

    What is there more to it? What is non-trivial in saying this for various examples of types?

    Sorry, I suppose this means that I missed the main point of “meaning explanation”. But maybe that point could be made more explicitly. (?)

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeDec 2nd 2012

    One thing that I guess is worth mentioning is that since you start from an untyped notion of computation, there are more terms assigned to a type than in the usual rules of type theory. For instance, maybe (λx.0)Ω(\lambda x. 0)\Omega computes to 00, and hence has type NN, regardless of whether Ω\Omega is even well-typed.

    However, you’re not the only one who is confused about the point of this. I’m in the middle of a discussion with Peter Dybjer and Bob Harper about it; so far I gather that it is regarded as a “pre-mathematical” or “philosophical” explanation of why the rules of type theory are what they are. I don’t really get the point either, though.

  1. To me it is not clear why z s(g,1̲,z s(0̲,z 0))z_s(g,\underline{1},z_s(\underline{0},z_0)) is not written z s(g,1̲,z s(g,0̲,z 0))z_s(g,\underline{1},z_s(g,\underline{0},z_0)).

    • CommentRowNumber11.
    • CommentAuthorjcmckeown
    • CommentTimeDec 3rd 2012

    @Stephen: Probably because Toby is a real human; or else the program playing Toby has a subtle fencepost error.

  2. subtle fencepost error

    Oh, I expected a subtle meaning - or rather a subtle meaning explanation.:)

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 3rd 2012
    • (edited Dec 3rd 2012)

    On p. 25 here Peter Dybjer paraphrases Martin-Löf as saying

    Some people feel that when I have presented my meaning explanations I have said nothing. And this is how it should be. The standard semantics should be just that: standard. It should come as no surprise.

    ( Martin-Löf at the Types Summer School in Giens 2002 (as I [Peter Dybjer] recall it) )

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeDec 3rd 2012

    I added that quote, and clarified the natural numbers type. I think the conclusion of my discussions with the type theorists is that there is a mathematical component, which can be regarded as a realizability model, and then also a philosophical component, which I don’t understand and probably never will.

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeDec 3rd 2012

    Or the program implementing me (I would not say ‘playing’) has subtle errors deliberately introduced to help pass Turing tests.

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeDec 3rd 2012

    @Mike #7 re first footnote #5: Normally I see people say things like ‹Let z sz_s be a term (of this type) with these free variables (of these types).›; but in this raw context, I agree that (besides not specifying the types ahead of time) it’s nice to put it all directly into the syntax.

    • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeDec 3rd 2012

    I moved the page back to a singular name, in accordance with the naming conventions, but the text still refers to multiple meaning explanations.

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 3rd 2016

    I just read the email discussion linked to at uf-ias-2012, and find myself perfectly in agreement with Mike. A view of philosophy which would pin down one correct way of seeing things is so enormously implausible in the context of the long course of human inquiry. I’d much rather it make its contribution by providing occasional fresh insights to be fed into the mix. On the other hand, I suppose some people wouldn’t be motivated to do their work if they didn’t believe they were on the one true path.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMay 3rd 2016

    Rereading that email discussion again myself, I find myself astonished at how much energy and time I had for conversations like that three years ago. (-:

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 3rd 2016

    Just see yourself as playing the role of Hilbert in the Hilbert-Frege (or Brouwer or Weyl) discussions. If he thought it worth the energy and time, why not you?

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeMay 3rd 2016

    Whether it’s worth the energy and time is a different question from whether I have that energy and time available… (-:

    • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 4th 2016

    I see the search continues for a meaning explanation of higher type theory, in arXiv:1604.08873, and then a constructive understanding of univalence in Cubical Type Theory: a constructive interpretation of the univalence axiom.

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 16th 2017

    I added

    • Jonathan Sterling, Type theory and its meaning explanations, (pdf)
    • CommentRowNumber24.
    • CommentAuthorjonsterling
    • CommentTimeOct 16th 2017

    I would like to propose that we remove the link to the video of my talk, “Type theory and its meaning explanations”; the talk contains a serious error in the definition of ‘functionality’/sequents, which is corrected in the notes that David has just added.

    Are people OK with that?

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeOct 16th 2017

    If you prefer you should remove it. But might the topic better be served if you leave it there and add a quick remark to the link regarding the error and how to fix it?

    • CommentRowNumber26.
    • CommentAuthorjonsterling
    • CommentTimeOct 16th 2017
    • (edited Oct 16th 2017)

    Hi Urs, I have just added a note to that link saying that the explanation of functionality is incorrect, but that it is fixed in the notes that are also linked.

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeOct 17th 2017

    Thanks. I have edited the formatting slightly: here

    • CommentRowNumber28.
    • CommentAuthorjonsterling
    • CommentTimeOct 17th 2017

    Thank you, Urs!

    • CommentRowNumber29.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 17th 2017

    I changed the YouTube link to point to just Jon’s video, rather than including also the playlist information that was in the previous link.

    • CommentRowNumber30.
    • CommentAuthoratmacen
    • CommentTime7 days ago
    Say, this explanation of function types isn’t right is it? It’s not enforcing that they respect equality.
    • CommentRowNumber31.
    • CommentAuthorjonsterling
    • CommentTime7 days ago

    Yes, the explanation of function types seems incorrect. I’m having trouble reading it because the changes to the style changes have resulted in some bizarre effects (gigantic text mixed with small text, all very closely spaced together), but from what I can tell, the definitions in the page need a lot of corrections. If I were not stuck between a bunch of deadlines right now, I would make some corrective changes to the page.

    • CommentRowNumber32.
    • CommentAuthoratmacen
    • CommentTime7 days ago

    Well, I think I fixed the issue of functions respecting equality, anyway.

    diff, v19, current

    • CommentRowNumber33.
    • CommentAuthoratmacen
    • CommentTime7 days ago

    Changes to wording that I think are less misleading. For example: “equal terms” -> “equal elements”; certainly they need not be syntactically equal.

    diff, v20, current

    • CommentRowNumber34.
    • CommentAuthoratmacen
    • CommentTime6 days ago

    Clarified the way the inductive judgments for Nat elements are separate from the overall induction-recursion.

    diff, v21, current

    • CommentRowNumber35.
    • CommentAuthorDavidRoberts
    • CommentTime6 days ago

    @Jon

    should the link to your meaning explanations notes (which is broken, and the pdf doesn’t appear to be in your GH repo for your webpage) point to https://arxiv.org/abs/1512.01837?

    • CommentRowNumber36.
    • CommentAuthoratmacen
    • CommentTime6 days ago

    Clarification about what aspects of the explanation for identity types gets UIP vs equality reflection.

    diff, v22, current

    • CommentRowNumber37.
    • CommentAuthoratmacen
    • CommentTime6 days ago

    Corrections to reduction rules. This is big-step reduction; you need premises. There should probably be a section explaining the operational setup.

    diff, v23, current

    • CommentRowNumber38.
    • CommentAuthoratmacen
    • CommentTime6 days ago

    Put in some stuff about properties this meaning explanation should satisfy and why.

    diff, v24, current

    • CommentRowNumber39.
    • CommentAuthoratmacen
    • CommentTime6 days ago

    Updated/rearranged pedagogical commentary about why this is mutual inductive-recursive.

    diff, v25, current

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTime6 days ago
    • (edited 6 days ago)

    made more of the keywords in the first sentences be hyperlinked

    diff, v26, current

    • CommentRowNumber41.
    • CommentAuthoratmacen
    • CommentTime6 days ago

    Perfunctory mention of type equality and hypothetical judgements.

    diff, v27, current

    • CommentRowNumber42.
    • CommentAuthorjonsterling
    • CommentTime5 days ago

    Hi all, I wanted to remove the links to my presentation and notes from this page, but I felt I should consult the forum.

    I don’t feel that the notes are in bad shape in a technical sense, but I no longer subscribe to the point of view which I was expressing in those notes, and feel that it might be misleading to people who reach them from this page. The technical material in the note is of course correct and fine as far as I am aware, but the ethos is a bit odious. Can we let other references, such as the works of Per, stand for themselves?

    • CommentRowNumber43.
    • CommentAuthorDavidRoberts
    • CommentTime5 days ago

    Sure, but I think the video has some merit despite the mistake, in that I’ve not seen another presentation on it in that style I found it helpful.

    • CommentRowNumber44.
    • CommentAuthorjonsterling
    • CommentTime4 days ago
    • (edited 4 days ago)

    Hi David, thank you for your comment! By the way, I am too concerned about the error in the presentation, because it is corrected in the notes — my main concern is that the ethos presented is naive and may lead people down an unnecessary rabbit hole. I wish I could say more at the moment, but let me be a bit mysterious and say that after spending a lot of time working on it, I am skeptical of the notion of ’meaning explanation’ as a scientific discipline which can tell the difference between correct and incorrect versions of type theory. I felt I was a bit overzealous in promoting it, and perhaps made stronger claims than Per intended in his own work.

    • CommentRowNumber45.
    • CommentAuthorDavidRoberts
    • CommentTime4 days ago
    • (edited 4 days ago)

    Ah, ok. I should go have a (re)read of Martin-Löf’s original treatment. Is the referenced article (“Constructive mathematics and computer programming”) the only place?

    Also, the link to the IAS special year wiki needs updating!

    • CommentRowNumber46.
    • CommentAuthorDavidRoberts
    • CommentTime4 days ago

    Updated the link to the IAS2012 wiki to point to the archived version, and added reference to Martin-Löf’s On the Meanings of the Logical Constants and the Justifications of the Logical Laws.

    diff, v28, current

    • CommentRowNumber47.
    • CommentAuthorjonsterling
    • CommentTime4 days ago

    Hi David, Per has also propounded the meaning explanation of his type theory in his subsequent monograph, Intuitionistic Type Theory (what some call the “Bibliopolis book”): http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf

    • CommentRowNumber48.
    • CommentAuthorDavidRoberts
    • CommentTime4 days ago

    @Jon,

    thanks, I’ve added it. Some words around how these different texts relate would be good, but I’m not confident in getting it right, since I know there are subtle changes over time in Martin-Löf’s work.

    • CommentRowNumber49.
    • CommentAuthorDavidRoberts
    • CommentTime4 days ago

    Added the Bibliopolis book reference

    diff, v29, current

    • CommentRowNumber50.
    • CommentAuthoratmacen
    • CommentTime4 days ago
    • (edited 3 days ago)

    Justification for my weird reflexivity property. Discussion of how this function type differs from Martin-Löf’s. Finally noticed mistake where the function type clause didn’t use CC when it should.

    diff, v30, current

    • CommentRowNumber51.
    • CommentAuthorjonsterling
    • CommentTime3 days ago

    Removed the links to my notes & presentation, as I proposed in the n-forum thread. At some point within the next month or so, I also intend to update this page with a brief map to through the literature — as PML’s views on the topic have evolved, and without a guide, it can be hard to understand the history of these ideas.

    diff, v31, current

    • CommentRowNumber52.
    • CommentAuthorDavidRoberts
    • CommentTime3 days ago

    Thanks, Jon!

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)