Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Хаскелл Брукс Карри
HaskellBCurry.jpg
Родившийся( 1900-09-12 )12 сентября 1900 г.
Миллис, Массачусетс , США
Умер1 сентября 1982 г. (1982-09-01)(81 год)
Государственный колледж, Пенсильвания , США
НациональностьАмериканец
Альма-матер
ИзвестенКомбинаторная логика
Соответствие Карри – Ховарда
Парадокс Карри
Формализм в философии математики
Научная карьера
ПоляМатематика
логика
УчрежденияГосударственный университет Пенсильвании,
Амстердамский университет
ДокторантДэвид Гильберт
ВлиянияАльфред Норт Уайтхед
Бертран Рассел
Мозес Шенфинкель

Haskell Brooks Curry ( / ч æ s к əl / ; 12 сентября 1900 - 1 сентября 1982) был американский математик и логик . Карри наиболее известен своими работами по комбинаторной логике . Хотя первоначальная концепция комбинаторной логики была основана на одной бумаге Шейнфинкель , [1] Карри сделал большую часть развития. Карри также известен парадокс Карри и переписки Карри-Говарда . В его честь названы три языка программирования: Haskell , Brook.и Карри , а также концепция каррирования - техники, используемой для преобразования функций в математике и информатике.

Жизнь [ править ]

Карри родился 12 сентября 1900 года в Миллисе, штат Массачусетс , в семье Сэмюэля Сайласа Карри и Анны Барит Карри , которые руководили школой ораторского искусства . Он поступил в Гарвардский университет в 1916 году, чтобы изучать медицину, но переключился на математику, прежде чем получить диплом в 1920 году. После двух лет работы в магистратуре в области электротехники в Массачусетском технологическом институте он вернулся в Гарвард, чтобы изучать физику, получив степень магистра в 1924 году. Карри начал интересоваться математической логикой. в этот период, когда он познакомился с Principia Mathematica , попытка Альфреда Норта Уайтхеда и Бертрана Расселачтобы основать математику на символической логике. Оставаясь в Гарварде, Карри защитила докторскую диссертацию. по математике. Хотя Джордж Дэвид Биркгоф направил его работать над дифференциальными уравнениями, его интересы продолжали смещаться в сторону логики. В 1927 году, будучи преподавателем в Принстонском университете, он открыл для себя работы Моисея Шенфинкеля по комбинаторной логике. Работа Шенфинкеля предвосхитила большую часть собственных исследований Карри, и, как следствие, он переехал в Геттингенский университет, где мог работать с Генрихом Беманом и Полем Бернейсом , которые были знакомы с работами Шенфинкеля. Карри руководил Дэвид Гильберти работал в тесном сотрудничестве с Бернейсом, получив докторскую степень. в 1930 г. защитил диссертацию по комбинаторной логике. [2]

В 1928 году перед отъездом в Геттинген Карри женился на Мэри Вирджиния Уитли. Пара жила в Германии, пока Карри защитил диссертацию, а затем, в 1929 году, перешел в Государственный колледж в Пенсильвании, где Карри поступил в Государственный колледж Пенсильвании . У них было двое детей, Энн Райт Карри (27 июля 1930 г.) и Роберт Уитли Карри (6 июля 1934 г.). Карри оставался в штате Пенсильвания в течение следующих 37 лет. В 1931–1932 годах он провел один год в Чикагском университете в рамках национальной исследовательской стипендии, а один год в 1938–1939 годах в Институте перспективных исследований в Принстоне. В 1942 году он взял отпуск, чтобы заниматься прикладной математикой для правительства США во время Второй мировой войны., особенно во Франкфордском Арсенале . Сразу после войны он работал над проектом ENIAC в 1945 и 1946 годах. По стипендии Фулбрайта он сотрудничал с Робертом Фейсом в Лувене , Бельгия. После ухода из Пенсильванского университета в 1966 году Карри устроился на работу в Амстердамский университет . В 1970 году, закончив второй том своего трактата по комбинаторной логике, Карри ушел из Амстердамского университета и вернулся в Государственный колледж в Пенсильвании.

Хаскелл Карри умер 1 сентября 1982 года в Государственном колледже штата Пенсильвания.

Работа [ править ]

В центре внимания работы Карри были попытки показать, что комбинаторная логика может стать основой математики. К концу 1933 года он узнал о парадоксе Клини – Россера из переписки с Джоном Россером . Парадокс, разработанный Россером и Стивеном Клини , доказал несостоятельность ряда связанных формальных систем, включая систему, предложенную Алонзо Черчем (система, в которой лямбда-исчисление было согласованной подсистемой) и собственной системы Карри. [2] Однако, в отличие от Черча, Клини и Россера, Карри не отказался от основополагающего подхода, заявив, что он не хочет «убегать от парадоксов». [3]

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

