Пер Мартин-Лёф - Per Martin-Löf

Пер Мартин-Лёф
Пер Мартин-Лёф
	Пер Мартин-Лёф в 2004 году
Родившийся	8 мая 1942 г. (возраст 78); Стокгольм, Швеция
Национальность	Шведский
Гражданство	Швеция
Альма-матер	Стокгольмский университет
Известен	Случайные последовательности ; Точные тесты ; Повторяющаяся структура ; Достаточная статистика ; Метод максимизации ожидания ; Теория типа Мартина-Лёфа
Награды	Шведская королевская академия наук
	Научная карьера
Поля	Информатика; Логика; Математическая статистика; Философия
Учреждения	Стокгольмский университет; Чикагский университет; Орхусский университет
Докторант	Андрей Николаевич Колмогоров

Пер Эрик Рутгер Мартин-Лёф (/лɒж/;^[2] Шведский:[ˈMǎʈːɪn ˈløːv];^[3] родился 8 мая 1942 г.) Шведский логик, философ, и математик-статистик. Он всемирно известен своими работами по основам теории вероятностей, статистики, математической логики и информатики. С конца 1970-х годов публикации Мартина-Лёфа были в основном в логика. В философская логика Мартин-Лёф боролся с философией логическое следствие и суждение, частично вдохновленные работой Брентано, Frege, и Гуссерль. В математическая логика, Мартин-Лёф активно занимался разработкой интуиционистская теория типов как конструктивная основа математики; Работа Мартина-Лёфа по теории типов повлияла на Информатика.^[4]

До выхода на пенсию в 2009 году^[5] Пер Мартин-Лёф занимал кафедру математики и философии в Стокгольмский университет.^[6]

Его брат Андерс Мартин-Лёф в настоящее время является почетным профессором математической статистики Стокгольмского университета; два брата сотрудничали в исследованиях вероятностей и статистики. Исследования Андерса и Пера Мартин-Лёфа повлияли на статистическую теорию, особенно в отношении экспоненциальные семейства, то метод максимизации ожидания за отсутствующие данные, и выбор модели.^[7]

Пер Мартин-Лёф - энтузиаст орнитолог; его первая научная публикация была посвящена уровню смертности окольцованные птицы.^[8]

Случайность и колмогоровская сложность

В 1964 и 1965 годах Мартин-Лёф учился в Москве под руководством Андрей Николаевич Колмогоров. Он написал статью 1966 года Определение случайных последовательностей это дало первое подходящее определение случайной последовательности.^[9]

Ранее исследователи, такие как Рихард фон Мизес попытался формализовать понятие тест на случайность чтобы определить случайную последовательность как такую, которая прошла все тесты на случайность; однако точное понятие теста на случайность осталось неясным. Ключевой вывод Мартина-Лёфа заключался в использовании теория вычислений формально определить понятие теста на случайность. Это контрастирует с идеей случайности в вероятность; В этой теории ни один конкретный элемент пространства выборки нельзя назвать случайным.

С тех пор было показано, что случайность Мартина-Лёфа допускает множество эквивалентных характеристик - в терминах сжатие, тесты на случайность и играть в азартные игры - которые внешне мало похожи на исходное определение, но каждое из них удовлетворяет нашему интуитивному представлению о свойствах, которыми должны обладать случайные последовательности: случайные последовательности должны быть несжимаемыми, они должны проходить статистические тесты на случайность, и должно быть невозможно зарабатывать деньги делать ставки на них. Существование этих множественных определений случайности Мартина-Лёфа и стабильность этих определений при различных моделях вычислений свидетельствуют о том, что случайность Мартина-Лёфа является фундаментальным свойством математики, а не случайностью конкретной модели Мартина-Лёфа. Тезис о том, что определение случайности Мартина-Лёфа «правильно» отражает интуитивное понятие случайности, получил название «Мартин-Лёф-Чайтин Тезис »; он в чем-то похож на Тезис Черча – Тьюринга.^[10]

Следуя работе Мартина-Лёфа, алгоритмическая теория информации определяет случайную строку как строку, которая не может быть получена из компьютерной программы, которая короче строки (Случайность Чайтина – Колмогорова ); т.е. строка, чья Колмогоровская сложность не меньше длины строки. Это значение отличается от использования термина в статистике. В то время как статистическая случайность относится к процесс который производит строку (например, подбрасывание монеты для получения каждого бита случайным образом дает строку), алгоритмическая случайность относится к сама струна. Алгоритмическая теория информации отделяет случайные от неслучайных строк способом, который относительно инвариантен к модель вычисления быть использованным.

An алгоритмически случайная последовательность является бесконечный последовательность символов, все префиксы которой (за исключением, возможно, конечного числа исключений) являются строками, «близкими к» алгоритмически случайными (их длина находится в пределах константы их колмогоровской сложности).

Математическая статистика

Пер Мартин-Лёф провел важные исследования в математическая статистика, который (в шведской традиции) включает теория вероятности и статистика.

Наблюдение за птицами и определение пола

В Чернозобик (Calidris alpina)

Пер Мартин-Лёф начал наблюдение за птицами в молодости и остается увлеченным орнитологом.^[11] В подростковом возрасте он опубликовал статью об оценке уровень смертности птиц, используя данные из звенящая птица, в шведском зоологическом журнале: Эта статья вскоре была процитирована в ведущих международных журналах, и эту статью продолжают цитировать.^[8]^[12]

