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

Хаскелл Брукс Карри (12 сентября 1900 — 1 сентября 1982) — американский математик и логик. Программа его исследований способствовала становлению конструктивного подхода к выработке оснований математики. Существенно повлиял на развитие логики, способствовал формированию направления структурализма и формализма в метаматематике. Разработал основы комбинаторной логики, которая, в свою очередь, явилась стимулом становления нескольких парадигм программирования, среди которых аппликативное и функциональное программирование.

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

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

Логические труды

Понятие «логика» он истолковывает в трёх смыслах:

• философическая логика, которая изучает нормы, то есть принципы правильного рассуждения;
• математическая логика — логика, тесно связанная с философской логикой, возникнув в результате применения математических методов при изучении философской логики, математическая логика осталась ветвью математики; основная проблема математической логики — объяснение природы математической строгости, изучение оснований математики и разработка техники, которой математики могут с уверенностью пользоваться, с учётом специфической природы логики, положенной в основу математики;
• логика как любая из конкретных систем, являющихся предметом изучения математической или философской логики, например аристотелевская логика, модальная логика, кантовская логика и т. д.

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

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

Основные работы

• Curry H. B. Functionality in combinatory logic. — Proc. National Academy of Sciences of the USA, Vol. 20, 1934. — pp. 584—590.
• Curry H. B., Feys R. Combinatory Logic. — Vol. I, North-Holland Co., Amsterdam, 1958.
• Curry H. B. Foundations of mathematical logic. — McGraw-Hill Book Co., Inc., N.Y., 1963.

Русский перевод: Х. Б. Карри Основания математической логики. — М.: Мир, 1969. — 568 с. Выполнено детальное изучение основных понятий математической логики. Представлена общая теория формальных систем и исчислений. Обсуждены общие методологические вопросы, последовательно описаны исчисления, содержащие импликацию, отрицание и кванторы. Рассмотрены вопросы теории модальностей. Для всех доказательств и определений применен конструктивный подход.

• Curry H. B., Hindley R., Seldin J. P. Combinatory Logic. — Vol. II. Studies in Logic 65, North-Holland Co., Amsterdam, 1972.