Хаскелл Брукс Карри ( / ˈ h æ s k əl / HAS -kəl ; 12 сентября 1900 — 1 сентября 1982) был американским математиком и логиком . Карри наиболее известен своей работой в комбинаторной логике , чья первоначальная концепция основана на статье Моисея Шёнфинкеля , [1] для которой Карри сделал большую часть разработки. Карри также известен парадоксом Карри и соответствием Карри–Говарда . В его честь названы три языка программирования : Haskell , Brook и Curry , а также концепция каррирования , метода преобразования функций, используемого в математике и информатике .
Карри родился 12 сентября 1900 года в Миллисе, штат Массачусетс , в семье Сэмюэля Сайласа Карри и Анны Барайт Карри , которая руководила школой ораторского искусства . Он поступил в Гарвардский университет в 1916 году, чтобы изучать медицину, но переключился на математику до окончания университета в 1920 году. После двух лет аспирантуры по электротехнике в Массачусетском технологическом институте (MIT) он вернулся в Гарвард, чтобы изучать физику , получив степень магистра искусств (MA) в 1924 году. Интерес Карри к математической логике начался в этот период, когда он познакомился с Principia Mathematica , попыткой Альфреда Норта Уайтхеда и Бертрана Рассела обосновать математику в символической логике. Оставаясь в Гарварде, Карри получил степень доктора философии (Ph.D.) по математике. В то время как Джордж Дэвид Биркгоф направлял его на работу над дифференциальными уравнениями , его интересы продолжали смещаться в сторону логики. В 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)