Пер Мартин Лёф: Логик, философ и статистик

Мартин Лёф: шведский логик, философ и математик. Основы вероятности, статистики, логики и информатики. Интуиционистская теория типов и её влияние.

11 мин чтения

100%

Источник: Per Martin-Löf — Wikipedia

Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.

Содержание

Введение

Шведский логик, философ и математический статистик

Пер Эрик Рутгер Мартин Лёф (/l//ɒ//f/; родился 8 мая 1942) — шведский логик, философ и математический статистик. Он всемирно известен своими работами в области теории вероятностей, статистики, математической логики и информатики. С конца 1970-х годов публикации Мартина Лёфа касались преимущественно логики. В философской логике Мартин Лёф занимался вопросами философии логического следования и суждений, отчасти вдохновлённый работами Брентано, Фреге и Гуссерля. В математической логике Мартин Лёф активно развивал интуиционистскую теорию типов как конструктивное основание математики; работы Мартина Лёфа по теории типов оказали влияние на информатику. До выхода на пенсию в 2009 году Пер Мартин Лёф занимал совместную должность профессора математики и философии в Стокгольмском университете. Его брат Андерс Мартин Лёф в настоящее время является профессором математической статистики в отставке в Стокгольмском университете; оба брата сотрудничали в исследованиях в области теории вероятностей и статистики. Исследования Андерса и Пер Мартина Лёфа оказали влияние на статистическую теорию, особенно в отношении экспоненциальных семей, метода максимизации ожидания для работы с пропущенными данными и выбора моделей. Пер Мартин Лёф получил степень доктора философии в 1970 году в Стокгольмском университете под руководством Андрея Колмогорова. Мартин Лёф — увлечённый орнитолог; его первая научная публикация была посвящена показателям смертности кольцеванных птиц.

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

В 1964 и 1965 годах Мартин Лёф учился в Москве под руководством Андрея Н. Колмогорова. В 1966 году он опубликовал статью "Определение случайных последовательностей", в которой было дано первое адекватное определение случайной последовательности. Более ранние исследователи, такие как Ричард фон Мизес, пытались формализовать понятие теста на случайность, чтобы определить случайную последовательность как ту, которая проходит все тесты на случайность; однако само понятие теста на случайность оставалось нечетким. Ключевым прозрением Мартина Лёфа стало использование теории вычислений для формального определения теста на случайность. Это отличается от понимания случайности в теории вероятностей, где ни один конкретный элемент пространства элементарных событий не может считаться случайным. С тех пор было показано, что случайность Мартина Лёфа имеет множество эквивалентных характеристик – с точки зрения сжатия, тестов на случайность и азартных игр – которые мало похожи на исходное определение, но каждая из которых соответствует нашему интуитивному представлению о свойствах, которыми должны обладать случайные последовательности: случайные последовательности должны быть несжимаемыми, они должны проходить статистические тесты на случайность, и на них нельзя стабильно выигрывать, делая ставки. Существование этих множественных определений случайности Мартина Лёфа и стабильность этих определений при различных моделях вычислений свидетельствуют о том, что случайность Мартина Лёфа является фундаментальным свойством математики, а не артефактом конкретной модели Лёфа. Утверждение о том, что определение случайности Мартина Лёфа "корректно" отражает интуитивное понятие случайности, называется "Тезисом Лёфа — Чейтина"; оно в некоторой степени аналогично тезису Черча — Тьюринга. После работы Мартина Лёфа алгоритмическая теория информации определяет случайную строку как строку, которую нельзя получить из какой-либо компьютерной программы, короче самой строки (случайность Колмогорова — Чейтина); то есть строку, чья сложность Колмогорова не меньше длины строки. Это отличается от использования этого термина в статистике. В то время как статистическая случайность относится к процессу, порождающему строку (например, подбрасывание монеты для получения каждого бита случайным образом создаст строку), алгоритмическая случайность относится к самой строке. Алгоритмическая теория информации разделяет случайные и неслучайные строки таким образом, что это разделение относительно инвариантно к используемой модели вычислений. Алгоритмически случайная последовательность — это бесконечная последовательность символов, все префиксы которой (за исключением, возможно, конечного числа исключений) являются строками, которые "близки" к алгоритмически случайным (их длина отличается от их сложности Колмогорова на константу).

In 1964 and 1965, Martin Löf studied in Moscow under the supervision of Andrei N. Kolmogorov. He wrote a 1966 article The definition of random sequences that gave the first suitable definition of a random sequence. Earlier researchers such as Richard von Mises had attempted to formalize the notion of a test for randomness in order to define a random sequence as one that passed all tests for randomness; however, the precise notion of a randomness test was left vague. Martin Löf's key insight was to use the theory of computation to define formally the notion of a test for randomness. This contrasts with the idea of randomness in probability; in that theory, no particular element of a sample space can be said to be random. Martin Löf randomness has since been shown to admit many equivalent characterizations — in terms of compression, randomness tests, and gambling — that bear little outward resemblance to the original definition, but each of which satisfies our intuitive notion of properties that random sequences ought to have: random sequences should be incompressible, they should pass statistical tests for randomness, and it should be impossible to make money betting on them. The existence of these multiple definitions of Martin Löf randomness, and the stability of these definitions under different models of computation, give evidence that Martin Löf randomness is a fundamental property of mathematics and not an accident of Martin Löf's particular model. The thesis that the definition of Martin Löf randomness "correctly" captures the intuitive notion of randomness has been called the "Martin Löf–Chaitin Thesis"; it is somewhat similar to the Church–Turing thesis. Following Martin Löf's work, algorithmic information theory defines a random string as one that cannot be produced from any computer program that is shorter than the string (Chaitin–Kolmogorov randomness); i. e. a string whose Kolmogorov complexity is at least the length of the string. This is a different meaning from the usage of the term in statistics. Whereas statistical randomness refers to the process that produces the string (e. g. flipping a coin to produce each bit will randomly produce a string), algorithmic randomness refers to the string itself. Algorithmic information theory separates random from nonrandom strings in a way that is relatively invariant to the model of computation being used. An algorithmically random sequence is an infinite sequence of characters, all of whose prefixes (except possibly a finite number of exceptions) are strings that are "close to" algorithmically random (their length is within a constant of their Kolmogorov complexity).

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

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

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

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

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

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

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

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

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

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

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

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

Теория типов

Мартин Лёф много десятилетий работал в области математической логики. С 1968 по 1969 год он работал ассистентом профессора в Чикагском университете, где встретил Уильяма Элвина Говарда, с которым обсуждал вопросы, связанные с корреспонденцией Кэрри-Ховарда. Первый проект статьи Мартина Лёфа о теории типов датируется 1971 годом. Эта непредсказуемая теория обобщила систему F Жирара. Однако эта система оказалась противоречивой из-за парадокса Жирара, который был обнаружен Жираром при изучении системы U, противоречивого расширения системы F. Этот опыт побудил Пер Мартина Лёфа разработать философские основы теории типов, его объяснение смысла, форму теоретико-доказательной семантики, которая обосновывает предикативную теорию типов, представленную в его книге Bibliopolis 1984 года, и расширенную в ряде все более философских текстов, таких как его влиятельные работы «О значениях логических констант» и «Обоснование логических законов». Теория типов 1984 года была экстенсиональной, в то время как теория типов, представленная в книге Нордстрема и др. в 1990 году, которая находилась под сильным влиянием его более поздних идей, была интенсиональной и более пригодной для реализации на компьютере. Интуиционистская теория типов Мартина Лёфа развила понятие зависимых типов и оказала непосредственное влияние на развитие исчисления конструкций и логической структуры LF. Ряд популярных компьютерных систем доказательства теорем основаны на теории типов, например, NuPRL, LEGO, Coq, ALF, Agda, Twelf, Epigram и Idris.

Награды

Мартин Лёф является членом Королевской шведской академии наук (избран в 1990 году) и Академии Европы (избран в 1989 году).

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

Джордж А. Барнард, «Увлечение наблюдением за птицами», New Scientist, 4 декабря 1999 года, номер журнала 2215.

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

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

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

Гренандер, Ульф. Вероятность на алгебраических структурах. (Переиздание Dover)
Мартин Лёф, П. Теорема о непрерывности для локально компактной группы. Теория вероятностей и ее применения. 10, 1965, 367–371.
Мартин Лёф, Пер. Теория вероятностей на дискретных полугруппах. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete. 4, 1965, 78–102.
Нитиш Мухопадхьяй. "Беседа с Ульфом Гренандeром". Statist. 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, Отдел теоретической статистики, Институт математики, Орхусский университет, Орхус, 1974. Мартин Лёф, П. Рекурсивные структуры и связь между каноническим и микроканоническим распределениями в статистике и статистической механике. С обсуждением Д. Р. Кокса и Г. Раша и ответом автора. Материалы конференции по фундаментальным вопросам статистического вывода (Аархус, 1973), с. 271–294. Мемуары, № 1, Отдел теоретической статистики, Институт математики, Орхусский университет, Орхус, 1974. Мартин Лёф, П. Понятие избыточности и его использование в качестве количественной меры отклонения между статистической гипотезой и набором наблюдательных данных. С обсуждением Ф. Абильдгард, А. П. Демпстера, Д. Басу, Д. Р. Кокса, А. В. Ф. Эдвардса, Д. А. Спротта, Г. А. Барнарда, О. Барндорфа Нильсена, Дж. Д. Калбфлейша и Г. Раша и ответом автора. Материалы конференции по фундаментальным вопросам статистического вывода (Аархус, 1973), с. 1–42. Мемуары, № 1, Отдел теоретической статистики, Институт математики, Орхусский университет, Орхус, 1974. Мартин Лёф, Пер. Понятие избыточности и его использование в качестве количественной меры несоответствия между статистической гипотезой и набором наблюдательных данных. Scand. J. Statist. 1 (1974), № 1, 3–18. Свердруп, Эрлинг. "Тесты без мощности". Scand. J. Statist. 2 (1975), № 3, 158–160. Мартин Лёф, Пер. Ответ на полемическую статью Эрлинга Свердрупа: "Тесты без мощности" (Scand. J. Statist. 2 (1975), № 3, 158–160). Scand. J. Statist. 2 (1975), № 3, 161–165. Свердруп, Эрлинг. Ответ на: "Тесты без мощности" (Scand. J. Statist. 2 (1975), 161–165) П. Мартина Лёфа. Scand. J. Statist. 4 (1977), № 3, 136–138. Мартин Лёф, П. Точные тесты, доверительные интервалы и оценки. Основы теории вероятностей и статистики. II. Synthese 36 (1977), № 2, 195–206. Рольф Сундберг. 1971. Теория максимального правдоподобия и приложения для распределений, генерируемых при наблюдении функции экспоненциальной переменной. Диссертация, Институт математической статистики, Стокгольмский университет. Сундберг, Рольф. Теория максимального правдоподобия для неполных данных из экспоненциального семейства. Scand. J. Statist. 1 (1974), № 2, 49–58. Сундберг, Рольф. Итеративный метод решения уравнений правдоподобия для неполных данных из экспоненциальных семейств. Comm. Statist.—Simulation Comput. B5 (1976), № 1, 55–64. Сундберг, Рольф. Некоторые результаты о декомпозируемых (или марковского типа) моделях для многомерных таблиц сопряженности: распределение маржиналов и разбиение тестов. Scand. J. Statist. 2 (1975), № 2, 71–79. Хёглунд, Томас. Точная оценка — метод статистической оценки. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29 (1974), 257–271. Лауритцен, Стеффен Л. Экстремальные семейства и системы достаточной статистики. Lecture Notes in Statistics, 49. Springer Verlag, Нью-Йорк, 1988. xvi+268 с.

Anders Martin Löf. 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Evaluation of lifetimes in time lengths below one nanosecond"). ("Sundberg formula", according to Sundberg 1971)
Per Martin Löf. 1966. Statistics from the point of view of statistical mechanics. Lecture notes, Mathematical Institute, Aarhus University. ("Sundberg formula" credited to Anders Martin Löf, according to Sundberg 1971)
Per Martin Löf. 1970. Statistika Modeller (Statistical Models): Anteckningar fran seminarier läsåret 1969–1970 (Notes from seminars in the academic year 1969–1970), with the assistance of Rolf Sundberg. Stockholm University. Martin Löf, P. "Exact tests, confidence regions and estimates", with a discussion by A. W. F. Edwards, G. A. Barnard, D. A. Sprott, O. Barndorff Nielsen, D. Basu and G. Rasch. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), pp. 121–138. Memoirs, No. 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974. Martin Löf, P. Repetitive structures and the relation between canonical and microcanonical distributions in statistics and statistical mechanics. With a discussion by D. R. Cox and G. Rasch and a reply by the author. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), pp. 271–294. Memoirs, No. 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974. Martin Löf, P. The notion of redundancy and its use as a quantitative measure of the deviation between a statistical hypothesis and a set of observational data. With a discussion by F. Abildgård, A. P. Dempster, D. Basu, D. R. Cox, A. W. F. Edwards, D. A. Sprott, G. A. Barnard, O. Barndorff Nielsen, J. D. Kalbfleisch and G. Rasch and a reply by the author. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), pp. 1–42. Memoirs, No. 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974. Martin Löf, Per The notion of redundancy and its use as a quantitative measure of the discrepancy between a statistical hypothesis and a set of observational data. Scand. J. Statist. 1 (1974), no. 1, 3—18. Sverdrup, Erling. "Tests without power." Scand. J. Statist. 2 (1975), no. 3, 158–160. Martin Löf, Per Reply to Erling Sverdrup's polemical article: Tests without power (Scand. J. Statist. 2 (1975), no. 3, 158–160). Scand. J. Statist. 2 (1975), no. 3, 161–165. Sverdrup, Erling. A rejoinder to: Tests without power (Scand. J. Statist. 2 (1975), 161—165) by P. Martin Löf. Scand. J. Statist. 4 (1977), no. 3, 136—138. Martin Löf, P. Exact tests, confidence regions and estimates. Foundations of probability and statistics. II. Synthese 36 (1977), no. 2, 195—206. 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. Sundberg, Rolf. Maximum likelihood theory for incomplete data from an exponential family. Scand. J. Statist. 1 (1974), no. 2, 49—58. Sundberg, Rolf An iterative method for solution of the likelihood equations for incomplete data from exponential families. Comm. Statist.—Simulation Comput. B5 (1976), no. 1, 55—64. Sundberg, Rolf Some results about decomposable (or Markov type) models for multidimensional contingency tables: distribution of marginals and partitioning of tests. Scand. J. Statist. 2 (1975), no. 2, 71—79. Höglund, Thomas. The exact estimate — a method of statistical estimation. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29 (1974), 257—271. Lauritzen, Steffen L. Extremal families and systems of sufficient statistics. Lecture Notes in Statistics, 49. Springer Verlag, New York, 1988. xvi+268 pp.

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

