Введение

Итальянский учёный в области информатики (1923–2017)

Коррадо Бём (17 января 1923 – 23 октября 2017) – итальянский учёный в области информатики и профессор-эмерит Римского университета "La Sapienza", наиболее известный своими вкладами в теорию структурированного программирования, конструктивную математику, комбинаторную логику, лямбда-исчисление, а также семантику и реализацию функциональных языков программирования.

Работа

В своей докторской диссертации (по математике, в ETH Zurich, 1951; опубликованной в 1954 году) Бём впервые описал полноценный метациркулярный компилятор, то есть механизм трансляции языка программирования, написанный на самом этом языке. Его наиболее значительным вкладом является так называемая теорема о структурированной программе, опубликованная в 1966 году совместно с Джузеппе Джакопини. Вместе с Алессандро Берардуччи он продемонстрировал изоморфизм между строго положительными алгебраическими типами данных и полиморфными лямбда-термами, также известные как кодировка Бёма — Берардуччи. В лямбда-исчислении он установил важную теорему о разделении нормальных форм, известную как теорема Бёма, которая утверждает, что для любых двух замкнутых λ-термов T1 и T2, имеющих различные βη-нормальные формы, существует терм Δ, такой что ΔT1 и ΔT2 приводятся к различным свободным переменным (то есть их можно разложить внутри). Это означает, что для нормализуемых термов контекстная эквивалентность Морриса, являющаяся семантическим свойством, может быть определена посредством равенства нормальных форм, синтаксического свойства, поскольку она совпадает с βη-равенством. Специальный выпуск журнала Theoretical Computer Science был посвящен ему в 1993 году, в связи с его 70-летием. Он является лауреатом премии EATCS 2001 года за выдающиеся достижения в теоретической информатике.

Избранные публикации

C. Böhm, "Цифровые вычислительные машины. Разбор математических формул машиной непосредственно в процессе разработки программы", Annali di Mat. pura e applicata, серия IV, том XXXVII, 1–51, 1954. PDF доступен в ETH Zürich. Английский перевод 2016 года Питера Сестофта.
C. Böhm, "О семействе машин Тьюринга и соответствующем языке программирования", ICC Bull., 3, 185–194, июль 1964 года. Введен P′′, первый императивный язык без оператора GOTO, для которого доказана полнота по Тьюрингу.
C. Böhm, G. Jacopini, "Блок-схемы, машины Тьюринга и языки с двумя правилами порождения", Comm. of the ACM, 9(5): 366–371, 1966.
C. Böhm, "Некоторые свойства нормальных βη-форм в λK-исчислении", Pubbl. INAC, n. 696, Рим, 1968.
C. Böhm, A. Berarducci, "Автоматический синтез типизированных лямбда-программ на термальных алгебрах", Theoretical Computer Science, 39: 135–154, 1985.
C. Böhm, "Функциональное программирование и комбинаторные алгебры", MFCS, Карлсбад, Чехословакия, под редакцией M. P. Chytil, L. Janiga и V. Koubek, LNCS 324, 14–26, 1988.