ハスケル・カリー

ハスケル・ブルックス・カリー（/ ˈ h æ s k əl / HAS -kəl ; 1900年9月12日 - 1982年9月1日）は、アメリカの数学者、論理学者、コンピュータ科学者である。カリーは組合せ論理における業績で最もよく知られており、その最初の概念はモーゼス・シェーンフィンケルの論文^[1]に基づいており、カリーはその論文の発展の多くを担った。カリーはカリーのパラドックスやカリー・ハワード対応でも知られている。彼にちなんで名付けられたプログラミング言語は3つあり、Haskell、Brook、Curryである。また、数学やコンピュータサイエンスで使われる関数の変換方法であるカリー化の概念も彼の名を冠している。

カリーは1900年9月12日、マサチューセッツ州ミリスで、朗読学校を経営していたサミュエル・サイラス・カリーとアナ・バライト・カリーの息子として生まれた。 1916年にハーバード大学に入学し医学を専攻したが、1920年に卒業する前に数学に転向した。マサチューセッツ工科大学（MIT）で電気工学の大学院課程を2年間修了した後、物理学を学ぶためにハーバード大学に戻り、1924年に文学修士号（MA）を取得した。カリーの数理論理学への興味は、アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルによる記号論理学に基づく数学の試みである『プリンキピア・マセマティカ』を紹介されたこの時期に始まった。ハーバード大学に残ったカリーは、数学の博士号（Ph.D.）の取得を目指した。ジョージ・デイヴィッド・バーコフから微分方程式の研究をするよう指導されていたが、彼の興味は論理学に移り続けていた。 1927年、プリンストン大学で講師をしていたとき、カリーはモーゼス・シェーンフィンケルの組合せ論理の研究を発見した。シェーンフィンケルの研究はカリー自身の研究の多くを先取りしていたため、カリーはゲッティンゲン大学に移り、シェーンフィンケルの研究に精通していたハインリヒ・ベーマンとポール・バーナイスと研究することができた。カリーはデイヴィッド・ヒルベルトの指導を受け、バーナイスと密接に研究し、1930年に組合せ論理に関する論文で博士号を取得した。^[2]( 1900-09-12 )

1928年、ゲッティンゲンへ出発する前に、カリーはメアリー・バージニア・ホイートリーと結婚した。カリーが博士論文を完成させる間、夫婦はドイツに住み、その後1929年にペンシルベニア州立大学ステートカレッジへ移り、カリーはそこでペンシルベニア州立大学の職を得た。二人の間にはアン・ライト・カリー（1930年7月27日生まれ）とロバート・ホイートリー・カリー（1934年7月6日生まれ）の二人の子供が生まれた。カリーはその後37年間、ペンシルベニア州立大学に留まった。彼は1931年から1932年まで国立研究員としてシカゴ大学で1年間、1938年から1939年までプリンストン高等研究所で1年間過ごした。1942年、彼は休職し、第二次世界大戦中に米国政府のために応用数学に従事し、特にフランクフォード兵器廠で働いた。戦後すぐに、彼は1945年から1946年にかけてENIACプロジェクトに携わりました。フルブライト奨学金を得て、ベルギーのルーヴァンでロバート・フェイズと共同研究しました。1966年にペンシルベニア州立大学を退職した後、カリーはアムステルダム大学の職に就きました。1970年、組合せ論理に関する論文の第2巻を書き終えた後、カリーはアムステルダム大学を退職し、ペンシルベニア州ステートカレッジに戻りました。

ハスケル・カリーは1982年9月1日(1982-09-01)（享年81歳）、ペンシルベニア州ステートカレッジで亡くなった。

カリーの研究の焦点は、組合せ論理が数学の基礎を提供できることを示す試みであった。1933年の終わりごろ、彼はジョン・ロッサーとのやり取りからクリーネ・ロッサーのパラドックスについて知った。ロッサーとスティーブン・クリーネによって開発されたこのパラドックスは、アロンゾ・チャーチによって提案されたもの（ラムダ計算を一貫したサブシステムとするシステム）やカリー自身のシステムなど、関連する多くの形式システムの矛盾を証明していた。 ^[2]しかし、チャーチ、クリーネ、ロッサーとは異なり、カリーは基礎的なアプローチをあきらめず、「パラドックスから逃げたくない」と述べた。^[3]

カリーは、キャリア全体を通じて組み合わせ論理の分野で研究し、この分野の創始者および最大の人物となりました。組み合わせ論理は、関数型プログラミング言語の 1 つのスタイルの基礎です。組み合わせ論理の威力と範囲はチャーチのラムダ計算と非常に似ており、後者の形式主義はここ数十年で主流になりつつあります。

第二次世界大戦中、カリーはフランクフォード兵器廠で働き、そこでコーシーの研究に基づいて最急降下法のアルゴリズムを開発した。 ^{[4]これは現代の}勾配降下法 の基礎的な例となった。

