هذه المقالة يتيمة. ساعد بإضافة وصلة إليها في مقالة متعلقة بها

بير مارتن لوف

من أرابيكا، الموسوعة الحرة
اذهب إلى التنقل اذهب إلى البحث
بير مارتن لوف
معلومات شخصية

بير إريك روتغر مارتن لوف (من موالين 8 مايو 1942)، هو منطقي سويدي وفيلسوف وإحصائي رياضي،[1] وهو مشهور دوليًا بعمله في أسس الاحتمالات والإحصاء والمنطق الرياضي وعلوم الحاسوب. منذ أواخر السبعينيات، كانت منشورات مارتن لوف مركزة حول المنطق. في المنطق الفلسفي، تعامل مارتن لوف مع فلسفة الاستتباع المنطقي والحكم مستلهمًا بأعمال برنتانو وفريجه وهوسرل. في المنطق الرياضي، كان مارتن لوف نشطًا في تطوير نظرية النمط الحدسي كأساس بناء للرياضيات. أثر عمل مارتن لوف على نظرية النمط في علوم الحاسوب.[2]

حتى تقاعده في عام 2009، شغل بير مارتن لوف كرسيًا مشتركًا للرياضيات والفلسفة في جامعة ستوكهولم.

شقيقه أندرس مارتن لوف هو الآن أستاذ فخري للإحصاء الرياضي في جامعة ستوكهولم.[3] تعاون الأخوان في البحث في الاحتمالات والإحصاء. أثر بحث أندريه وبير مارتن لوف على النظرية الإحصائية، خاصةً فيما يتعلق بالعوائل الأسية وطريقة تحقيق أقصى قدر لتوقع البيانات المفقودة واختيار النموذج.[4]

يراقب بير مارتن لوف الطيور بحماسة، وأول منشور علمي له كان حول معدلات وفيات الطيور المُطوَّقة.[5]

منطقه

المنطق الفلسفي

في المنطق الفلسفي، نشر بير مارتن لوف أوراقًا حول نظرية الاستتباع المنطقية وحول الأحكام، وما إلى ذلك. كان مهتمًا بالتقاليد الفلسفية لأوروبا الوسطى، خاصةً المنشورات الألمانية لفرانز برنتانو وغوتلوب فريجه وإدموند هوسرل.

نظرية النمط

عمل بير مارتن لوف في المنطق الرياضي لعدة عقود.[6]

من عام 1968 إلى عام 1969، عمل بير مارتن لوف كأستاذ مساعد في جامعة شيكاغو، حيث التقى ويليام آلفين هوارد الذي ناقش معه القضايا المتعلقة بمراسلات كاري- هوارد. تعود أول مسودة مقال لمارتن لوف حول نظرية النمط إلى عام 1971. عممت هذه النظرية غير الإسنادية نظام جيرارد ف. ومع ذلك، تبين أن هذا النظام غير متناسق بسبب مفارقة جيرارد التي اكتشفها جيرارد عند دراسة النظام يو، وهو امتداد غير متناسق للنظام ف. قادت هذه التجربة بير مارتن لوف إلى تطوير الأسس الفلسفية لنظرية النمط وتفسير معناه وهو شكل من دلالات إثبات صحة النظرية التي تبرر نظرية النمط الإسنادية كما قُدِّمَت في كتابه ببليوبوليس لعام 1984. وسّع مبير مارتن لوف النظرية ضمن عدد متزايد من النصوص الفلسفية كما في عمله المؤثر «في معاني الثوابت المنطقية ومبررات القوانين المنطقية».[7]

كانت نظرية النمط لعام 1984 امتدادًا للعمل السابق عندما قُدِّمَت النظرية في الكتاب من قبل نوردستروم وآخرون في عام 1990. تأثرت النظرية لاحقًا بأفكاره الدلالية القابلة للتطبيق على الكمبيوتر.

طورت نظرية النمط الحدسي لمارتن لوف فكرة الأنماط التابعة، وأثرت بشكل مباشر على تطور حساب البناء والإطار المنطقي. يعتمد عدد من أنظمة الإثبات المعتمدة على الحاسوب على نظرية النمط، على سبيل المثال: نو بي آر إل وإل إي جي أو وكوك وإيه إل إف وآغدا وتويلف وإبيغرام وإدريس.

المراجع

  1. ^ Peter Dybjer on types and testing – The Type Theory Podcast نسخة محفوظة 2020-05-17 على موقع واي باك مشين.
  2. ^ See e.g. Nordström، Bengt؛ Petersson، Kent؛ Smith، Jan M. (1990)، Programming in Martin-Löf 's Type Theory: An Introduction (PDF)، Oxford University Press، مؤرشف من الأصل (PDF) في 2022-04-25.
  3. ^ Member profile, الأكاديمية الأوروبية, retrieved 2014-01-26. "نسخة مؤرشفة". مؤرشف من الأصل في 2016-03-11. اطلع عليه بتاريخ 2020-09-12.{{استشهاد ويب}}: صيانة الاستشهاد: BOT: original URL status unknown (link)
  4. ^ For details, see the بير مارتن لوف section of this article.
  5. ^ Martin-Löf (1961).
  6. ^ Rolf Sundberg. 1971. Maximum likelihood theory and applications for distributions generated when observing a function of an exponential family variable. Dissertation, Institute for Mathematical Statistics, Stockholm University.
  7. ^ أندرس مارتن [English]. 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Evaluation of lifetimes in time-lengths below one nanosecond"). ("Sundberg formula")