WikiDer > Пер Мартин-Лёф
Пер Мартин-Лёф | |
|---|---|
 Пер Мартин-Лёф в 2004 году | |
| Родившийся | 8 мая 1942 г. |
| Национальность | Шведский |
| Гражданство | Швеция |
| Альма-матер | Стокгольмский университет |
| Известен | Случайные последовательности Точные тесты Повторяющаяся структура Достаточная статистика Метод максимизации ожидания Теория типа Мартина-Лёфа |
| Награды | Шведская королевская академия наук |
| Научная карьера | |
| Поля | Информатика Логика Математическая статистика Философия |
| Учреждения | Стокгольмский университет Чикагский университет Орхусский университет |
| Докторант | Андрей Николаевич Колмогоров |
Пер Эрик Рутгер Мартин-Лёф (/лɒж/;[2] Шведский:[ˈMǎʈːɪn ˈløːv];[3] родился 8 мая 1942 г.) Шведский логик, философ, и математик-статистик. Он всемирно известен своими работами по основам теории вероятностей, статистики, математической логики и информатики. С конца 1970-х годов публикации Мартина-Лёфа были в основном в логика. В философская логикаМартин-Лёф боролся с философией логическое следствие и суждение, частично вдохновленные работой Брентано, Frege, и Гуссерль. В математическая логика, Мартин-Лёф активно занимался разработкой интуиционистская теория типов как конструктивная основа математики; Работа Мартина-Лёфа по теории типов повлияла на Информатика.[4]
До выхода на пенсию в 2009 году[5] Пер Мартин-Лёф занимал кафедру математики и философии в Стокгольмский университет.[6]
Его брат Андерс Мартин-Лёф в настоящее время является почетным профессором математической статистики Стокгольмского университета; два брата сотрудничали в исследованиях вероятностей и статистики. Исследования Андерса и Пера Мартин-Лёфа повлияли на статистическую теорию, особенно в отношении экспоненциальные семейства, то метод максимизации ожидания за отсутствующие данные, и выбор модели.[7]
Пер Мартин-Лёф - энтузиаст орнитолог; его первая научная публикация была посвящена уровню смертности окольцованные птицы.[8]
Случайность и колмогоровская сложность
В 1964 и 1965 годах Мартин-Лёф учился в Москве под руководством Андрей Николаевич Колмогоров. Он написал статью 1966 года Определение случайных последовательностей это дало первое подходящее определение случайной последовательности.[9]
Ранее исследователи, такие как Рихард фон Мизес попытался формализовать понятие тест на случайность чтобы определить случайную последовательность как такую, которая прошла все тесты на случайность; однако точное понятие теста на случайность осталось неясным. Ключевой вывод Мартина-Лёфа заключался в использовании теория вычислений формально определить понятие теста на случайность. Это контрастирует с идеей случайности в вероятность; В этой теории ни один конкретный элемент пространства выборки нельзя назвать случайным.
С тех пор было показано, что случайность Мартина-Лёфа допускает множество эквивалентных характеристик - в терминах сжатие, тесты на случайность и играть в азартные игры - которые внешне мало похожи на исходное определение, но каждое из них удовлетворяет нашему интуитивному представлению о свойствах, которыми должны обладать случайные последовательности: случайные последовательности должны быть несжимаемыми, они должны проходить статистические тесты на случайность, и должно быть невозможно зарабатывать деньги делать ставки на них. Существование этих множественных определений случайности Мартина-Лёфа и стабильность этих определений при различных моделях вычислений свидетельствуют о том, что случайность Мартина-Лёфа является фундаментальным свойством математики, а не случайностью конкретной модели Мартина-Лёфа. Тезис о том, что определение случайности Мартина-Лёфа «правильно» отражает интуитивное понятие случайности, получил название «Мартин-Лёф-Чайтин Тезис »; он в чем-то похож на Тезис Черча – Тьюринга.[10]
Следуя работе Мартина-Лёфа, алгоритмическая теория информации определяет случайную строку как строку, которая не может быть получена из компьютерной программы, которая короче строки (Случайность Чайтина – Колмогорова); т.е. строка, чья Колмогоровская сложность не меньше длины строки. Это значение отличается от использования термина в статистике. В то время как статистическая случайность относится к процесс который производит строку (например, подбрасывание монеты для получения каждого бита случайным образом дает строку), алгоритмическая случайность относится к сама струна. Алгоритмическая теория информации отделяет случайные от неслучайных строк способом, который относительно инвариантен к модель вычисления быть использованным.
An алгоритмически случайная последовательность является бесконечный последовательность символов, все префиксы которой (за исключением, возможно, конечного числа исключений) являются строками, «близкими к» алгоритмически случайными (их длина находится в пределах константы их колмогоровской сложности).
Математическая статистика
Пер Мартин-Лёф провел важные исследования в математическая статистика, который (в шведской традиции) включает теория вероятности и статистика.
Наблюдение за птицами и определение пола
Пер Мартин-Лёф начал наблюдение за птицами в молодости и остается увлеченным орнитологом.[11] В подростковом возрасте он опубликовал статью об оценке уровень смертности птиц, используя данные из звенящая птица, в шведском зоологическом журнале: Эта статья вскоре была процитирована в ведущих международных журналах, и эту статью продолжают цитировать.[8][12]
в биология и статистика из птицы, есть несколько проблем отсутствующие данные. В первой статье Мартина-Лёфа обсуждалась проблема оценки уровня смертности Чернозобик виды, использующие захват-повторный захват методы. Вторая проблема отсутствия данных возникает при изучении пола птиц. Проблема определения биологический пол птицы, что чрезвычайно сложно для человека, - один из первых примеров в лекциях Мартина-Лёфа о статистические модели.
Вероятность на алгебраических структурах
Мартин-Лёф написал лицензионную диссертацию о вероятности алгебраических структур, в частности, полугрупп, исследовательскую программу под руководством Ульф Гренандер в Стокгольмском университете.[13][14][15]
Статистические модели
Мартин-Лёф разработал инновационные подходы к статистическая теория. В своей статье «О таблицах случайных чисел» Колмогоров заметил, что частотная вероятность понятие ограничение свойства бесконечных последовательностей не смогли обеспечить основу для статистики, которая рассматривает только конечные выборки.[16] Большая часть работы Мартина-Лёфа в области статистики заключалась в обеспечении основы статистики на основе конечной выборки.
Выбор модели и проверка гипотез
В 1970-х годах Пер Мартин-Лёф внес важный вклад в статистическую теорию и вдохновил на дальнейшие исследования, особенно скандинавских статистиков, включая Рольфа Сундберга, Томаса Хёглунда и Штеффана Лауритцена. В этой работе предыдущее исследование Мартин-Лёфа вероятностных мер на полугруппах привело к понятию «повторяющейся структуры» и новому подходу к достаточной статистике, в котором однопараметрический экспоненциальные семейства были охарактеризованы. Он предоставил теоретико-категориальный подход к вложенные статистические модели, используя принципы конечной выборки. До (и после) Мартина-Лёфа такие вложенные модели часто тестировались с использованием критериев гипотезы хи-квадрат, обоснования которых являются только асимптотическими (и поэтому не имеют отношения к реальным задачам, которые всегда имеют конечные выборки).[16]
Метод максимизации ожидания для экспоненциальных семейств
Ученик Мартина-Лёфа, Рольф Сундберг, провел подробный анализ ожидание-максимизация (EM) метод для оценки с использованием данных из экспоненциальных семейств, особенно с отсутствующие данные. Сундберг приписывает формулу, позже известную как формула Сундберга, предыдущим рукописям братьев Мартин-Лёф, Пера и Андерс.[17][18][19][20] Многие из этих результатов стали известны международному научному сообществу благодаря статье 1976 г. максимизация ожидания (EM) метод к Артур П. Демпстер, Нэн Лэрд, и Дональд Рубин, который был опубликован в ведущем международном журнале, спонсируемом Королевское статистическое общество.[21]
Логика
Философская логика
В философская логика, Пер Мартин-Лёф опубликовал статьи по теории логическое следствие, на сужденияи т. д. Он интересовался Центральноевропейский философские традиции, особенно немецкоязычные сочинения Франц Брентано, Готтлоб Фреге, и из Эдмунд Гуссерль.
Теория типов
Мартин-Лёф работал в математическая логика на многие десятилетия.
С 1968 по 69 год работал доцентом в Чикагский университет где он встретился Уильям Элвин Ховард с которым он обсуждал вопросы, связанные с Переписка Карри – Ховарда. Первый черновик статьи Мартина-Лёфа по теории типов датируется 1971 годом. непредсказуемый теория обобщенная Жирара Система F. Однако эта система оказалась непоследовательный из-за Парадокс Жирара который был обнаружен Жираром при изучении Системы U, противоречивого расширения Системы F. Этот опыт привел Пера Мартин-Лёфа к разработке философских основ теория типов, его смысл объяснения, форма теоретико-доказательная семантика, что оправдывает предикативный теория шрифтов, представленная в его книге «Библиополис» 1984 г., и расширенная во многих философских текстах, которые становятся все более и более философскими, например О значениях логических констант и обоснованиях логических законов.
Теория типов 1984 года была экстенсиональной, в то время как теория типов, представленная в книге Нордстрёма. и другие. в 1990 году, на который сильно повлияли его более поздние идеи, интенсиональные и более подходящие для реализации на компьютере.
Интуиционистская теория типов Мартина-Лёфа развила понятие зависимые типы и непосредственно повлияли на развитие расчет конструкций и логическая структура LF. Ряд популярных компьютерных систем доказательства основаны на теории типов, например NuPRL, КОНСТРУКТОР ЛЕГО, Coq, ALF, Агда, Двенадцать, Эпиграмма, и Идрис.
Награды
Мартин-Лёф является членом Шведская королевская академия наук[22] и из Academia Europaea.[6]
Смотрите также
Примечания
- ^ The International Кто есть кто: 1996-97, Europa Publications, 1996, стр. 1020: «Мартин-Лёф, Пер Эрик Рутгер».
- ^ Обеспечивает ли HoTT основу для математики? Джеймс Лэдман (Бристольский университет, Великобритания)
- ^ Питер Дибьер о типах и тестировании - подкаст The Type Theory
- ^ См. Например Нордстрём, Бенгт; Петерссон, Кент; Смит, Ян М. (1990), Программирование в теории типов Мартина-Лёфа: введение (PDF), Oxford University Press.
- ^ Философия и основы математики: гносеологические и онтологические аспекты. Конференция, посвященная Перу Мартин-Лёфу по случаю его выхода на пенсию В архиве 2014-02-02 в Wayback Machine. Swedish Collegium for Advanced Study, Уппсала, 5–8 мая 2009 г. Источник: 26 января 2014 г.
- ^ а б Профиль участника, Academia Europaea, получено 26 января 2014.
- ^ Подробнее см. # Статистические модели раздел этой статьи.
- ^ а б Мартин-Лёф (1961).
- ^ Мартин-Лёф, Пер (1966). «Определение случайных последовательностей». Информация и контроль. 9 (6): 602–619. Дои:10.1016 / S0019-9958 (66) 80018-9.
- ^ Жан-Поль Делахайе, Случайность, непредсказуемость и отсутствие порядка, в Философия вероятности, п. 145–167, Springer 1993.
- ^ Джордж А. Барнард, "Наблюдение за птицами", Новый ученый, 4 декабря 1999 г., номер журнала 2215.
- ^ С. М. Тейлор (1966). «Недавняя количественная работа по популяциям британских птиц. Обзор». Журнал Королевского статистического общества, серия D. 16 (= № 2): 119–170. JSTOR 2986734.
- ^ Мартин-Лёф, П. Теорема непрерывности на локально компактной группе. Теор. Вероятность. и Применен. 10 1965 367–371.
- ^ Мартин-Лёф, Пер Теория вероятностей на дискретных полугруппах. Z. Wahrscheinlichkeitstheorie und Verw. Гебиете 4 1965 78–102
- ^ Нитис Мухопадхьяй. Разговор с Ульфом Гренандером. Статист. Sci. Том 21, номер 3 (2006), 404–426.
- ^ а б Колмогоров, Андрей Н. (1963). «О таблицах случайных чисел». Sankhyā Ser. А. 25: 369–375.
- ^ Рольф Сундберг. 1971 г. Теория максимального правдоподобия и приложения для распределений, сгенерированных при наблюдении функции экспоненциальной переменной семейства. Диссертация, Институт математической статистики, Стокгольмский университет.
- ^ Андерс Мартин-Лёф. 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Оценка продолжительности жизни во временном интервале менее одной наносекунды"). («Формула Сундберга»)
- ^ Пер Мартин-Лёф. 1966 г. Статистика с точки зрения статистической механики. Конспект лекций Математического института Орхусского университета. («Формула Сундберга» приписана Андерсу Мартин-Лёфу).
- ^ Пер Мартин-Лёф. 1970 г. Statistika Modeller (Статистические модели): Anteckningar fran Seminarier läsåret 1969–1970 (Записи семинаров в 1969–1970 учебном году) при содействии Рольфа Сундберга. Стокгольмский университет. («Формула Сундберга»)
- ^ Демпстер, А.; Лэрд, Н.; Рубин, Д. (1977). «Максимальная вероятность неполных данных с помощью алгоритма EM». Журнал Королевского статистического общества, серия B. 39 (1): 1–38. JSTOR 2984875. МИСТЕР 0501537.
- ^ "Шведская королевская академия наук: Пер Мартин-Лёф". Получено 2009-05-01.[мертвая ссылка]
Рекомендации
Наблюдение за птицами и недостающие данные
- Мартин-Лёф, П. (1961). "Расчет смертности окольцованных птиц с особым акцентом на чернозобых. Калидрис альпина". Arkiv för Zoologi (Zoology Files), Kungliga Svenska Vetenskapsakademien (Шведская королевская академия наук) Серия 2. Тесьма 13 (21).CS1 maint: ref = harv (связь)
- Джордж А. Барнард, "Наблюдение за птицами", Новый ученый, 4 декабря 1999 г., номер журнала 2215.
- Себер, Г.А.Ф. (2002). Оценка численности животных и связанных параметров. Колдвел, Нью-Джерси: Blackburn Press. ISBN 1-930665-55-5.
- Ройл, Дж. А .; Р. М. Дорацио (2008). Иерархическое моделирование и вывод в экологии. Эльзевир. ISBN 978-1-930665-55-2.
Основания вероятности
- Пер Мартин-Лёф. «Определение случайных последовательностей». Информация и контроль, 9(6): 602–619, 1966.
- Ли, Мин и Витаньи, Пол, Введение в колмогоровскую сложность и ее приложения, Springer, 1997. Полный текст вводной главы.
Вероятность на алгебраических структурах, по Ульфу Гренандеру
- Гренандер, Ульф. Вероятность на алгебраических структурах. (Отпечаток Dover)
- Мартин-Лёф, П. Теорема непрерывности на локально компактной группе. Теор. Вероятность. и Применен. 10 1965 367–371.
- Мартин-Лёф, Пер. Теория вероятностей на дискретных полугруппах. Z. Wahrscheinlichkeitstheorie und Verw. Гебиете 4 1965 78—102
- Нитис Мухопадхьяй. «Разговор с Ульфом Гренандером». Статист. Sci. Том 21, номер 3 (2006), 404–426.
Основы статистики
- Андерс Мартин-Лёф. 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Оценка продолжительности жизни во временном интервале менее одной наносекунды"). («Формула Сундберга», согласно Сундбергу 1971 г.)
- Пер Мартин-Лёф. 1966 г. Статистика с точки зрения статистической механики. Конспект лекций Математического института Орхусского университета. («Формула Сундберга» зачислена Андерсом Мартин-Лёфом, согласно Сундбергу 1971 г.)
- Пер Мартин-Лёф. 1970 г. Statistika Modeller (Статистические модели): Anteckningar fran Seminarier läsåret 1969–1970 (Записи семинаров в 1969–1970 учебном году) при содействии Рольфа Сундберга. Стокгольмский университет.
- Мартин-Лёф, П. «Точные тесты, доверительные интервалы и оценки», с обсуждением А. В. Ф. Эдвардс, Г. А. Барнард, Д. А. Спротт, О. Барндорф-Нильсен, Д. Басу и Г. Раш. Труды конференции по основополагающим вопросам статистического вывода (Орхус, 1973), стр. 121–138. Воспоминания, № 1, Теорет. Статист., Инст. Математика, Univ. Орхус, Орхус, 1974.
- Мартин-Лёф, П. Повторяющиеся структуры и связь между каноническим и микроканоническим распределениями в статистике и статистической механике. С обсуждением Д. Р. Кокс и Г. Раш и ответ автора. Труды конференции по основополагающим вопросам статистического вывода (Орхус, 1973), стр. 271–294. Воспоминания, № 1, Теорет. Статист., Инст. Математика, Univ. Орхус, Орхус, 1974.
- Мартин-Лёф, П. Понятие избыточности и его использование в качестве количественной меры отклонения между статистической гипотезой и набором данных наблюдений. С обсуждением Ф. Абильдгарда, А. П. Демпстер, Д. Басу, Д. Р. Кокс, А. В. Ф. Эдвардс, Д. А. Спротт, Г. А. Барнард, О. Барндорф-Нильсен, Дж. Д. Кальбфляйш и Г. Раш и ответ автора. Труды конференции по основополагающим вопросам статистического вывода (Орхус, 1973), стр. 1–42. Воспоминания, № 1, Теорет. Статист., Инст. Математика, Univ. Орхус, Орхус, 1974.
- Мартин-Лёф, Пер Понятие избыточности и его использование в качестве количественной меры расхождения между статистической гипотезой и набором данных наблюдений. Сканд. J. Statist. 1 (1974), нет. 1, 3-18.
- Свердруп, Эрлинг. «Испытания без питания». Сканд. J. Statist. 2 (1975), нет. 3, 158–160.
- Мартин-Лёф, ответ на полемическую статью Эрлинга Свердрупа: `` Испытания без силы (Сканд. J. Statist. 2 (1975), нет. 3, 158–160). Сканд. J. Statist. 2 (1975), нет. 3, 161–165.
- Свердруп, Эрлинг. Ответ на: `` Испытания без питания (Сканд. J. Statist. 2 (1975), 161–165) П. Мартин-Лёфа. Сканд. J. Statist. 4 (1977), нет. 3, 136–138.
- Мартин-Лёф, П. Точные тесты, доверительные интервалы и оценки. Основы вероятности и статистики. II. Синтез 36 (1977), нет. 2, 195—206.
- Рольф Сундберг. 1971 г. Теория максимального правдоподобия и приложения для распределений, сгенерированных при наблюдении функции экспоненциальной переменной семейства. Диссертация, Институт математической статистики, Стокгольмский университет.
- Сундберг, Рольф. Теория максимального правдоподобия для неполных данных из экспоненциального семейства. Сканд. J. Statist. 1 (1974), нет. 2, 49—58.
- Сандберг, Рольф Итерационный метод решения уравнений правдоподобия для неполных данных из экспоненциальных семейств. Comm. Статист. - Simulation Comput. B5 (1976), нет. 1, 55–64.
- Сундберг, Рольф Некоторые результаты о разложимых (или марковских) моделях для многомерных таблиц сопряженности: распределение маргиналов и разбиение тестов. Сканд. J. Statist. 2 (1975), нет. 2, 71–79.
- Хёглунд, Томас. Точная оценка - метод статистической оценки. Z. Wahrscheinlichkeitstheorie und Verw. Гебиете 29 (1974), 257—271.
- Лауритцен, Штеффен Л. Экстремальные семейства и системы достаточной статистики. Конспект лекций по статистике, 49. Springer-Verlag, New York, 1988. xvi + 268 с. ISBN 0-387-96872-5
Основы математики, логики и информатики
- Пер Мартин-Лёф. Теория типов. Препринт, Стокгольмский университет, 1971.
- Пер Мартин-Лёф. Интуиционистская теория типов. В Дж. Самбин и Дж. Смит, редакторы, Двадцать пять лет теории конструктивного типа. Oxford University Press, 1998. Перепечатанная версия неопубликованного отчета 1972 года.
- Пер Мартин-Лёф. Интуиционистская теория типов: Предикативная часть. В Х. Э. Роуз и Дж. К. Шепердсон, редакторах, Logic Colloquium ‘73, стр. 73–118. Северная Голландия, 1975 год.
- Пер Мартин-Лёф. Конструктивная математика и компьютерное программирование. В Логика, методология и философия науки VI, 1979 г.. Ред. Коэн и др. Северная Голландия, Амстердам. С. 153–175, 1982.
- Пер Мартин-Лёф. Интуиционистская теория типов. (Примечания Джованни Самбина к серии лекций, прочитанных в Падуе, июнь 1980 г.). Неаполь, Библиополис, 1984.
- Пер Мартин-Лёф. Философские последствия теории типов, Неопубликованные заметки, 1987?
- Пер Мартин-Лёф. Исчисление подстановки, 1992. Заметки из лекции, прочитанной в Гетеборге.
- Бенгт Нордстрем, Кент Петерссон и Ян М. Смит. Программирование в теории типов Мартина-Лёфа. Oxford University Press, 1990. (Книга больше не издается, но бесплатная версия был доступен.)
- Пер Мартин-Лёф. О значениях логических констант и обоснованиях логических законов. Северный журнал философской логики, 1(1): 11–60, 1996.
- Пер Мартин-Лёф. Логика и этика. В редакции Т. Пиеха и П. Шредер-Хайстер, Теоретико-доказательная семантика: оценка и перспективы на будущее. Труды Третьей Тюбингенской конференции по теоретико-доказательной семантике, 27–30 марта 2019 г., страницы 227-235. URI: http://dx.doi.org/10.15496/publikation-35319. Тюбингенский университет 2019.