1947年にカリーは最初の高水準プログラミング言語の一つを記述し、一般的な算術式を1アドレスコンピュータのコードに変換する手順を初めて記述した。^[5]

彼はハーバード大学、プリンストン大学で教鞭をとり、1929年から1966年までペンシルベニア州立大学で教鞭をとった。1942年にカリーのパラドックスを出版した。1966年にアムステルダム大学でエバート・ウィレム・ベスの後任として論理学とその歴史、および精密科学の哲学の教授となった。^[6]

カリーは、より一般的には数理論理学の著作や教育も行っており、この分野での彼の教育は、1963年の著書『数理論理学の基礎』で最高潮に達した。彼が好んだ数学哲学は、師であるヒルベルトに倣った形式主義（1951年の著書を参照）であったが、彼の著作からは、多大な哲学的探究心と、直観主義論理に対する非常に偏見のない考え方が伺える。

• 「組合せ論理の基礎」[組合せ論理の基礎]。アメリカ数学ジャーナル（ドイツ語）。52（3）。ジョンズホプキンス大学出版局：509-536。1930年。doi：10.2307/2370619。JSTOR  2370619。
• 形式的演繹可能性の理論。ノートルダム大学出版局。1950年。^[7]
  • 形式的演繹可能性の理論（第2版）。ノートルダム大学出版局。1957年。
• 数学の形式主義哲学の概要。アムステルダム：エルゼビアサイエンス。1951年。ISBN 0444533680. 2012年7月23日閲覧。
• Leçons de logique algébrique (フランス語)。パリ：ゴーティエ・ヴィラール。 1952年。^[8]
• カリー、ハスケル・ブルックス;フェイズ、ロバート(1958)。組合せ論理。第 1 巻。アムステルダム: North Holland Publishing Company。ISBN 0-7204-2208-6。
• 数理論理学の基礎。マグロウヒル。1963年。
  • 数理論理学の基礎（完全版および修正版ドーバー版）。ニューヨーク：ドーバー出版。1977年。ISBN 0-486-63462-0. 2012年7月23日閲覧。
• カリー、ハスケル・ブルックス、ヒンドレー、J. ロジャー、セルディン、ジョナサン P. (1972)。組合せ論理。第 2 巻。アムステルダム: 北ホラント。ISBN 0-7204-2208-6。

• Seldin & Hindley (1980) — 伝記エッセイが含まれています。

• Barendregt, Hendrik Pieter (1984)。ラムダ計算、その構文と意味論。論理学と数学の基礎研究。第 103 巻。北ホラント。ISBN 0-444-87508-5。
• Knuth, Donald Ervin ; Pardo, Luis Trabb (1976)。プログラミング言語の初期開発。スタンフォード大学、コンピュータサイエンス学部。
• マーカス、R. バルカン(1952)。 「レビュー: Leçons de logique algébrique、HB カリー著」。アメリカ数学協会の会報。58 (2): 673–674。土井: 10.1090/s0002-9904-1952-09657-9。
• ネルソン、D. ( 1952)。「レビュー： HBカリーの形式的演繹可能性の理論」アメリカ数学会報。58 （3）：415–417。doi ：10.1090/s0002-9904-1952-09596-3。
• モーセのシェーンフィンケル(1924)。 「バウスタインの数学的論理学」(PDF)。Mathematische Annalen (ドイツ語)。92 (3-4): 305-316。土井：10.1007/bf01448013。S2CID  118507515。組み合わせロジックを確立した記事。英語翻訳: シェーンフィンケル (1967)
• シェーンフィンケル、モーセ(1967) [1924]。Van Heijenoort、Jean (編)。Über die Bausteine der mathematischen Logik [数学的論理の構成要素について]。フレーゲからゲーデルまで: 数理論理学の情報源の本、1879 ～ 1931 年。シュテファン・バウアー＝メンゲルベルク訳。米国マサチューセッツ州ケンブリッジ: Harvard University Press。 355–366ページ。ISBN 978-0674324497. OCLC  503886453.
• セルディン、ジョナサン P.、ヒンドリー、JR 編 (1980)。HBカリー宛: 組合せ論理、ラムダ計算、形式主義に関するエッセイ。アカデミック プレス。
• セルディン、ジョナサン・P. (2008年3月3日)。「カリーと教会の論理」(PDF) 。 2023年9月23日閲覧。

• セルディン、ジョナサン P.「ハスケル・ブルックス・カリー（1900-1982）」。インターネット哲学百科事典。
• オコナー、ジョン J.、ロバートソン、エドマンド F.、「ハスケル カリー」、マクチューター数学史アーカイブ、セント アンドリュース大学
• カリーのアーカイブには、1920 年から 1931 年にかけての数百ページの原稿の画像が掲載されています。
• CLg. 書誌 587 ページ
• アムステルダム大学編 (2023)。「アカデミックアルバム - 1632年から今日までの教授と博士号取得者」 。 2023年9月23日閲覧。