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 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).
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.
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?
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.)
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 reason^{1} 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:
After the first line, these follow from a general rule:
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:
(where for some reason^{2} reduction is written as $\Rightarrow$ instead of as $\rightsquigarrow$).
Ah, thanks Toby! That makes it very clear.
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.
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. (?)
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.
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))$.
@Stephen: Probably because Toby is a real human; or else the program playing Toby has a subtle fencepost error.
subtle fencepost error
Oh, I expected a subtle meaning - or rather a subtle meaning explanation.:)
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) )
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.
Or the program implementing me (I would not say ‘playing’) has subtle errors deliberately introduced to help pass Turing tests.
@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.
I moved the page back to a singular name, in accordance with the naming conventions, but the text still refers to multiple meaning explanations.
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.
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. (-:
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?
Whether it’s worth the energy and time is a different question from whether I have that energy and time available… (-:
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.
I added
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?
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?
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.
Thanks. I have edited the formatting slightly: here
Thank you, Urs!
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.
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.
@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?
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?
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.
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.
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!
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
@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.
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.
Thanks, Jon!
1 to 52 of 52