в биология и статистика из птицы, есть несколько проблем отсутствующие данные. В первой статье Мартина-Лёфа обсуждалась проблема оценки уровня смертности Чернозобик виды, использующие захват-повторный захват методы. Вторая проблема отсутствия данных возникает при изучении пола птиц. Проблема определения биологический пол птицы, что чрезвычайно сложно для человека, - один из первых примеров в лекциях Мартина-Лёфа о статистические модели.

Вероятность на алгебраических структурах

Мартин-Лёф написал лицензионную диссертацию о вероятности алгебраических структур, в частности, полугрупп, исследовательскую программу под руководством Ульф Гренандер в Стокгольмском университете.^[13]^[14]^[15]

Статистические модели

Мартин-Лёф разработал инновационные подходы к статистическая теория. В своей статье «О таблицах случайных чисел» Колмогоров заметил, что частотная вероятность понятие ограничение свойства бесконечных последовательностей не смогли обеспечить основу для статистики, которая рассматривает только конечные выборки.^[16] Большая часть работы Мартина-Лёфа в области статистики заключалась в обеспечении основы статистики на основе конечной выборки.

Выбор модели и проверка гипотез

Шаги алгоритма EM на двухкомпонентном гауссовском модель смеси на Старый Верный набор данных

В 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.^{[мертвая ссылка ]}

внешняя ссылка

Пер Мартин-Лёф на Проект "Математическая генеалогия"

[1] The International Кто есть кто: 1996-97, Europa Publications, 1996, стр. 1020: «Мартин-Лёф, Пер Эрик Рутгер».

[2] Обеспечивает ли HoTT основу для математики? Джеймс Лэдман (Бристольский университет, Великобритания)

[3] Питер Дибьер о типах и тестировании - подкаст The Type Theory

[4] См. Например Нордстрём, Бенгт; Петерссон, Кент; Смит, Ян М. (1990), Программирование в теории типов Мартина-Лёфа: введение (PDF), Oxford University Press.

[5] Философия и основы математики: гносеологические и онтологические аспекты. Конференция, посвященная Перу Мартин-Лёфу по случаю его выхода на пенсию В архиве 2014-02-02 в Wayback Machine. Swedish Collegium for Advanced Study, Уппсала, 5–8 мая 2009 г. Источник: 26 января 2014 г.

[ae-6] а ^б Профиль участника, Academia Europaea, получено 26 января 2014.

[7] Подробнее см. # Статистические модели раздел этой статьи.

[ml61-8] а ^б Мартин-Лёф (1961).

[kolrand1-9] Мартин-Лёф, Пер (1966). «Определение случайных последовательностей». Информация и контроль. 9 (6): 602–619. Дои:10.1016 / S0019-9958 (66) 80018-9.

[10] Жан-Поль Делахайе, Случайность, непредсказуемость и отсутствие порядка, в Философия вероятности, п. 145–167, Springer 1993.

[11] Джордж А. Барнард, "Наблюдение за птицами", Новый ученый, 4 декабря 1999 г., номер журнала 2215.

[12] С. М. Тейлор (1966). «Недавняя количественная работа по популяциям британских птиц. Обзор». Журнал Королевского статистического общества, серия D. 16 (= № 2): 119–170. JSTOR 2986734.

[13] Мартин-Лёф, П. Теорема непрерывности на локально компактной группе. Теор. Вероятность. и Применен. 10 1965 367–371.

[14] Мартин-Лёф, Пер Теория вероятностей на дискретных полугруппах. Z. Wahrscheinlichkeitstheorie und Verw. Гебиете 4 1965 78–102

[15] Нитис Мухопадхьяй. Разговор с Ульфом Гренандером. Статист. Sci. Том 21, номер 3 (2006), 404–426.

[kolrand-16] а ^б Колмогоров, Андрей Н. (1963). «О таблицах случайных чисел». Sankhyā Ser. А. 25: 369–375.

[17] Рольф Сундберг. 1971 г. Теория максимального правдоподобия и приложения для распределений, сгенерированных при наблюдении функции экспоненциальной переменной семейства. Диссертация, Институт математической статистики, Стокгольмский университет.

[18] Андерс Мартин-Лёф. 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Оценка продолжительности жизни во временном интервале менее одной наносекунды"). («Формула Сундберга»)

[19] Пер Мартин-Лёф. 1966 г. Статистика с точки зрения статистической механики. Конспект лекций Математического института Орхусского университета. («Формула Сундберга» приписана Андерсу Мартин-Лёфу).

[20] Пер Мартин-Лёф. 1970 г. Statistika Modeller (Статистические модели): Anteckningar fran Seminarier läsåret 1969–1970 (Записи семинаров в 1969–1970 учебном году) при содействии Рольфа Сундберга. Стокгольмский университет. («Формула Сундберга»)

[21] Демпстер, А.; Лэрд, Н.; Рубин, Д. (1977). «Максимальная вероятность неполных данных с помощью алгоритма EM». Журнал Королевского статистического общества, серия B. 39 (1): 1–38. JSTOR 2984875. МИСТЕР 0501537.

[22] "Шведская королевская академия наук: Пер Мартин-Лёф". Получено 2009-05-01.^{[мертвая ссылка ]}

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

Пер Мартин-Лёф - Per Martin-Löf

Содержание