Пер Эрик Рутгер Мартин-Лёф ( / l ɒ f / ; [2] шведский: [ˈmǎʈːɪn ˈløːv] ; [3] родился 8 мая 1942 года) - шведский логик , философ и математик-статистик . Он всемирно известен своими работами по основам теории вероятностей, статистики, математической логики и информатики. С конца 1970-х годов публикации Мартина-Лёфа были в основном по логике . В философской логике Мартин-Лёф боролся с философией логического следствия и суждения., отчасти вдохновленный работами Брентано , Фреге и Гуссерля . В математической логике Мартин-Лёф активно разрабатывал интуиционистскую теорию типов как конструктивную основу математики; Работа Мартина-Лёфа по теории типов повлияла на информатику . [4]
Пер Мартин-Лёф | |
---|---|
Родившийся | |
Национальность | Шведский |
Гражданство | Швеция |
Альма-матер | Стокгольмский университет |
Известен | Случайные последовательности Точные тесты Повторяющаяся структура Достаточная статистика Метод максимизации ожиданий Теория типа Мартина-Лёфа |
Награды | Премия Шведской королевской академии наук имени Рольфа Шока (2020) |
Научная карьера | |
Поля | Компьютерные науки Логика Математическая статистика Философия |
Учреждения | Стокгольмский университет Чикагский университет Орхусский университет |
Докторант | Андрей Николаевич Колмогоров |
До выхода на пенсию в 2009 году [5] Пер Мартин-Лёф занимал совместную кафедру математики и философии в Стокгольмском университете . [6]
Его брат Андерс Мартин-Лёф в настоящее время является заслуженным профессором математической статистики Стокгольмского университета; два брата сотрудничали в исследованиях в области вероятности и статистики. Исследования Андерса и Пера Мартин-Лёфа повлияли на статистическую теорию, особенно в отношении экспоненциальных семейств , метода максимизации ожидания для недостающих данных и выбора модели . [7]
Пер Мартин-Лёф - увлеченный орнитолог ; его первая научная публикация была посвящена смертности окольцованных птиц . [8]
Случайность и колмогоровская сложность
В 1964 и 1965 годах Мартин-Лёф учился в Москве у Андрея Н. Колмогорова . В 1966 году он написал статью «Определение случайных последовательностей», в которой было дано первое подходящее определение случайной последовательности. [9]
Ранее исследователи, такие как Ричард фон Мизес, пытались формализовать понятие теста на случайность , чтобы определить случайную последовательность как последовательность, которая прошла все тесты на случайность; однако точное понятие теста на случайность осталось неясным. Ключевой вывод Мартина-Лёфа заключался в использовании теории вычислений для формального определения понятия теста на случайность. Это контрастирует с идеей случайности в вероятности ; в этой теории ни один конкретный элемент выборочного пространства нельзя назвать случайным.
С тех пор было показано, что случайность Мартина-Лёфа допускает множество эквивалентных характеристик - в терминах сжатия , тестов на случайность и азартных игр - которые внешне мало похожи на исходное определение, но каждая из которых удовлетворяет нашему интуитивному представлению о свойствах, которым должны обладать случайные последовательности. имеют: случайные последовательности должны быть несжимаема, то они должны пройти статистические тесты на случайность, и это должно быть невозможно , чтобы заработать деньги ставки на них. Существование этих множественных определений случайности Мартина-Лёфа и стабильность этих определений при различных моделях вычислений свидетельствуют о том, что случайность Мартина-Лёфа является фундаментальным свойством математики, а не случайностью конкретной модели Мартина-Лёфа. Тезис о том , что определение Мартина-LOF случайности «правильно» захваты интуитивного понятие случайности было названо «Мартин-Löf- Хайтина Thesis»; он чем-то похож на тезис Черча – Тьюринга . [10]
Следуя работе Мартина-Лёфа, алгоритмическая теория информации определяет случайную строку как строку, которая не может быть получена из любой компьютерной программы, которая короче строки ( случайность Чайтина – Колмогорова ); т.е. строка, колмогоровская сложность которой не меньше длины строки. Это значение отличается от использования термина в статистике. В то время как статистическая случайность относится к процессу, который создает строку (например, подбрасывание монеты для получения каждого бита случайным образом дает строку), алгоритмическая случайность относится к самой строке . Теория алгоритмической информации отделяет случайные от неслучайных строк способом, который относительно инвариантен к используемой модели вычислений .
Алгоритмический случайная последовательностью является бесконечной последовательностью символов, у которых все префиксы ( за исключением , возможно , конечным числа исключений) являются строками, которые «близко к» алгоритмический случайной (их длине находится в пределах постоянная их сложность Колмогорова).
Математическая статистика
Пер Мартин-Лёф провел важные исследования в области математической статистики , которая (в шведской традиции) включает теорию вероятностей и статистику .
Наблюдение за птицами и определение пола
Пер Мартин-Лёф начал наблюдать за птицами в юности и до сих пор увлечен орнитологом. [11] В подростковом возрасте он опубликовал в шведском зоологическом журнале статью об оценке уровня смертности птиц с использованием данных кольцевания птиц. Вскоре эта статья стала цитироваться в ведущих международных журналах, и эту статью продолжают цитировать. [8] [12]
В биологии и статистике из птиц , есть несколько проблем недостающих данных . В первой статье Мартина-Лёфа обсуждалась проблема оценки уровня смертности видов чернозобиков с использованием методов отлова-повторной отлова . Вторая проблема отсутствия данных возникает при изучении пола птиц. Чрезвычайно сложная для человека проблема определения биологического пола птицы - один из первых примеров в лекциях Мартина-Лёфа по статистическим моделям .
Вероятность на алгебраических структурах
Мартин-Лёф написал докторскую диссертацию о вероятности алгебраических структур, в частности, полугрупп, в рамках исследовательской программы, возглавляемой Ульфом Гренандером из Стокгольмского университета. [13] [14] [15]
Статистические модели
Мартин-Лёф разработал новаторские подходы к статистической теории . В своей статье «О таблицах случайных чисел» Колмогоров заметил, что понятие вероятности частоты предельных свойств бесконечных последовательностей не может обеспечить основу для статистики, которая рассматривает только конечные выборки. [16] Большая часть работы Мартина-Лёфа в области статистики заключалась в том, чтобы обеспечить основу для статистики на основе конечных выборок.
Выбор модели и проверка гипотез
В 1970-х годах Пер Мартин-Лёф внес важный вклад в статистическую теорию и вдохновил на дальнейшие исследования, особенно скандинавских статистиков, в том числе Рольфа Сундберга, Томаса Хёглунда и Штеффана Лауритцена. В этой работе предыдущее исследование Мартина-Лёфа вероятностных мер на полугруппах привело к понятию «повторяющейся структуры» и новому подходу к достаточной статистике, в котором были охарактеризованы однопараметрические экспоненциальные семейства . Он представил теоретико-категориальный подход к вложенным статистическим моделям с использованием принципов конечной выборки. До (и после) Мартина-Лёфа такие вложенные модели часто тестировались с использованием тестов гипотез хи-квадрат, обоснования которых носят только асимптотический характер (и поэтому не имеют отношения к реальным задачам, которые всегда имеют конечные выборки). [16]
Метод максимизации ожидания для экспоненциальных семейств
Студент Мартина-Лёфа, Рольф Сундберг, разработал подробный анализ метода максимизации ожидания (EM) для оценки с использованием данных из экспоненциальных семейств, особенно с отсутствующими данными . Сундберг приписывает формулу, позже известную как формула Сундберга, предыдущим рукописям братьев Мартин-Лёф, Пера и Андерса . [17] [18] [19] [20] Многие из этих результатов достигли международного научного сообщества через 1976 документ о ожидании максимизации методы (EM) по Артуру П. Демпстеру , Nan Laird и Дональд Рубину , который был опубликован в ведущий международный журнал, спонсируемый Королевским статистическим обществом . [21]
Логика
Философская логика
В области философской логики Пер Мартин-Лёф опубликовал статьи по теории логических следствий , суждений и т. Д. Он интересовался центральноевропейскими философскими традициями, особенно немецкоязычными произведениями Франца Брентано , Готлоба Фреге и других авторов. Эдмунд Гуссерль .
Теория типов
Мартин-Лёф много десятилетий занимается математической логикой .
С 1968 по 69 год он работал доцентом в Чикагском университете, где познакомился с Уильямом Элвином Ховардом, с которым обсудил вопросы, связанные с перепиской Карри-Ховарда . Первый черновой вариант статьи Мартина-Лёфа по теории типов датируется 1971 годом. Эта импредикативная теория обобщает Систему F Жирара . Однако эта система оказалась непоследовательной из-за парадокса Жирара, который был обнаружен Жираром при изучении Системы U, непоследовательного расширения Системы F. Этот опыт привел Пера Мартина-Лёфа к разработке философских основ теории типов , его объяснения смысла , форма теоретико-доказательной семантики , которая оправдывает теорию предикативных типов, представленную в его книге Bibliopolis 1984 года, и расширенную в ряде все более философских текстов, таких как его влиятельные « О значениях логических констант и обоснования логических законов» .
Теория типов 1984 года была экстенсиональной, в то время как теория типов, представленная в книге Нордстрёма и др. в 1990 году, на которую сильно повлияли его более поздние идеи, интенсиональные и более подходящие для реализации на компьютере.
Интуиционистская теория типов Мартина-Лёфа развила понятие зависимых типов и напрямую повлияла на развитие исчисления конструкций и логической основы LF . Ряд популярных компьютерных систем доказательства основаны на теории типов, например NuPRL , LEGO, Coq , ALF, Agda , Twelf , Epigram и Idris .
Награды
Мартин-Лёф является членом Шведской королевской академии наук [22] и Academia Europaea . [6]
Смотрите также
- Франц Брентано
- Рудольф Карнап
- Майкл Даммит
- Готтлоб Фреге
- Ульф Гренандер
- Яакко Хинтикка
- Эдмунд Гуссерль
- Андрей Николаевич Колмогоров
- Андерс Мартин-Лёф
- Джон фон Нейман
- Питер Пагин
- Даг Правиц
- Чарльз Сандерс Пирс
- Фрэнк П. Рэмси
- Бертран Рассел
- Дана Скотт
- Альфред Тарский
- Алан Тьюринг
Заметки
- ↑ The International Who's Who: 1996-97 , Europa Publications, 1996, стр. 1020: «Мартин-Лёф, Пер Эрик Рутгер».
- ^ Обеспечивает ли HoTT основу для математики? Джеймс Лэдман (Бристольский университет, Великобритания)
- ^ Питер Дайбьер о типах и тестировании - Подкаст The Type Theory
- ^ См., Например, Nordström, Bengt; Петерссон, Кент; Смит, Ян М. (1990), Программирование в теории типов Мартина-Лёфа: Введение (PDF) , Oxford University Press.
- ^ Философия и основы математики: эпистемологические и онтологические аспекты. Конференция, посвященная Перу Мартин-Лёфу по случаю его выхода на пенсию. Архивировано 2 февраля 2014 г. в Wayback Machine . Swedish Collegium for Advanced Study, Уппсала, 5–8 мая 2009 г. Источник: 26 января 2014 г.
- ^ a b Профиль участника , Academia Europaea , получено 26 января 2014 г.
- ^ Подробнее см. В разделе # Статистические модели этой статьи.
- ^ а б Мартин-Лёф (1961) .
- ^ Мартин-Лёф, Пер (1966). «Определение случайных последовательностей» . Информация и контроль . 9 (6): 602–619. DOI : 10.1016 / S0019-9958 (66) 80018-9 .
- ^ Жан-Поль Делахай , Случайность, непредсказуемость и отсутствие порядка , в философии вероятности , с. 145–167, Springer 1993.
- ↑ Джордж А. Барнард , "Gone Birdwatching" , New Scientist , 4 декабря 1999 г., выпуск журнала 2215.
- ^ С. М. Тейлор (1966). «Недавние количественные исследования британских популяций птиц. Обзор». Журнал Королевского статистического общества, серия D . 16 (= № 2): 119–170. JSTOR 2986734 .
- ^ Мартин-Лёф, П. Теорема непрерывности на локально компактной группе. Теор. Вероятность. и Применен. 10 1965 367–371.
- ^ Мартин-Лёф, Пер Теория вероятностей на дискретных полугруппах. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 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 учебном году) при содействии Рольфа Сундберга. Стокгольмский университет. («Формула Сундберга»)
- ^ Демпстер, AP ; Лэрд, Нью-Мексико ; Рубин, ДБ (1977). «Максимальная вероятность неполных данных с помощью алгоритма EM». Журнал Королевского статистического общества, Series B . 39 (1): 1–38. JSTOR 2984875 . Руководство по ремонту 0501537 .
- ^ «Шведская королевская академия наук: Пер Мартин-Лёф» . Проверено 1 мая 2009 .[ мертвая ссылка ]
Рекомендации
Наблюдение за птицами и недостающие данные
- Мартин-Лёф, П. (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.
- Мартин-Лёф, П. Понятие избыточности и его использование в качестве количественной меры отклонения между статистической гипотезой и набором данных наблюдений. С обсуждением Ф. Абильдгарда, А. П. Демпстера , Д. Басу , Д. Р. Кокса , AWF Эдвардса , Д. А. Спротта, Г. А. Барнарда , О. Барндорфф-Нильсена, Дж. Д. Калбфляйша и Г. Раша и ответом автора. Труды конференции по основополагающим вопросам статистического вывода (Орхус, 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 с. 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.
Внешние ссылки
- Пер Мартин-Лёф из проекта « Математическая генеалогия»