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

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

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

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

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

Пер Мартин-Лёф - увлеченный орнитолог ; его первая научная публикация была посвящена смертности окольцованных птиц .

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В 1970-х годах Пер Мартин-Лёф внес важный вклад в статистическую теорию и вдохновил на дальнейшие исследования, особенно скандинавских статистиков, в том числе Рольфа Сундберга, Томаса Хёглунда и Штеффана Лауритцена. В этой работе предыдущее исследование Мартин-Лёфа вероятностных мер на полугруппах привело к понятию «повторяющейся структуры» и новому подходу к достаточной статистике, в котором были охарактеризованы однопараметрические экспоненциальные семейства . Он представил теоретико-категориальный подход к вложенным статистическим моделям с использованием принципов конечной выборки. До (и после) Мартина-Лёфа такие вложенные модели часто тестировались с использованием тестов гипотез хи-квадрат, обоснования которых носят только асимптотический характер (и поэтому не имеют отношения к реальным задачам, которые всегда имеют конечные выборки).

Метод максимизации ожидания для экспоненциальных семейств

Студент Мартина-Лёфа, Рольф Сундберг, разработал подробный анализ метода максимизации ожидания (EM) для оценки с использованием данных из экспоненциальных семейств, особенно с отсутствующими данными . Сундберг приписывает формулу, позже известную как формула Сундберга, предыдущим рукописям братьев Мартин-Лёф, Пера и Андерса . Многие из этих результатов достигли международного научного сообщества по 1976 документ о ожидание максимизация метода (EM) по Артур П. Демпстера , Nan Laird и Дональд Рубин , который был опубликован в ведущем международном журнале, авторами которого Королевского статистического общества .

Логика

Философская логика

В области философской логики Пер Мартин-Лёф опубликовал статьи по теории логических следствий , суждений и т. Д. Он интересовался центральноевропейскими философскими традициями, особенно немецкоязычными сочинениями Франца Брентано , Готтлоба Фреге и других авторов. Эдмунд Гуссерль .

Теория типов

Мартин-Лёф много десятилетий занимается математической логикой .

С 1968 по 69 год он работал доцентом в Чикагском университете, где познакомился с Уильямом Элвином Ховардом, с которым обсудил вопросы, связанные с перепиской Карри-Ховарда . Первый черновой вариант статьи Мартина-Лёфа по теории типов датируется 1971 годом. Эта импредикативная теория обобщает Систему F Жирара . Однако эта система оказалась непоследовательной из-за парадокса Жирара, который был обнаружен Жираром при изучении Системы U, непоследовательного расширения Системы F. Этот опыт привел Пера Мартина-Лёфа к разработке философских основ теории типов , его объяснения смысла , форма теоретико-доказательной семантики , которая оправдывает теорию предикативных типов, представленную в его книге Bibliopolis 1984 года, и расширенную во многих все более философских текстах, таких как его влиятельные « О значениях логических констант и обоснования логических законов» .

Теория типов 1984 года была экстенсиональной, в то время как теория типов, представленная в книге Нордстрёма и др. в 1990 году, на которую сильно повлияли его более поздние идеи, интенсиональные и более подходящие для реализации на компьютере.

Интуиционистская теория типов Мартина-Лёфа развила понятие зависимых типов и напрямую повлияла на развитие исчисления конструкций и логической основы LF . Ряд популярных компьютерных систем доказательства основаны на теории типов, например NuPRL , LEGO, Coq , ALF, Agda , Twelf , Epigram и Idris .

Награды

Мартин-Лёф является членом Шведской королевской академии наук и Academia Europaea .

Смотрите также

Примечания

использованная литература

Наблюдение за птицами и недостающие данные

• Мартин-Лёф, П. (1961). «Расчеты уровня смертности окольцованных птиц с особым упором на чернозобых Calidris alpina ». Arkiv för Zoologi (Zoology Files), Kungliga Svenska Vetenskapsakademien (Шведская королевская академия наук) Серия 2 . Тесьма 13 (21).

• Джордж А. Барнард , "Gone Birdwatching" , New Scientist , 4 декабря 1999 г., выпуск журнала 2215.
• Себер, ГАФ (2002). Оценка численности животных и связанных с ней параметров . Колдвел, Нью-Джерси: Blackburn Press. ISBN 1-930665-55-5.
• Ройл, JA; Р. М. Дорацио (2008). Иерархическое моделирование и вывод в экологии . Эльзевир. ISBN 978-1-930665-55-2.

Основания вероятности

• Пер Мартин-Лёф. «Определение случайных последовательностей». Информация и контроль , 9 (6): 602–619, 1966.
• Ли, Мин и Витаньи, Пол, Введение в сложность Колмогорова и ее приложения , Springer, 1997. Полный текст главы введения .

Вероятность на алгебраических структурах, вслед за Ульфом Гренандером

