# 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.
• 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 $N$, $0$, and $s(x)$, along with a recursor $rec(n,z_0,x r. z_s)$ such that

$rec(0,z_0,x r.z_s) \Rightarrow z_0$

and

$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 $x r$ or $z_s$, or $rec$ 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,x r. z_s)$, $n$ is a term for a natural number, $z_0$ is a term of some type $Z$, and $z_s$ is a term of type $Z$ with a free variable $x$ for a natural number and a free variable $r$ of type $Z$ (where for some reason1 the presence of these free variables is indicated by writing $x r. z_s$ instead of just $z_s$). Then $rec(n,z_0,x r. z_s)$ is also a term of type $Z$.

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

• $rec(\underline{0},z_0,x r. z_s)(g) \coloneqq z_0(g)$,
• $rec(\underline{1},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{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(\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(\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, $\underline{0}$ is what Mike is simply calling $0$, and then $\underline{m+1}$ is $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,x r.z_s) \Rightarrow z_0$ and
• $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)$ then how do you know whether $r$ or $s$ (or neither) is the free variable denoting the recursive call? The notation $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 $(\lambda x. 0)\Omega$ computes to $0$, and hence has type $N$, 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,\underline{1},z_s(\underline{0},z_0))$ is not written $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_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

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

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

• CommentRowNumber34.
• CommentAuthoratmacen
• CommentTime6 days ago

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

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

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

• CommentRowNumber38.
• CommentAuthoratmacen
• CommentTime6 days ago

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

• CommentRowNumber39.
• CommentAuthoratmacen
• CommentTime6 days ago

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

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

• CommentRowNumber41.
• CommentAuthoratmacen
• CommentTime6 days ago

Perfunctory mention of type equality and hypothetical judgements.

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

• 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

• 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 $C$ when it should.

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

• CommentRowNumber52.
• CommentAuthorDavidRoberts
• CommentTime3 days ago

Thanks, Jon!