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

Биография

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

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

В 1950 году женился на художнице из Падуи Еве Романин Якур, и в 1951 году вернулся в Италию. В 1953 году работал в Ивреа в фирме Olivetti , в том же году принят на должность исследователя в ( итал. ) в Риме . В институте совместно с британской фирмой Ferranti под руководством ( итал. ) создавался первый итальянский компьютер , и Бём занимался тестированием его производительности . В основном же работы периода 1950-х годов посвящены с основному направлению института — дифференциальному и интегральному исчислению и его приложениям. Во второй половине 1950-х годов в браке с Евой родились три дочери.

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

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

В 1990 году избран академиком Европейской академии . В 1994 году получил степень honoris causa Миланского университета . В 2001 году за достижения в области теории языков программирования награждён ( англ. ) .

Научный вклад

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

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

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

Примечания

Ссылки

• (неопр.) . corradobohm.it (26 января 2013). Дата обращения: 7 января 2017. 17 февраля 2017 года.