Talk:Per Martin-Löf

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.

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)

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)

Concerning the origin of dependent types: Curry had it already in the 50's, according to this article: Jonathan Seldin. "Curry's anticipation of the types used in programming languages" (PDF). --- 130.241.53.165 (talk) 09:39, 12 August 2010 (UTC)

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)

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)

Statistics and birdwatching

His work has been very influential in statistics. I moved the material on type theory below, because it's rather technical and is last chronologically. I rated him as of high importance in philosophy and for the Sweden project, since he's probably the most influential Swedish mathematical scientist of the later half of the 20th century (I don't claim that he's stronger than Carlsson or Hörmander.). Thanks (TACK!), best regards/mvh, Kiefer.Wolfowitz (talk) 23:36, 25 February 2010 (UTC)

Thank you for extending the article, but I am actually very concerned about your de-emphasis of Martin-Löf's work in type theory. Calling it "rather technical and last chronologically" is misleading at best, since it represents his highly influential and ongoing work over the past four decades (which also makes the "In recent years" in the lede somewhat ridiculous). It's hard to judge relative importance of his early work in probability vs his early work in type theory--since both were very important. But we can at least use Google scholar as a sanity check for the tone of this article. Of Martin-Löf's top ten most cited papers, eight are in type theory, two in probability. Noamz (talk) 08:21, 27 February 2010 (UTC)

It is chronological to list bird-watching first, and then probability (licenciate and foundations) earlier than statistics. Martin-Löf's publications on statistics ceased around 1977, after which most of his publications on type theory appeared. Can we agree on that chronology?

Following your comment, I'll change "in recent years". I wrote "technical" referring to the stub-paragraph on type theory, which is rather technical---I did not intend to de-emphasize type theory. (At least my article text was clear.)

Thanks/mvh, Kiefer.Wolfowitz (talk) 19:26, 27 February 2010 (UTC)

I wrote the following text for the introduction (Kiefer.Wolfowitz (talk) 19:44, 27 February 2010 (UTC)):

Since the late 1970s, Martin-Löf's publications have been mainly in logic. In philosophical logic, Martin-Löf has wrestled with the philosophy of logical consequence and judgments, partly inspired by the work of Brentano, Frege, and Husserl. In mathematical logic, Martin-Löf has been active in developing intuitionistic type theory as a constructive foundation of mathematics; Martin-Löf's work on type theory has influenced computer science.

File:Kolmogorov-m.jpg Nominated for Deletion

An image used in this article, File:Kolmogorov-m.jpg, has been nominated for deletion at Wikimedia Commons in the following category: Deletion requests May 2012 What should I do? Don't panic; a discussion will now take place over on Commons about whether to remove the file. This gives you an opportunity to contest the deletion, although please review Commons guidelines before doing so. If the image is non-free then you may need to upload it to Wikipedia (Commons does not allow fair use) If the image isn't freely licensed and there is no fair use rationale then it cannot be uploaded or used. To take part in any discussion, or to review a more detailed deletion rationale please visit the relevant image page (File:Kolmogorov-m.jpg) This is Bot placed notification, another user has nominated/tagged the image --CommonsNotificationBot (talk) 16:13, 14 May 2012 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Per Martin-Löf. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20140202185943/http://www2.math.uu.se/PFM/ to http://www2.math.uu.se/PFM/

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 17:02, 10 September 2017 (UTC)