Пер Мартин Лёф. Теория типов. Препринт, Стокгольмский университет, 1971. Пер Мартин Лёф. Интуиционистская теория типов. В Г. Самбине и Дж. Смите, редакторы, Двадцать пять лет конструктивной теории типов. Издательство Оксфордского университета, 1998. Перепечатанная версия неопубликованного доклада 1972 года. Пер Мартин Лёф. Интуиционистская теория типов: Предикативная часть. В H. E. Rose и J. C. Shepherdson, редакторы, Logic Colloquium ‘73, страницы 73–118. North Holland, 1975. Пер Мартин Лёф. Конструктивная математика и программирование на компьютерах. В Logic, Methodology and Philosophy of Science VI, 1979. Под редакцией Коэна и др. North Holland, Амстердам. С. 153–175, 1982. Пер Мартин Лёф. Интуиционистская теория типов. (Записи Джованни Самбина конспектов серии лекций, прочитанных в Падуе в июне 1980 г.). Неаполь, Bibliopolis, 1984. Пер Мартин Лёф. Философские следствия теории типов, Неопубликованные заметки, 1987? Пер Мартин Лёф. Исчисление подстановок, 1992. Записи с лекции, прочитанной в Гётеборге. Бенгт Нордстрём, Кент Петерссон и Ян М. Смит. Программирование в теории типов Мартина Лёфа. Издательство Оксфордского университета, 1990. (Книга снята с печати, но бесплатная версия доступна.) Пер Мартин Лёф. О значениях логических констант и обосновании логических законов. Nordic Journal of Philosophical Logic, 1(1): 11–60, 1996. Пер Мартин Лёф. Логика и этика. В Т. Пиехе и П. Шредер-Хейстер, редакторы, Теоретическая семантика доказательств: оценка и перспективы развития. Материалы третьей Тюбингенской конференции по теоретической семантике доказательств, 27–30 марта 2019 г., страницы 227–235. URI: http://dx.doi.org/10.15496/publikation 35319. Университет Тюбингена, 2019.