Хаскелл Карри

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

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

Жизнь

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

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

Хаскелл Карри умер 1 сентября 1982 года (1982-09-01) (81 год) в Государственном колледже, Пенсильвания.

Работа

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

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

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

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

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

Основные публикации

• «Grundlagen der Kombinatorischen Logik» [Основы комбинаторной логики]. Американский журнал математики (на немецком языке). 52 (3). Издательство Университета Джонса Хопкинса: 509–536. 1930. дои : 10.2307/2370619 . JSTOR   2370619 .
• Теория формальной выводимости . Издательство Университета Нотр-Дам. 1950.
  • Теория формальной выводимости (2-е изд.). Издательство Университета Нотр-Дам. 1957.
• Очертания формалистической философии математики . Амстердам: Elsevier Science. 1951. ISBN  0444533680 . Проверено 23 июля 2012 г.
• Уроки алгебраической логики (на французском языке). Париж: Готье-Виллар. 1952.
• Карри, Хаскелл Брукс ; Фейс, Роберт (1958). Комбинаторная логика . Том. I. Амстердам: Издательство Северной Голландии . ISBN  0-7204-2208-6 .
• Основы математической логики . Макгроу Хилл. 1963.
  • Основы математической логики (Полное и исправленное изд. Дувра). Нью-Йорк: Dover Publications. 1977. ISBN  0-486-63462-0 . Проверено 23 июля 2012 г.
• Карри, Хаскелл Брукс ; Хиндли, Дж. Роджер ; Селдин, Джонатан П. (1972). Комбинаторная логика . Том. II. Амстердам: Северная Голландия. ISBN  0-7204-2208-6 .

Дальнейшее чтение

• Селдин и Хиндли (1980) — включает биографический очерк.

Ссылки

• Барендрегт, Хендрик Питер (1984). Лямбда-исчисление, его синтаксис и семантика. Исследования по логике и основам математики . Том. 103. Северная Голландия . ISBN  0-444-87508-5 .
• Кнут, Дональд Эрвин ; Пардо, Луис Трабб (1976). Раннее развитие языков программирования . Стэнфордский университет, факультет компьютерных наук.
• Маркус, Р. Баркан (1952). «Обзор: Leçons de logique algébrique , Х. Б. Карри» . Бюллетень Американского математического общества . 58 (2): 673–674. дои : 10.1090/s0002-9904-1952-09657-9 .
• Нельсон, Д. (1952). «Обзор: теория формальной выводимости Х. Б. Карри» . Бюллетень Американского математического общества . 58 (3): 415–417. дои : 10.1090/s0002-9904-1952-09596-3 .
• Шенфинкель, Моисей (1924). «О строительных блоках математической логики» (PDF) . Математические анналы (на немецком языке). 92 (3–4): 305–316. дои : 10.1007/bf01448013 . S2CID   118507515 . Статья, положившая начало комбинаторной логике. Английский перевод: Шенфинкель (1967)
• Шенфинкель, Моисей (1967) [1924]. Ван Хейеноорт, Жан (ред.). строительных блоках логики математической О От Фреге до Гёделя: справочник по математической логике, 1879–1931. Перевод Бауэра-Менгельберга, Стефана. Кембридж, Массачусетс, США: Издательство Гарвардского университета . стр. 355–366. ISBN  978-0674324497 . OCLC   503886453 .
• Селдин, Джонатан П.; Хиндли-младший, ред. (1980). Х.Б. Карри: Очерки по комбинаторной логике, лямбда-исчислению и формализму . Академическая пресса.
• Селдин, Джонатан П. (3 марта 2008 г.). «Логика Карри и Черча» (PDF) . Проверено 23 сентября 2023 г.

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

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