コラード・ベーム

コッラード・ベーム（1923年1月17日 - 2017年10月23日）は、イタリアのコンピュータ科学者であり、ローマ・ラ・サピエンツァ大学の名誉教授でした。構造化プログラミング理論、構成的数学、組み合わせ論理、ラムダ計算、関数型プログラミング言語の意味論と実装への貢献で特に知られています。

ベームは、博士論文（チューリッヒ工科大学数学、1951年、1954年出版）の中で、プログラミング言語の翻訳メカニズムである完全なメタ循環コンパイラを初めて記述した。彼の最も影響力のある貢献は、ジュゼッペ・ヤコピニと共に1966年に発表された、いわゆる構造化プログラム定理である。彼はアレッサンドロ・ベラルドゥッチと共に、厳密に正の代数的データ型と多相ラムダ項の間の同型性、別名ベーム・ベラルドゥッチ符号化を実証した。^{[ 1 ]}

ラムダ計算において、彼は正規形間の重要な分離定理、すなわちベームの定理を確立した。この定理は、異なるβη正規形を持つ任意の2つの閉じたλ項T ₁とT _{2に対して、Δ T 1}とΔ T ₂が異なる自由変数に評価される（つまり、内部的に分離できる）項Δが存在することを述べている。これは、正規化項に関して、意味論的性質であるモリスの文脈的等価性が、βη等価性と一致するため、構文的性質である正規形の等価性によって決定できることを意味する。

1993年、彼の70歳の誕生日に、理論計算機科学誌『Theoretical Computer Science』の特集号が彼に捧げられた。彼は理論計算機科学における卓越した業績により、2001年にEATCS賞を受賞している。

• ベーム、コッラード (1954)。「デジタル計算。プログラムの概念による機械計算の数式計算」(PDF)。アンナリ・ディ・マット。プラエアプリカタ。セリエ IV (トモ XXXVII): 1–51。「ベーム：デジタルコンピュータ。プログラム構想時に機械自体を用いて論理数学式を符号化することについて」。B. セストフト訳。2016年5月4日。
• — (1964). 「チューリングマシンのファミリーと関連するプログラミング言語について」. ICC ブレティン. 3 : 185– 194. doi : 10.2307/2270680 .: GOTO 命令を持たない最初の命令型言語であるP′′を導入し、チューリング完全であることが証明された。
• — ; Jacopini, Giuseppe [イタリア語] (1966年5 月)。 「フロー図、チューリング マシン、および 2 つの形成規則のみを持つ言語」。Communications of the ACM。9 ( 5 ): 366–371。CiteSeerX 10.1.1.119.9119。doi : 10.1145/ 355592.365646。S2CID 10236439。  
• — (1968)。 「β-η-normali nel λ-K-calcolo の固有の形状」。出版物INAC（イタリア語）。696。ローマ。
• — ; Berarducci, A. (1985). "項代数上の型付きラムダプログラムの自動合成". Theoretical Computer Science . 39 : 135– 154. doi : 10.1016/0304-3975(85)90135-5 .
• — (1988). 「関数型プログラミングと組み合わせ代数」。Chytil, MP; Janiga, L.; Koubek, V. (編)『MFCS』LNCS 324。カールスバート、チェコスロバキア。pp. 14–26。 

• P′′、最小限のコンピュータプログラミング言語
• 構造化プログラム定理
• コンピュータ科学の先駆者一覧
• ベームの木
• ベームの定理

• ヴィタエ（ローマ大学）

• 数学系譜プロジェクトのコラード・ベーム
• 「コラード・ベーム氏の70歳の誕生日を記念する寄稿集」、理論計算機科学、第121巻、第1号および第2号、1993年。
• コラード・ベームの個人ページ。