• Гренандер, Ульф . Вероятность на алгебраических структурах . (Отпечаток Dover)
• Мартин-Лёф, П. Теорема непрерывности локально компактной группы. Теор. Вероятность. и Применен. 10 1965 367–371.
• Мартин-Лёф, Пер. Теория вероятностей на дискретных полугруппах. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 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 учебном году) при содействии Рольфа Сундберга. Стокгольмский университет.
• Мартин-Лёф, П. «Точные тесты, доверительные интервалы и оценки», с обсуждением AWF Edwards , GA Barnard , DA Sprott, O. Barndorff-Nielsen, D. Basu и G. Rasch . Труды конференции по основополагающим вопросам статистического вывода (Орхус, 1973), стр. 121–138. Воспоминания, № 1, Теорет. Статист., Инст. Матем., Univ. Орхус, Орхус, 1974.
• Мартин-Лёф, П. Повторяющиеся структуры и связь между каноническим и микроканоническим распределениями в статистике и статистической механике. С обсуждением Д.Р. Кокса и Г. Раша и ответом автора. Труды конференции по основополагающим вопросам статистического вывода (Орхус, 1973), стр. 271–294. Воспоминания, № 1, Теорет. Статист., Инст. Матем., Univ. Орхус, Орхус, 1974.
• Мартин-Лёф, П. Понятие избыточности и его использование в качестве количественной меры отклонения между статистической гипотезой и набором данных наблюдений. При обсуждении Ф. Abildgård, А. П. Демпстера , Д. Басу , DR Кокс , AWF Эдвардс , Д. Шпротт, Г. А. Барнарда , О. Barndorff-Nielsen, JD Kalbfleisch и Г. Раша и ответ автора. Труды конференции по основополагающим вопросам статистического вывода (Орхус, 1973), стр. 1–42. Воспоминания, № 1, Теорет. Статист., Инст. Матем., Univ. Орхус, Орхус, 1974.
• Мартин-Лёф, Пер Понятие избыточности и его использование в качестве количественной меры расхождения между статистической гипотезой и набором данных наблюдений. Сканд. J. Statist. 1 (1974), нет. 1, 3-18.
• Свердруп, Эрлинг. «Испытания без питания». Сканд. J. Statist. 2 (1975), нет. 3, 158–160.
• Мартин-Лёф, за ответ на полемическую статью Эрлинга Свердрупа: «Испытания без силы» ( Scand. J. Statist. 2 (1975), № 3, 158–160). Сканд. J. Statist. 2 (1975), нет. 3, 161–165.
• Свердруп, Эрлинг. Ответ на: `` Испытания без питания ( Scand. J. Statist. 2 (1975), 161-165) П. Мартин-Лёфа. Сканд. J. Statist. 4 (1977), нет. 3, 136–138.
• Мартин-Лёф, П. Точные тесты, доверительные интервалы и оценки. Основы вероятности и статистики. II. Synthese 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. Gebiete 29 (1974), 257–271.
• Лауритцен, Штеффен Л. Экстремальные семейства и системы достаточной статистики . Конспект лекций по статистике, 49. Springer-Verlag, New York, 1988. xvi + 268 pp. ISBN  0-387-96872-5

Основы математики, логики и информатики

• Пер Мартин-Лёф. Теория типов. Препринт, Стокгольмский университет, 1971.
• Пер Мартин-Лёф. Интуиционистская теория типов . В Дж. Самбин и Дж. Смит, редакторы, Двадцать пять лет теории конструктивного типа. Oxford University Press, 1998. Перепечатанная версия неопубликованного отчета 1972 года.
• Пер Мартин-Лёф. Интуиционистская теория типов: Предикативная часть. В HE Rose и JC Shepherdson, редакторах, Logic Colloquium '73, страницы 73–118. Северная Голландия, 1975 год.
• Пер Мартин-Лёф. Конструктивная математика и компьютерное программирование . В логике, методологии и философии науки VI, 1979 . Ред. Коэн и др. Северная Голландия, Амстердам. С. 153–175, 1982.
• Пер Мартин-Лёф. Интуиционистская теория типов . (Примечания Джованни Самбина к серии лекций, прочитанных в Падуе, июнь 1980 г.). Неаполь, Библиополис, 1984.
• Пер Мартин-Лёф. Философские последствия теории типов , Неопубликованные заметки, 1987?
• Пер Мартин-Лёф. Исчисление подстановки , 1992. Заметки из лекции, прочитанной в Гетеборге.
• Бенгт Нордстрем, Кент Петерссон и Ян М. Смит. Программирование в теории типов Мартина-Лёфа . Oxford University Press, 1990. (Книга больше не издается, но есть бесплатная версия ).
• Пер Мартин-Лёф. О значениях логических констант и обоснованиях логических законов . Северный журнал философской логики , 1 (1): 11–60, 1996.
• Пер Мартин-Лёф. Логика и этика . В T. Piecha и P. Schroeder-Heister, редакторах, Proof-Theoretic Semantics: Assessment and Future Perspectives. Труды Третьей Тюбингенской конференции по теоретико-доказательной семантике, 27–30 марта 2019 г. , страницы 227-235. URI: http://dx.doi.org/10.15496/publikation-35319 . Тюбингенский университет 2019.

внешние ссылки

• Пер Мартин-Лёф из проекта « Математическая генеалогия»