Corrado Böhm (17 January 1923 – 23 October 2017) was a Professor
Emeritus
''Emeritus'' (; female: ''emerita'') is an adjective used to designate a retired chair, professor, pastor, bishop, pope, director, president, prime minister, rabbi, emperor, or other person who has been "permitted to retain as an honorary title ...
at the
University of Rome "La Sapienza" and a
computer scientist
A computer scientist is a person who is trained in the academic study of computer science.
Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...
known especially for his contributions to the theory of
structured programming
Structured programming is a programming paradigm aimed at improving the clarity, quality, and development time of a computer program by making extensive use of the structured control flow constructs of selection ( if/then/else) and repetition ( ...
,
constructive mathematics
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
,
combinatory logic
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of comput ...
,
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
, and the semantics and implementation of
functional programming
In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declar ...
languages.
Work
In his PhD dissertation (in Mathematics, at ETH Zurich, 1951; published in 1954), Böhm describes for the first time a full
meta-circular compiler, that is a translation mechanism of a programming language, written in that same language. His most influential contribution is the so-called
structured program theorem
The structured program theorem, also called the Böhm–Jacopini theorem, is a result in programming language theory. It states that a class of control-flow graphs (historically called flowcharts in this context) can compute any computable function ...
, published in 1966 together with Giuseppe Jacopini. Together with Alessandro Berarducci, he demonstrated an isomorphism between the strictly-positive
algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., t ...
s and the polymorphic lambda-terms, otherwise known as Böhm–Berarducci encoding.
In the
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
, he established an important separation theorem between normal forms, known as
Böhm's theorem, which states that for every two closed λ-terms T
1 and T
2 which have different βη-normal forms, there exists a term Δ where Δ T
1 and Δ T
2 evaluate to different free variables (i.e., they may be taken apart internally). This means that, for normalizing terms, Morris'
contextual equivalence Observational equivalence is the property of two or more underlying entities being indistinguishable on the basis of their observable implications. Thus, for example, two scientific theories are observationally equivalent if all of their empiricall ...
, which is a semantic property, may be decided through equality of normal forms, a syntactic property, as it coincides with βη-equality.
A special issue of ''Theoretical Computer Science'' was dedicated to him in 1993, on his 70th birthday. He is the recipient of the 2001
EATCS
The European Association for Theoretical Computer Science (EATCS) is an international organization with a European focus, founded in 1972. Its aim is to facilitate the exchange of ideas and results among theoretical computer scientists as well as ...
Award for a distinguished career in theoretical computer science.
Selected publications
* C. Böhm, "Calculatrices digitales. Du déchiffrage des formules mathématiques par la machine même dans la conception du programme", ''Annali di Mat. pura e applicata'', serie IV, tomo XXXVII, 1–51, 1954
PDF at ETH ZürichEnglish translation 2016 by Peter Sestoft
* C. Böhm, "On a family of Turing machines and the related programming language", ''ICC Bull.'', 3, 185–194, July 1964.
*: Introduced P′′
P′′ (P double prime) is a primitive computer programming language created by Corrado BöhmBöhm, C.: "On a family of Turing machines and the related programming language", ICC Bull. 3, 185-194, July 1964.Böhm, C. and Jacopini, G.: "Flow diagr ...
, the first imperative language without GOTO
GoTo (goto, GOTO, GO TO or other case combinations, depending on the programming language) is a statement found in many computer programming languages. It performs a one-way transfer of control to another line of code; in contrast a function ca ...
to be proved Turing-complete
In computability theory, a system of data-manipulation rules (such as a computer's instruction set, a programming language, or a cellular automaton) is said to be Turing-complete or computationally universal if it can be used to simulate any Tur ...
.
* C. Böhm, G. Jacopini, "Flow diagrams, Turing Machines and Languages with only Two Formation Rules", ''Comm. of the ACM'', 9(5): 366–371,1966.
* C. Böhm, "Alcune proprietà delle forme β-η-normali nel λ-K-calcolo", ''Pubbl. INAC'', n. 696, Roma, 1968.
* C. Böhm, A. Berarducci, "Automatic Synthesis of typed Lambda-programs on Term Algebras", ''Theoretical Computer Science'', 39: 135–154, 1985.
* C. Böhm, "Functional Programming and Combinatory algebras", ''MFCS'', Carlsbad, Czechoslovakia, eds M.P. Chytil, L. Janiga and V. Koubek, ''LNCS 324'', 14–26, 1988.
See also
*
P′′
P′′ (P double prime) is a primitive computer programming language created by Corrado BöhmBöhm, C.: "On a family of Turing machines and the related programming language", ICC Bull. 3, 185-194, July 1964.Böhm, C. and Jacopini, G.: "Flow diagr ...
, a minimal computer programming language
*
Structured program theorem
The structured program theorem, also called the Böhm–Jacopini theorem, is a result in programming language theory. It states that a class of control-flow graphs (historically called flowcharts in this context) can compute any computable function ...
*
List of pioneers in computer science
This is a list of people who made transformative breakthroughs in the creation, development and imagining of what computers could do.
Pioneers
: ''To arrange the list by date or person (ascending or descending), click that column's small "up-do ...
*
Böhm tree
In the study of denotational semantics of the lambda calculus, Böhm trees, Lévy-Longo trees, and Berarducci trees are (potentially infinite) tree-like mathematical objects that capture the "meaning" of a term up to some set of "meaningless" ter ...
*
Böhm's theorem
References
Vitae (University of Rome)
External links
*
''Theoretical Computer Science'', Volume 121, Numbers 1&2, 1993.
Corrado Böhm's personal page
1923 births
2017 deaths
Italian computer scientists
Sapienza University of Rome faculty
Italian people of German descent
École Polytechnique Fédérale de Lausanne alumni
20th-century Italian scientists
21st-century Italian scientists
Scientists from Milan
{{compu-scientist-stub