Бём, Коррадо

Коррадо Бём
Коррадо Бём
Дата рождения	17 января 1923(1923-01-17)
Место рождения	Милан, Королевство Италия;
Дата смерти	23 октября 2017(2017-10-23) (94 года)
Место смерти	Рим, Италия;
Страна	Королевство Италия; Италия;
Научная сфера	информатика, структурное программирование, конструктивная математика, лямбда-исчисление, Комбинационная логика, функциональное программирование и семантика языков программирования
Место работы	Римский университет Ла Сапиенца; Туринский университет;
Альма-матер	ВТШ Цюриха; Федеральная политехническая школа Лозанны;
Научный руководитель	Эдуард Штифель[d] и Пауль Бернайс
Награды и премии	премия Европейской ассоциации теоретической информатики[d] (2001) почётный доктор Миланского университета[d] (1994)
Сайт	corradobohm.it
	Медиафайлы на Викискладе

Коррадо Бём (Corrado Böhm; 17 января 1923 года, Милан — 23 октября 2017 года, Рим) — итальянский математик, специалист в области информатики и математической логики, внёсший решающий вклад в теоретическое обоснование парадигмы структурного программирования и получивший важные результаты в λ-исчислении, комбинаторной логике, семантике языков программирования; один из ранних исследователей теории языков программирования. Профессор римского университета «Сапиенца», сооснователь факультетов информатики Туринского университета и «Сапиенцы».

БиографияПравить

Родился и вырос в Милане. В 1942 году уехал в Швейцарию, где поступил в Лозаннский университет. Окончил вуз в 1946 году с дипломом по электротехнике, после чего был принят ассистентом-исследователем в Высшую техническую школу Цюриха^[3].

В 1949—1950 годы работал в Цюрихском институте прикладной математики (входящем в систему Высшей технической школы Цюриха) в группе Эдуарда Штифеля (нем. Eduard Stiefel — версия статьи «Штифель, Эдуард» на немецком языке Eduard Stiefel), среди руководителей направления в институте работал также Пауль Бернайс, который, как впоследствии отмечал учёный, оказал на него большое влияние, стимулировав интерес к теоретическим вопросам вычислимости и машинам Тьюринга. Совместно с другим сотрудником института — Харри Лаэтом — протестировал компьютер Z4 Конрада Цузе^[4], который в итоге был куплен Высшей технической школой (и стал, таким образом, первым в мире коммерческим компьютером). В 1951 году под руководством Штифеля завершил докторскую диссертацию, работа выпущена в 1952 году, формальная защита состоялась в 1954 году.

В 1950 году женился на художнице из Падуи Еве Романин Якур, и в 1951 году вернулся в Италию. В 1953 году работал в Ивреа в фирме Olivetti, в том же году принят на должность исследователя в Институт прикладного математического анализа (итал. Istituto per le applicazioni del calcolo) в Риме. В институте совместно с британской фирмой Ferranti под руководством Мауро Пиконе (итал. Mauro Picone — версия статьи «Пиконе, Мауро» на итальянском языке Mauro Picone) создавался первый итальянский компьютер FINAC^[it], и Бём занимался тестированием его производительности^[3]. В основном же работы периода 1950-х годов посвящены с основному направлению института — дифференциальному и интегральному исчислению и его приложениям. Во второй половине 1950-х годов в браке с Евой родились три дочери.

С 1960 года, продолжая работать в Институте прикладного математического анализа, начал читать курсы по информатике в римском университете «Сапиенца», там же появились первые ученики-аспиранты. В 1968 году получил профессорское звание.

С 1969 года — руководитель курса информатики факультета наук Туринского университета, в 1974 году вернулся в Рим в «Сапиенцу». В 1975 году организовал в университете международную конференцию по λ-исчислению, ставшую первым таким событием в направлении, и сыгравшем важную роль в бурном его развитии в ближайшее десятилетие. В том же году вошёл в редакционный совет журнала Theoretical Computer Science^[en], в котором оставался до последних лет; к 70-летию учёного в 1993 году журнал посвятил специальный выпуск.

В 1990 году избран академиком Европейской академии^[5]. В 1994 году получил степень honoris causa Миланского университета^[6]. В 2001 году за достижения в области теории языков программирования награждён премией Европейской ассоциации теоретической информатики (англ. EATCS Award — версия статьи «Премия Европейской ассоциации теоретической информатики» на английском языке EATCS Award)^[7].

Научный вкладПравить

В рамках диссертационной работы создал язык Formules^[en] и компилятор для него. Главным новшеством стало то, что компилятор языка был разработан на самом же языке, то есть стал первым в истории полным метациркулярным компилятором (англ. meta-circular compiler — версия статьи «Метациркулярный компилятор» на английском языке meta-circular compiler)^[8]. Текст компилятора занимал всего 114 строк кода.

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

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

Избранная библиографияПравить

C. Böhm. Calculatrices digitales. Di déchiffrage des formules logico-mathématiques par la machine même dans la conception du programme // Annali di Matematica Pura ed Applicata. — 1954. — Т. 37, № 4. — С. 175—217.
C. Böhm. On a family of Turing machines and related programming language // International Computer Centre Bulletin. — 1964. — Т. 3, № 3. — публикация о P′′
C. Böhm, G. Jacopini. Flow diagrams, Turing machines and languages with only two formation rules // Communications of the ACM. — 1966. — Т. 5, № 9. — С. 366—371. — статья с теоремой Бёма — Якопини
C. Böhm. Alcune proprietà delle forme normali nel calcolo // Publicazioni del’Istituto per le applicazioni del calcolo. — № 696. — статья с теоремой Бёма об отделимости термов в нормальной форме и содержащая технику выворачивания термов
C. Böhm, M. Dezani-Ciancaglini. Can syntax be ignored during translation? // Automata, Languages and Programming / M. Nivat. — Amsterdam: North-Holland, 1972. — С. 197—207. — статья о стратегии вычисления с вызовом по имени с автоматической $\text{[math]}$ $\text{[math]}$ $\alpha$ -конверсией
λ-Calculus and Computer Science Theory / C. Böhm (editor). — Berlin: Springer-Verlag, 1975. — Т. 37. — 383 с. — (Lecture Notes in Computer Science). — ISBN 3-540-07416-3. — материалы симпозиума по λ-исчислению в информатике, прошедшего 25—27 марта 1975 года

