Talk:Per Martin-Löf
From Wikipedia, the free encyclopedia
 |
This article is within the scope of WikiProject Biography. For more information, visit the project page. | ||
| ??? | This article has not yet received a rating on the Project's quality scale. Please rate the article and then leave a short summary here to explain the ratings and/or to identify the strengths and weaknesses of the article. [FAQ] | ||
Contents |
[edit] Comment by User:80.177.13.22
I believe that he was born in 1942, not 1943.
It is probable that he is best-known for a certain information-theoretic definition of "random sequence", published in Martin Lof, P. "The Definition of Random Sequences", Information and Control, Vol. 9, no. 6, Dec. 1966, pp. 602--619.
(Of course I agree that well-known-ness aside, the type-theory will be by far his most important contribution.)
He has also worked in statistics. There are some influential notes "Statistika Modeller" (1973), and "The notion of redundancy and its use as a quantitative measure of the discrepancy between a statistical hypothesis and a set of observational data" (Scandanavian Journal of Statistics 1974, I, 3-18.)
There is another notion of randomness due to him (1968), based on a constructive approach to measure theory, that seems to be universally ignored.
[edit] Origins of dependent types
I had thought that the first usage of dependent types in a recognisable type theory was Dana Scott's usage in Constructive Validity, which was published in 1970. Scott used a less satisfactory formulation of equality than even the extensional formulation (to my mind), but the precedence seems clear. In any case, dependent types were not all that big a discovery, since Lawvere was using very similar ideas in topos theory.
While I'm at it, Martin-Loef randomness is a worthwhile page on its own: I encountered the idea as corresponding to one of the handful of natural intermediate degrees in talks by Stephen Simpson on Mass problems. This would be well worth writing up: it's been on my to do list for too long for me to have any confidence that I will ever do it... --- Charles Stewart 13:43, 2 Jun 2005 (UTC)
[edit] Re: Origins of dependent types
Good ideas like that get discovered by several people usually as a result of some direct or indirect interaction. Hence, I wouldn't claim that Martin-Lôf was the only one who discovered dependent types. I personally think that he was the one who used them most effectively.
Btw, why do you call the meaning explanation a form of a proof-theoretic semantics, this sounds a bit contradictory to me, proof-theory is usually about form not meaning. I am just asking, your other additions are very appropriate. --Thorsten 15:04, 2 Jun 2005 (UTC)
- I agree that it was PML's ideas that really got the ball rolling with dependent types, but we have to be careful with the idea that he invented it. I have the idea that PML cited Scott's work, but it might not be in his 1971 paper, and most of my papers are the other side of the Atlantic. De Bruijn's formulation of dependent types, I think in 1974, looks to me a clearer case of reinvention.
- Check out proof-theoretic semantics for more about meaning explanations. The NJPL paper I cited discusses Prawitz's and Dummett's work: he is very much working in this strain, although he has this two-layered semantics that works rather differently to the work of the others. --- Charles Stewart 15:48, 2 Jun 2005 (UTC)
-
- Btw the influence of Dana's article on Per's work was also discussed at a seminar in Nijmegen on occassion of Per's 60th birthday. I believe by Peter Aczel, but I am not sure.--Thorsten 18:25, 2 Jun 2005 (UTC)
[edit] picture
I admit this isn't a very good one, but it is my own (maybe the two facts are corelated). Also I wanted to try out how to upload an image... If sb has got a better one (with a clear copyright situation) you are more then welcome to replace it. Btw, why doesn't my caption show up? --Thorsten 18:28, 2 Jun 2005 (UTC)
- The image markup can be a little tricky. You just had to swap "frame" for "thumb".eg, "[[Image:MartinLoef.jpg|thumb|200px|Per Martin-Löf 2004]]<nowiki>" instead of "<nowiki>[[Image:MartinLoef.jpg|frame|200px|Per Martin-Löf 2004]]". I like the photo. Its brooding. --Commander Keane 09:35, August 5, 2005 (UTC)
[edit] NPOV
Martin-Löf's work provides a continuing inspiration for logic in computer science, and it seems that the potential of his ideas hasn't yet been fully realized.
Isn't this a non-verifiable fact -- it would be better to be quoting someone influential instead?
131.111.250.149 22:04, 15 October 2005 (UTC) genneth
Good point. Any ideas, or shall I just erase the offending factoid? :-)
--Thorsten 12:52, 19 October 2005 (UTC)
