Хенк Барендрегт ( Хендрик Питер Барендрегт , нидерл. Hendrik Pieter Barendregt ; родился 18 декабря 1947 года ) — нидерландский математик и логик , исследователь λ-исчисления и теории типов , автор λ-куба . Профессор, заведующий кафедрой оснований математики и информатики Университета Неймегена .

Биография

Родился в 1947 году в Амстердаме . В 1952—1965 годы учился в образовательных учреждениях, использующих систему Монтессори . В 1967 году окончил Утрехтский университет по классу математической логики, получив степень магистра. В 1971 году под руководством ( нидерл. ) и ( нем. ) защитил докторскую диссертацию ( Ph. D. ) по экстенсиональным моделям λ-исчисления и комбинаторной логики .

После защиты диссертации в 1971—1972 годах работал исследователем в Стэнфордском университете . С 1972 по 1986 год занимал профессорские должности в Утрехтском университете . С 1986 года — профессор Университета Неймегена , заведующий кафедрой оснований математики и информатики. В разное время работал на приглашённых позициях в Дармштадтском техническом университете , Швейцарской высшей технической школе Цюриха , Университете Карнеги — Меллон , Киотском университете , Сиенском университете .

Увлекается буддизмом и медитацией , публикует статьи о медитации в психологических и научно-популярных журналах .

Научная и редакционная работа

Результаты начала 1970-х годов относятся к нормальным формам в λ-исчислении и реализуемости в комбинаторной логике . Труды второй половины 1970-х годов посвящены вопросам моделей λ-исчисления. Известность получил в 1981 году после выхода монографии «Ламбда-исчисление. Его синтаксис и семантика», дважды переиздававшейся и переведённой на русский и китайский языки и отмечаемой как основополагающий труд по бестиповому λ-исчислению .

В 1980-е годы изучал вопросы автоматического доказательства и взаимосвязи математического доказательства с λ-исчислением и теорией типов (впоследствии концептуализированные как изоморфизм Карри — Ховарда ). В 1986 году после перехода в Университет Неймегена организовал группу, занимающуюся вопросами формализации математики, идейно продолжающую работы, которые велись в рамках проекта Николаса де Брёйна . Во второй половине 1980-х изучал типизированные варианты λ-исчисления, с особым вниманием к взаимосвязям между ними; в 1991 году предложил λ-куб — графическую интерпретацию восьми различных типов типизированного λ-исчисления, снискавшую популярность как в среде логиков, так и среди специалистов по основаниям информатики и языкам программирования .

Член редколлегий журналов , , , .

Награды и сообщества

Член Европейской академии (1992). Академик Нидерландской королевской академии наук (1997).

В 2002 году удостоен ордена Нидерландского льва (рыцарь ордена). В том же году получил Премию Спинозы — крупную премию от нидерландской правительственной ( нидерл. ).

Библиография

• Henk Barendregt. The Lambda Calculus. Its syntax and semantics (англ.) . — Amsterdam: North Holland, 1981. — 622 p. — (Studies in Logic and the Foundations of Mathematics, vol. 103). — ISBN 0-444-87508-5 . — фундаментальная монография по λ-исчислению, дважды переиздавалась (1984, 2012), переведена на китайский (1990) и русский (1985) языки:

  Барендрегт, Хенк. Ламбда-исчисление. Его синтаксис и семантика (рус.) . — М. : Мир , 1985. — 606 с. — 4800 экз.

• Henk Barendregt, Wil Dekkers, Richard Statman. Lambda Calculus With Types (англ.) . — Cambridge : Cambridge University Press , 2010. — 703 p. — (Perspectives in Logic). — ISBN 9780521766142 . — объемлющее изложение вариантов типизированного λ-исчисления , различных расширений и приложений, задуманная как продолжение книги «Ламбда-исчисление. Его синтаксис и семантика». Переиздавалась в 2013 году.

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

• Henk Barendregt. Combinatory logic and the axiom of choice (англ.) // Indagationes Mathematicae. — 1973. — Vol. 3 , no. 76 . — P. 203—221 .
• Henk Barendregt. A global representation of the recursive functions in the λ-calculus (англ.) // . — 1976. — No. 3.2 . — P. 225—242 .
• Барендрегт Х. Бестиповое λ-исчисление // Справочная книга по математической логике. / Под редакцией Дж. Барвайса. — М. : Наука, 1983. — Т. 4: Теория доказательств. — С. 278—318.
• Henk Barendregt, Adrian Rezus. (англ.) // . — 1983. — Vol. 59 . — P. 127—147 .
• Henk Barendregt. Lambda calculi with types (англ.) // S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum (editors) Handbook of Logic in Computer Science. — Oxford : Oxford University Press , 1992. — Vol. 2: Background: Computational Structures . — P. 117–309 . — ISBN 0-19-853761-1 . — публикация, где впервые введён λ-куб.

Примечания

Ссылки

• — официальный сайт факультета оснований математики и информатики Университета Неймегена — страница Хенка Барендрегта