ПримечанияПравить

↑ ¹ ² http://www.corradobohm.it/Corrado_Bohm/Biography.html
↑ http://www.cnrs.fr/ins2i/spip.php?article2697
↑ ¹ ² Биография, 2013.
↑ Herbert Bruderer. Computing History Beyond the U.K. and U.S.: Selected Landmarks from Continental Europe // Communications of the ACM. — 2017. — Т. 60, № 2. — С. 76—84. — doi:10.1145/2959085. Архивировано 18 сентября 2020 года.
↑ Corrado Böhm (неопр.). Academia Europaea (24 октября 2017). Дата обращения: 8 января 2018. Архивировано 24 января 2021 года.
↑ In memoria di Corrado Böhm (1923—2017) (неопр.). Università degli Studi di Roma „La Sapienza” (23 октября 2017). Дата обращения: 8 января 2018. Архивировано 8 января 2018 года.
↑ EATCS Award (неопр.). European Association of Theoretical Computer Science (1 января 2018). Дата обращения: 8 января 2018. Архивировано 17 января 2018 года.
↑ Donald E. Knuth, Luis Trabb Pardo. The Early Development of Programming Languages // A History of Computing in the Twentieth Century / N. Metropolis, I. Howlett, Gian-Carlo Rota. — N. Y.: Academic Press. — С. 200—276. — ISBN 0-12-491650-3.
↑ E. Dijkstra. Go to statement considered harmful // Communications of the ACM. — 1968. — Т. 11, № 3. — С. 147–148. — doi:10.1145/362929.362947.
↑ Барендрегт, Хенк. Глава 10. Деревья Бёма // Ламбда-исчисление. Его синтаксис и семантика = The Lambda Calculus. Its syntax and semantics (рус.) / перевод с английского Г. Е. Минца. — М.: Мир, 1985. — С. 19, 46, 220—276. — 606 с. — 4800 экз.

СсылкиПравить

Corrado Böhm’s bio and bibliography (неопр.). corradobohm.it (26 января 2013). Дата обращения: 7 января 2017. Архивировано 17 февраля 2017 года.

[_4aadd1b7478f2a3f-1] ¹ ² http://www.corradobohm.it/Corrado_Bohm/Biography.html

[_71166c123f84474f-2] ttp://www.cnrs.fr/ins2i/spip.php?article2697

[_644447db654f8483-3] ¹ ² Биография, 2013.

[4] Herbert Bruderer. Computing History Beyond the U.K. and U.S.: Selected Landmarks from Continental Europe // Communications of the ACM. — 2017. — Т. 60, № 2. — С. 76—84. — doi:10.1145/2959085. Архивировано 18 сентября 2020 года.

[5] Corrado Böhm (неопр.). Academia Europaea (24 октября 2017). Дата обращения: 8 января 2018. Архивировано 24 января 2021 года.

[6] In memoria di Corrado Böhm (1923—2017) (неопр.). Università degli Studi di Roma „La Sapienza” (23 октября 2017). Дата обращения: 8 января 2018. Архивировано 8 января 2018 года.

[7] EATCS Award (неопр.). European Association of Theoretical Computer Science (1 января 2018). Дата обращения: 8 января 2018. Архивировано 17 января 2018 года.

[8] Donald E. Knuth, Luis Trabb Pardo. The Early Development of Programming Languages // A History of Computing in the Twentieth Century / N. Metropolis, I. Howlett, Gian-Carlo Rota. — N. Y.: Academic Press. — С. 200—276. — ISBN 0-12-491650-3.

[9] E. Dijkstra. Go to statement considered harmful // Communications of the ACM. — 1968. — Т. 11, № 3. — С. 147–148. — doi:10.1145/362929.362947.

[10] Барендрегт, Хенк. Глава 10. Деревья Бёма // Ламбда-исчисление. Его синтаксис и семантика = The Lambda Calculus. Its syntax and semantics (рус.) / перевод с английского Г. Е. Минца. — М.: Мир, 1985. — С. 19, 46, 220—276. — 606 с. — 4800 экз.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

Коррадо Бём

Дата рождения	17 января 1923(1923-01-17)^[1]
Место рождения	Милан, Королевство Италия^[1]
Дата смерти	23 октября 2017(2017-10-23)^[2] (94 года)
Место смерти	Рим, Италия
Страна	Королевство Италия Италия
Научная сфера	информатика, структурное программирование, конструктивная математика, лямбда-исчисление, Комбинационная логика, функциональное программирование и семантика языков программирования
Место работы	Римский университет Ла Сапиенца Туринский университет
Альма-матер	ВТШ Цюриха Федеральная политехническая школа Лозанны
Научный руководитель	Эдуард Штифель^[d] и Пауль Бернайс
Награды и премии	премия Европейской ассоциации теоретической информатики^[d] (2001) почётный доктор Миланского университета^[d] (1994)
Сайт	corradobohm.it
Медиафайлы на Викискладе