В 1947 году Карри также описал один из первых языков программирования высокого уровня и предоставил первое описание процедуры преобразования общего арифметического выражения в код для одноадресного компьютера. [4]

Он преподавал в Гарварде, Принстоне и с 1929 по 1966 год в Государственном университете Пенсильвании . В 1942 году он опубликовал парадокс Карри . В 1966 году он стал профессором логики и ее истории, а также философии точных наук в Амстердамском университете , преемнике Эверта Виллема Бета . [5]

Карри также писал и преподавал математическую логику в целом; его обучение в этой области достигло высшей точки в 1963 году, когда он написал «Основы математической логики» . Его любимой философией математики был формализм (см. Его книгу 1951 года), вслед за его наставником Гильбертом, но его труды выдают существенное философское любопытство и очень непредвзятое отношение к интуиционистской логике .

Основные публикации [ править ]

  • "Grundlagen der Kombinatorischen Logik" [Основы комбинаторной логики]. Американский журнал математики (на немецком языке). Издательство Университета Джона Хопкинса. 52 (3): 509–536. 1930. DOI : 10,2307 / 2370619 . JSTOR  2370619 .
  • Теория формальной выводимости . Университет Нотр-Дам Пресс. 1950 г.[6]
    • Теория формальной выводимости (2-е изд.). Университет Нотр-Дам Пресс. 1957 г.
  • Очертания формалистической философии математики . Амстердам: Elsevier Science. 1951. ISBN. 0444533680. Проверено 23 июля 2012 года .
  • Leçons de logique algébrique (на французском языке). Париж: Готье-Виллар. 1952 г.[7]
  • Карри, Хаскелл ; Фейс, Роберт (1958). Комбинаторная логика . Я . Амстердам: Издательская компания Северной Голландии.
  • Основы математической логики . Макгроу Хилл. 1963 г.
    • Основы математической логики (Несокращенное и исправленное Дуврское изд.). Нью-Йорк: Dover Publications. 1977. ISBN. 0-486-63462-0. Проверено 23 июля 2012 года .
  • Комбинаторная логика . II . Амстердам: Издательская компания Северной Голландии. 1972. ISBN. 0720422086.

Ссылки [ править ]

  1. ^ 1924. «Uber die Bausteine ​​der Mathematischen Logik», Mathematische Annalen 92 , стр. 305–316. Переведено Стефаном Бауэром-Менгельбергом как «О строительных блоках математической логики» Жана ван Хейеноорта , 1967. Справочник по математической логике, 1879–1931 . Harvard Univ. Пресс: 355–66.
  2. ^ a b Селдин, Джонатан. «Логика Карри и Черча». Cite journal requires |journal= (help)
  3. ^ Барендрегт, HP . Лямбда-исчисление: его синтаксис и семантика . Эльзевир. п. 4.
  4. ^ Кнут, Дональд Э .; Пардо, Луис Трабб (1976). «Раннее развитие языков программирования». Стэнфордский университет, факультет компьютерных наук, стр. 22
  5. ^ Альбом Academicum , Амстердамский университет
  6. Перейти ↑ Nelson, D. (1952). "Обзор: теория формальной выводимости , Х. Б. Карри" . Бык. Амер. Математика. Soc . 58 (3): 415–417. DOI : 10.1090 / s0002-9904-1952-09596-3 .
  7. ^ Маркус, Р. Баркан (1952). "Обзор: Leçons de logique algébrique , Х. Б. Карри" . Бык. Амер. Математика. Soc . 58 (2): 673–674. DOI : 10,1090 / s0002-9904-1952-09657-9 .

Дальнейшее чтение [ править ]

  • Селдин, Дж. П., и Хиндли, Дж. Р., ред., 1980. К Х. Б. Карри: Очерки комбинаторной логики, лямбда-исчисления и формализма . Академическая пресса. Включает биографический очерк.

Внешние ссылки [ править ]

  • Селдин, Джонатан П. "Хаскелл Брукс Карри (1900-1982)" . Интернет-энциклопедия философии .
  • О'Коннор, Джон Дж .; Робертсон, Эдмунд Ф. , "Haskell Curry" , архив истории математики MacTutor , Университет Сент-Эндрюс.
  • Архивы Карри предоставляют изображения нескольких сотен страниц рукописей с 1920 по 1931 год.
  • CLg. библиография 587 стр.