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


Родился в Миллисе (штат Массачусетс), образование получил в Гарвардском университете. Диссертацию защитил в Гёттингене под руководством Гильберта (1930). Большую часть жизни проработал в Университете штата Пенсильвания.

С его именем связаны парадокс Карри и соответствие Карри — Ховарда, в его честь названы два языка программирования: Haskell и Curry, а также функциональная операция «каррирование», широко используемая в языках программирования.

Программа его исследований[4] способствовала становлению конструктивного подхода к выработке оснований математики. Существенно повлиял на развитие логики[5], способствовал формированию направления структурализма и формализма в метаматематике[6][7]. Разработал основы комбинаторной логики, которая, в свою очередь, явилась стимулом становления нескольких парадигм программирования, среди которых аппликативное и функциональное программирование.

Называя свою систему «конструктивным неоформализмом», Карри не принимает некоторые положения классического формализма Д. Гильберта. Так он делает послабление в отношении требования непротиворечивости, которое Д. Гильберт считал основным свойством системы аксиом. «Зачем, — спрашивает он, — скажем, нам так уж нужно быть уверенными в непротиворечивости теории … прежде, чем использовать эту теорию? Ведь ни к какой другой науке мы не предъявляем таких требований. В физике, например, теории всегда гипотетичны; мы принимаем теорию, коль скоро на её основе можно делать полезные предсказания, и видоизменяем или отвергаем её коль скоро этого сделать нельзя». Доля истины в этом, конечно, есть. Если установлено, что система аксиом противоречива, то такая система не имеет ценности, но начинать проверку системы аксиом можно и не с проверки её непротиворечивости, а с применения системы на деле.

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