Бём, Коррадо

В рамках диссертационной работы создал язык Formules и компилятор для него. Главным новшеством стало то, что компилятор языка был разработан на самом же языке, то есть стал первым в истории полным метациркулярным компилятором. Текст компилятора занимал всего 114 строк кода.

В 1960-х годах совместно с Вольфом Гроссом разработал функциональный язык программирования CUCH, основанный на комбинаторной логике Карри и бестиповом λ-исчислении Чёрча. Название языка является акронимом, образованным от фамилий этих двух логиков^[7].^[8]

В 1964 году создал язык программирования P′′ — минималистичный язык без оператора безусловного перехода. В поддержку вычислительной выразительности созданного языка в рамках совместной работы с одним из учеников в университете «Сапиенца» — Джузеппе Якопини — доказал в 1966 году тьюринг-полноту P′′, означавшую, в свою очередь, выразимость любого алгоритма лишь тремя структурами управления — последовательной передачей управления, ветвлением и циклом. Этот результат подвёл научный базис под структурное программирование: в заметке 1968 года Дейкстра сослался на теорему Бёма — Якопини как на возможность полностью искоренить оператор GOTO из практики программирования, после чего парадигма получила всеобщее признание.

С середины 1960-х годов работал над проблемами λ-исчисления. Среди полученных результатов — теорема о противоречивости утверждения об эквивалентности различных λ-термов в ${\displaystyle \beta \eta }$-нормальной форме (то есть не имеющих нераскрытых подтермов вида ${\displaystyle (\lambda x.P)Q}$ и ${\displaystyle \lambda x.Px}$, где ${\displaystyle x}$ не является свободной переменной в ${\displaystyle P}$). Из этого утверждения непосредственно следует полнота по Гильберту — Посту экстенсионального λ-исчисления. Кроме важности самого результата, оказались востребованы и методы доказательства утверждения: бёмовскую технику выворачивания термов использовал Барендрегт для сопоставления каждому терму конструкции, названной им деревом Бёма, примечательной тем, что в топологии Скотта на этих деревьях все определимые функции λ-исчисления непрерывны^[9].

Другая работа в области λ-исчисления, оказавшая влияние на теорию языков программирования — построение в начале 1970-х годов с ученицей Марьянджолой Дедзани-Чанкальини (итал. Mariangiola Dezani-Ciancaglini) абстрактной машины со стратегией вычисления вызова по имени с автоматической обработкой ${\displaystyle \alpha }$-конверсии.

В 1964 году создал язык программирования P′′ — минималистичный язык без оператора безусловного перехода. В поддержку вычислительной выразительности созданного языка в рамках совместной работы с одним из учеников в университете «Сапиенца» — Джузеппе Якопини — доказал в 1966 году тьюринг-полноту P′′, означавшую, в свою очередь, выразимость любого алгоритма лишь тремя структурами управления — последовательной передачей управления, ветвлением и циклом.

Этот результат подвёл научный базис под структурное программирование: в заметке 1968 года Дейкстра сослался на теорему Бёма — Якопини как на возможность полностью искоренить оператор GOTO из практики программирования, после чего парадигма получила всеобщее признание.

Итальянский оригинал статьи вышел в июне 1962 года^[10][11]. В современных учебниках теорема упоминается как фундаментальная основа структурного программирования. При этом отмечается её преимущественно теоретический характер: классическое доказательство требует введения дополнительных переменных, а на чисто пропозициональном уровне теорема неверна^{[12][13][14][15]}.

С середины 1960-х годов работал над проблемами λ-исчисления. Среди полученных результатов — доказанная в 1968 году теорема о противоречивости утверждения об эквивалентности различных λ-термов в ${\displaystyle \beta \eta }$-нормальной форме (то есть не имеющих нераскрытых подтермов вида ${\displaystyle (\lambda x.P)Q}$ и ${\displaystyle \lambda x.Px}$, где ${\displaystyle x}$ не является свободной переменной в ${\displaystyle P}$), известная как теорема Бёма (или теорема о разделимости)^{[16][17][18][19]}. Из этого утверждения непосредственно следует полнота по Гильберту — Посту экстенсионального λ-исчисления.

Кроме важности самого результата, оказались востребованы и методы доказательства утверждения: бёмовскую технику выворачивания термов использовал Барендрегт для сопоставления каждому терму конструкции, названной им деревом Бёма, примечательной тем, что в топологии Скотта на этих деревьях все определимые функции λ-исчисления непрерывны^[20]. Другая работа в области λ-исчисления, оказавшая влияние на теорию языков программирования — построение в начале 1970-х годов с ученицей Марьянджолой Дедзани-Чанкальини (итал. Mariangiola Dezani-Ciancaglini) абстрактной машины CUCH-machine^[21] со стратегией вычисления вызова по имени с автоматической обработкой ${\displaystyle \alpha }$-конверсии.