Хаскелл Брукс Карри ( / ˈ h æ s k əl / ; 12 сентября 1900 — 1 сентября 1982) — американский математик и логик . Карри наиболее известен своей работой в области комбинаторной логики , первоначальная концепция которой основана на статье Мозеса Шёнфинкеля [1] , для которой Карри внес большую часть разработок. Карри также известен парадоксом Карри и перепиской Карри-Ховарда . В его честь названы три языка программирования : Haskell , Brook и Curry , а также концепция каррирования — метода преобразования функций, используемого в математике и информатике .
Карри родился 12 сентября 1900 года в Миллисе, штат Массачусетс , в семье Сэмюэля Сайласа Карри и Анны Барайт Карри , которые руководили школой ораторского искусства . Он поступил в Гарвардский университет в 1916 году, чтобы изучать медицину, но переключился на математику, прежде чем окончил его в 1920 году. После двух лет работы в аспирантуре по электротехнике в Массачусетском технологическом институте (MIT) он вернулся в Гарвард, чтобы изучать физику , получив степень магистра искусств ( MA) в 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 года (в возрасте 81 года) в Государственном колледже, штат Пенсильвания.
В центре внимания работы Карри были попытки показать, что комбинаторная логика может стать основой математики. К концу 1933 года он узнал о парадоксе Клини-Россера из переписки с Джоном Россером . Парадокс, разработанный Россером и Стивеном Клин , доказал несогласованность ряда связанных формальных систем , в том числе системы, предложенной Алонзо Чёрчем (система, в которой лямбда-исчисление было последовательной подсистемой) и собственной системы Карри. [2] Однако, в отличие от Чёрча, Клини и Россера, Карри не отказался от основополагающего подхода, заявив, что он не хочет «убегать от парадоксов». [3]
Работая в области комбинаторной логики на протяжении всей своей карьеры, Карри, по сути, стал основателем и самым известным человеком в этой области. Комбинаторная логика является основой одного стиля функционального языка программирования . Мощь и возможности комбинаторной логики очень похожи на лямбда -исчисление Чёрча, и последний формализм имел тенденцию преобладать в последние десятилетия.
В 1947 году Карри также описал один из первых языков программирования высокого уровня и впервые описал процедуру преобразования общего арифметического выражения в код для одноадресного компьютера. [4]
Он преподавал в Гарварде, Принстоне , а с 1929 по 1966 год — в Университете штата Пенсильвания . В 1942 году он опубликовал парадокс Карри . В 1966 году он стал профессором логики и ее истории и философии точных наук в Амстердамском университете , преемником Эверта Виллема Бета . [5]
Карри также писал и преподавал математическую логику в более общем плане; его преподавание в этой области завершилось в 1963 году его « Основами математической логики» . Его любимой философией математики был формализм (см. его книгу 1951 года), следуя за его наставником Гильбертом, но его работы демонстрируют существенную философскую любознательность и очень непредвзятость в отношении интуиционистской логики .
Статья, основавшая комбинаторную логику. Английский перевод: Шёнфинкель (1967)