stanford-oval/wikipedia huggingface dataset:
カリー＝ハワード同型対応
ヒルベルト流の推論体系とコンビネータ論理との間の対応

この対応はCurry and Fays (1958)に於いて指摘された：最も単純なコンビネータ論理の一種におけるコンビネータ K と S が、驚くべきことにヒルベルト流の証明体系における公理図式  \alpha \to (\beta \to \alpha ) と  (\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))  とにそれぞれ対応するのである。このことから、しばしば上記の公理図式はそれぞれ K と S と呼ばれる。ヒルベルト流の証明と見做せるプログラムの例が与えられる（後述）。
直観主義論理の含意断片に制限するならば、次のようにヒルベルト流の極めて簡明な形式化が存在する。いま  \Gamma  を論理式の有限集合として、これを仮定と見做す。論理式  \delta  が  \Gamma  から導出可能である（ \Gamma \vdash \delta ）とは、以下の場合をいう：
\delta  は仮定である、すなわち  \Gamma  に属す、
\delta は公理図式の代入例である、すなわち：
\delta  は  \alpha \to (\beta \to \alpha ) の形をしているか、
\delta  は  (\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma )) の形をしている、
\delta  は推論により得られる、すなわち、ある  \alpha  について  \alpha  と  \alpha \to \delta  が  \Gamma  から導出可能である。
これは推論規則を用いて形式化できる。以下に示す表の左の列を参照されたい。
我々は同様の構文により型付きコンビネータ論理を形式化することができる。いま  \Gamma  を次の形式の有限集合（ただし同じ変数に異なる型が紐付けられてはならない）として、これを変数の型宣言と見做す。
このとき、CL項  M が  \Gamma  のもとで型  \delta  を持つ（ \Gamma \vdash M:\delta ）とは、以下の場合をいう：
M:\delta  は  \Gamma  に属す、
M:\delta は基本的なコンビネータの型付けである、すなわち：
M:\delta  は  K:\alpha \to (\beta \to \alpha ) であるか、あるいは
M:\delta  は  S:(\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma )) である、
M:\delta  は  \Gamma \vdash N:\alpha \to \delta  かつ  R:\alpha  なるCL項  M と  N の関数適用  (NR) である。
型付きCL項の構成規則は以下に示す表の右の列を参照されたい。カリーは各々の行が同型に対応していることを指摘した。この直観論理との対応の制限は、古典論理の恒真式、例えばパースの法則  ((\alpha \to \beta )\to \alpha )\to \alpha  などがこの対応から締め出されていることを意味する。
| 論理 | プログラミング |
| --- | --- |
 {\frac {\alpha \in \Gamma }{\Gamma \vdash \alpha }}{\text{Assum}}:  {\frac {x:\alpha \in \Gamma }{\Gamma \vdash x:\alpha }}
 {\frac {}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}{\text{Ax}}_{K}:  {\frac {}{\Gamma \vdash K:\alpha \rightarrow (\beta \rightarrow \alpha )}}
 {\frac {}{\Gamma \vdash (\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}{\text{Ax}}_{S}:  {\frac {}{\Gamma \vdash S:(\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}
 {\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}{\text{Modus Ponens}}:  {\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\alpha }{\Gamma \vdash E_{1}\;E_{2}:\beta }}{\text{Application}}
もっと抽象的なレベルから見ると、この対応は以下の表のようにして述べ直すことができる。とくに、ヒルベルト流の推論体系における演繹定理（のメタ証明）は、コンビネータ論理における抽象の除去手続きと対応している。
| 論理 | プログラミング |
| --- | --- |
仮定: 変数
公理: コンビネータ
モーダス・ポネンス: 関数適用
演繹定理: 抽象の除去
この対応によって、コンビネータ論理の結果をヒルベルト流の推論体系の結果に翻訳できる。その逆もまた同様である。例えば、CL項の簡約はヒルベルト流の証明図の簡約手続きと見ることができる。また、正規なCL項は正規な証明図へと翻訳される。ここで正規とは、これ以上簡約できないことを意味する。正規化定理は型付け可能なCL項は必ず正規形を持つという定理であるが、これはヒルベルト流の証明図は必ず正規形を持つという結果に翻訳できる。
反対に、直観主義論理における例えばパースの法則の証明不能性は、コンビネータ論理における次の結果に翻訳できる：型  ((\alpha \to \beta )\to \alpha )\to \alpha  を持つCL項は存在しない。
コンビネータからなる集合の完全性の結果もまた翻訳できる。例えば、 one-point basis  X は任意のCL項を表現できることが知られている。このコンビネータから公理図式
が得られる。これは  X の主要型（ X の可能な型で代入に関して極小なもの）である。 X コンビネータの完全性から、上に挙げた唯一の公理図式から次の公理図式が証明可能であることが従う：
自然演繹とラムダ計算との間の対応

ハスケル・カリーがヒルベルト流の体系とコンビネータ論理の構文的対応を強調した後、ウィリアム・アルヴィン・ハワードは1969年に単純型付きラムダ計算と自然演繹との構文的な同型性を明確にした。以下、左辺で直観主義的自然演繹の含意断片を形式化し、右辺でラムダ計算の型付け規則を示す。左辺では  \Gamma ,\Gamma _{1},\Gamma _{2} で順序付けられた論理式の列を表す。右辺ではラムダ項で名前付けられた論理式の列を表す。
| 論理 | プログラミング |
| --- | --- |
 {\frac {}{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}{\text{Ax}}:  {\frac {}{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}
 {\frac {\Gamma ,\alpha \vdash \beta }{\Gamma \vdash \alpha \rightarrow \beta }}\rightarrow I:  {\frac {\Gamma ,x:\alpha \vdash t:\beta }{\Gamma \vdash \lambda x.t:\alpha \rightarrow \beta }}
 {\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\rightarrow E:  {\frac {\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha }{\Gamma \vdash t\;u:\beta }}
この対応を言い換えれば、 \Gamma \vdash \alpha  を証明するということは、型宣言列  \Gamma  のもとで型  \alpha  を持つオブジェクトを構成することに対応する。公理は新しい変数の導入（とその型宣言）に、→ I 規則は関数抽象に、→ E 規則は関数適用に対応する。もし左辺の文脈  \Gamma  を単なる論理式の集合と見做す（暗黙の縮約と弱化を認める）ならば、この対応は正確ではないことが分かる。というのも、例えば  \Gamma  の中にラムダ項  \lambda x.\lambda y.x と  \lambda x.\lambda y.y で名前付けられた論理式  \alpha \to \alpha \to \alpha  が属していたならば、右辺ではこれらを区別するが、左辺ではこれを同じものと見做す。
ハワードは他の論理の結合子と単純型付きラムダ項の他の構成との間に対応を拡張できることを示した。例えば論理積との対応は次に示す表のようになる：
| 論理 | プログラミング |
| --- | --- |
 {\frac {\Gamma \vdash \alpha \qquad \Gamma \vdash \beta }{\Gamma \vdash \alpha \wedge \beta }}\wedge I:  {\frac {\Gamma \vdash t:\alpha \qquad \Gamma \vdash u:\beta }{\Gamma \vdash \langle t,u\rangle :\alpha \times \beta }}
 {\frac {\Gamma \vdash \alpha _{1}\wedge \alpha _{2}}{\Gamma \vdash \alpha _{i}}}\wedge E:  {\frac {\Gamma \vdash t:\alpha _{1}\wedge \alpha _{2}}{\Gamma \vdash \pi _{i}t:\alpha _{i}}}

もっと抽象的に見ればこの対応は次の表として纏められる。とりわけ、ラムダ計算における正規形の概念は自然演繹におけるプラヴィッツの正規な証明に対応する。型付けられたラムダ項は正規形を持つという結果（正規化定理）は、自然演繹の無矛盾性や論理和分離特性の証明に利用できる。型の具体性の問題の決定手続きを直観主義的な証明可能性の決定手続きに変換できる。
| 論理 | プログラミング |
| --- | --- |
公理: 変数
導入規則: コンストラクタ
除去規則: デストラクタ
正規な証明: 正規なラムダ項
証明の正規化: ラムダ項の弱正規化
証明可能性: 型の具体性の問題（type inhabitation problem）
直観論理の恒真式: 具体型（inhabited type）
ハワードの対応は自然演繹およびラムダ計算の拡張に対しても自然に延長できる。網羅的ではないがここに列挙しておく：
ジラールとレイノルズのSystem F：2階の命題論理と多相ラムダ計算
高階述語論理とジラールのSystem Fω
帰納型と代数的データ型
様相論理における必然性様相  \Box  とstaged computation
様相論理における可能性様相  \Diamond  とmonadic types for effects
λρ計算は古典論理と対応する
λI計算は適切さの論理と対応する
グロタンディーク位相に於ける局所真理(∇)様相、あるいは同じことだが Benton, Bierman, and de Paiva (1998) のlax様相(○)は計算型を記述するCL論理と対応する。
ハワードの対応はまた自然演繹およびラムダ計算の制限に対しても成り立つ。例えばBCKλ計算とBCK論理の対応が挙げられる。ここでBCKλ計算とは、ラムダ項の構成のうち関数適用の規則を
と制限することにより得られる項書換え系である。これにより自由変数の複数回の使用が禁止される。したがってこの体系は1つの仮定を複数回使用する（縮約規則）ことを禁止するBCK論理と対応する。さらにラムダ項の構成のうちラムダ抽象の規則を
と制限することにより得られる体系はBCI論理と対応する。これにより未使用の変数の束縛が禁止される。したがってこの体系は縮約規則に加えて未使用の仮定を解消する（弱化規則）ことを禁止するBCI論理と対応する。
古典論理と制御演算子との間の対応

カリーおよびハワードの時代では、「証明＝プログラム」対応は専ら直観主義論理においてのみ考察されていた。すなわち、ここでの論理では、とくにパースの法則は導出不能であった。パースの法則すなわち古典論理を含む明確な対応の拡張はグリフィンの仕事による。グリフィンはプログラムの実行における評価文脈（継続）をキャプチャしそれを再度使用するような制御演算子を持つラムダ計算が古典論理と対応することを指摘した。基本的な古典論理のカリー＝ハワード対応は以下で与えられる。なお、古典論理の証明から直観論理の証明への変換（グリベンコの定理）に用いられる二重否定変換は、制御演算子を持つラムダ項から純粋なラムダ項へのCPS変換に対応する。もっと具体的にいえば、名前呼びCPS変換はコルモゴロフの二重否定変換に、値呼びCPS変換は黒田の二重否定変換に関係する。
| 論理 | プログラミング |
| --- | --- |
パースの法則:  ((\alpha \to \beta )\to \alpha )\to \alpha : 継続呼び出し
二重否定変換: CPS変換
パースの法則の代りにシークエントの結論に複数の論理式を許容することによっても古典論理の自然演繹を定義できる。この場合もやはり対応が成立する。例えばある種の古典論理の自然演繹とM. Parigotのλμ計算の間に「証明＝プログラム」の対応が存在する。
シークエント計算

「証明＝プログラム」対応はゲンツェンのシークエント計算においても確立されるが、ヒルベルト流の体系や自然演繹のように、既に知られていたような計算模型との対応関係は存在しない。
シークエント計算は左導入規則、右導入規則、ならびに除去可能なカット規則により特徴づけられる。シークエント計算の構造はある種の抽象機械の構造に似ている。非形式的な対応は次のようである：
| 論理 | プログラミング |
| --- | --- |
カット除去: 抽象機械における簡約
右導入規則: コードのコンストラクタ
左導入規則: 評価スタックのコンストラクタ
カット除去において右側を優先: 名前呼び簡約戦略
カット除去において左側を優先: 値呼び簡約戦略
カット除去定理: 簡約の弱正規性
再帰型と自己言及

命題論理式に次のような構成規則を追加する場合を考える：
この論理式の内容的な意味は循環的命題  [{\rm {this}}/p]\alpha  である。ただし  [\mu q.\beta /p]\alpha  なる論理式の内容的意味  [[{\rm {this}}/q]\beta /p]\alpha  の中の this は命題全体ではなく  [{\rm {this}}/q]\beta  を指示するものである。すなわち  \mu p.\alpha  とは次の論理式の再帰方程式
の解（不動点）であるというに他ならない。例えば  \mu p.\neg p は嘘つきのパラドックスにおける嘘つき命題 this sentence is false を意味する論理式である。したがってこの論理体系は矛盾している。
この論理式構成に対応する型構成を再帰型という。例えば可変長リスト型は再帰型として実現できる：
ここで 1 はトップ型である。この型システムでは Yコンビネータ や  \Omega =(\lambda x.xx)(\lambda x.xx) などの項も型を持つことになる。これらの項は通常の型システムでは型を持たない。なおコンビネータ  \Omega  の（主要型の）型付けの導出はカリーのパラドックスの自然演繹による証明と対応する。
以上の体系の対応は次のように纏められる：
| 論理 | プログラミング |
| --- | --- |
循環的命題: 再帰型
 {\frac {\Gamma \vdash \mu p.\alpha }{\Gamma \vdash [\mu p.\alpha /p]\alpha }}:  {\frac {\Gamma \vdash X:\mu \tau .\alpha }{\Gamma \vdash X:[\mu \tau .\alpha /\tau ]\alpha }}
 {\frac {\Gamma \vdash [\mu p.\alpha /p]\alpha }{\Gamma \vdash \mu p.\alpha }}:  {\frac {\Gamma \vdash X:[\mu \tau .\alpha /\tau ]\alpha }{\Gamma \vdash X:\mu \tau .\alpha }}
「証明＝プログラム」対応に関連する話題 > ド・ブランの役割

ニコラース・ホーバート・ド・ブランはラムダ記法を証明検証器Automathにおいて用い、また命題をその証明の類として表現した。これはハワードが（CH対応に関する）原稿を書いた同時期の1960年後半のことであった。ド・ブランはハワードの仕事を知らず独立してこの対応を述べた（Sørensen & Urzyczyn [1998] 2006, pp 98–99）。一部の研究者[誰?]は、カリー＝ハワード対応という代りにカリー＝ハワード＝ド・ブラン対応という語を使用する。
「証明＝プログラム」対応に関連する話題 > BHK解釈

BHK解釈は直観主義的な証明の含意と全称化を関数として解釈するが、解釈における関数のクラスがどのようなものであるかを指定してはいない。もし関数のクラスとしてラムダ計算を取るならば、BHK解釈は自然演繹とラムダ計算との間の対応と同じことを述べていることになる。
「証明＝プログラム」対応に関連する話題 > 実現可能性解釈

スティーヴン・コール・クリーネの実現可能性解釈は、直観主義的算術の証明を再帰的関数とその関数が論理式を実現していることを表す論理式の証明とに分離する。これにより、例えば「任意の自然数 a と b に対して、a と b を割り切る最大の自然数 c が存在する」ことを直観主義的に証明できたならば、ここから最大公約数を計算する再帰的関数と、それが最大公約数を計算していることの証明を抽出できる。
ゲオルク・クライゼルにより変更された実現可能性解釈を高階の直観主義論理に適用することで、もとの論理式の証明からそれを実現する単純型付けされたラムダ項を帰納的に抽出できることが示せる。命題論理の場合、これはカリー＝ハワード対応のステートメントと一致する：抽出されたラムダ項はもとの証明（をラムダ項と見做したもの）と一致し、実現可能性のステートメントは抽出されたラムダ項がもとの論理式の意味する型を持つということの言い換えである。
クルト・ゲーデルのディアレクティカ解釈は計算可能汎関数を備えた直観主義的算術（のある拡張）を実現する。これのラムダ計算との繋がりは自然演繹ほど明白ではない。
「証明＝プログラム」対応に関連する話題 > カリー＝ハワード＝ランベック対応

ヨアヒム・ランベックは1970年始めに直観主義命題論理とデカルト閉圏の等式理論と対応するある種の型付きコンビネータとの対応関係の証明を示した。このカリー＝ハワード＝ランベック対応は直観主義論理、型付きラムダ計算およびデカルト閉圏との間の対応として知られる。ここではオブジェクトは型あるいは命題に、モルフィズムは項あるいは証明に解釈される。この対応は等号レベルに於いて働き、カリー＝ハワード対応にあるような構文的・構造的同等性を表現しない：すなわち、デカルト閉圏のモルフィズムの構造と、対応する判定のヒルベルト流あるいは自然演繹の証明の構造と比較することはできない。もちろん構文的に対応するような証明体系を構成することはできる。この区別を明確にするために、デカルト閉圏の構文的な構造を次のように言い換える。すなわちデカルト閉圏を型付きの等式理論として形式化する。
オブジェクト（型）は次のように帰納的に定義される：
\top  はオブジェクトである、
\alpha  と  \beta  がオブジェクトならば、  \alpha \times \beta  と  \alpha \rightarrow \beta  はオブジェクトである。
モルフィズム（項）は次のように帰納的に定義される：
id、 \star 、 \operatorname {eval} 、 \pi _{1} と  \pi _{2} はモルフィズムである、
t がモルフィズムならば  \lambda t はモルフィズムである、
t と  u がモルフィズムならば  \langle t,u\rangle  と  u\circ t はモルフィズムである。
Well-definedなモルフィズム（型付きの項）は以下の型付け規則にしたがって構成される：
恒等射：
合成:
終対象:
直積:
射影:
カリー化:
評価:
最後に、圏の等式を次により定める：
id\circ t=t,t\circ id=t,(v\circ u)\circ t=v\circ (u\circ t),
\star \circ t=\star ,
\pi _{1}\circ \langle t,u\rangle =t,\pi _{2}\circ \langle t,u\rangle =u,\langle \pi _{1}\circ t,\pi _{2}\circ t\rangle =t,
eval\circ \langle \lambda t,id\rangle =t,\lambda eval=id.
このとき、 t:\alpha _{1}\times \ldots \times \alpha _{n}\longrightarrow \beta  なるモルフィズム  t が存在することと、 \alpha _{1},\ldots ,\alpha _{n}\vdash \beta  なるシークエントが直観論理の含意論理積断片で証明可能であることとは同値である。上記のデカルト閉圏の射の等式体系として得られる計算模型はカテゴリカルコンビネータあるいは圏的コンビネータ論理として知られる。
| 論理 | 圏論 |
| --- | --- |
論理式: オブジェクト
含意  \alpha \supset \beta : 指数  \alpha \to \beta 
論理積  \alpha \wedge \beta : 直積  \alpha \times \beta 
論理和  \alpha \vee \beta : 余積  \alpha +\beta 
真  \top : 終対象  1
偽  \bot : 始対象  0
証明: モルフィズム
証明図の合成・カット: モルフィズムの合成
例

カリー＝ハワード対応により、型付けられた表現は対応する論理式の証明と見做すことができる。以下、いくつかの例を与える。
例 > 恒等コンビネータと α → α のヒルベルト流の証明

簡単な例として  \alpha \to \alpha  のヒルベルト流の証明を構成する。ラムダ計算では、これは恒等関数  I=\lambda x.x の型であり、コンビネータ論理では恒等関数は  S と  K により  I=SKK （ただし慣例によって適用は左結合と見做す）と表現できる。以上の説明は  \alpha \to \alpha  の証明の構成を与えている。実際、この論理式は次のようにしてヒルベルト流の証明体系にて証明可能である（慣例に従い含意記号は右結合と見做す）：
第二の公理図式から  (\alpha \to (\beta \to \alpha )\to \alpha )\to (\alpha \to \beta \to \alpha )\to \alpha \to \alpha  を得る、
第一の公理図式から  \alpha \to (\beta \to \alpha )\to \alpha  を得る、
第一の公理図式から  \alpha \to \beta \to \alpha  を得る、
モーダス・ポネンスを2回適用して  \alpha \to \alpha  を得る。
例 > 合成コンビネータと (β → α) → (γ → β) → γ → α のヒルベルト流の証明

もっと複雑な例として、 B コンビネータに対応する定理を示そう。 B の型は  (\beta \to \alpha )\to ((\gamma \to \beta )\to (\gamma \to \alpha )) である。 B は  S(KS)K に対応する（この事実は抽象除去などを用いて得られる）。これは目的の定理の証明の道筋を与えている。
まず  KS を構成する。公理  K の前にまず公理  S の形を見る。そして公理  K の  \alpha  に公理  S の論理式を代入する。すると次が得られる：
ここで  S:(\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma  とモーダス・ポネンスにより、
次にこの論理式と公理  S の最初の部分  \alpha \to \beta \to \gamma  とが同一になるような代入を求め（ユニフィケーション）、
を得る。これと先の論理式にモーダス・ポネンスを適用すれば、
この論理式の最初の部分  \delta \to \alpha \to \beta \to \gamma  と公理  K:\alpha \to \beta \to \alpha  とが同一になるような代入を求めれば、それは  \delta =\beta \to \gamma  であるから、
最後にこれらにモーダス・ポネンスを適用すれば次を得る：
適当に命題変数の名前を付け替えれば所望の論理式の証明が得られる。
例 > (β → α) → (γ → β) → γ → α の自然演繹における証明とラムダ項

次の図は  (\beta \to \alpha )\to (\gamma \to \beta )\to \gamma \to \alpha  の自然演繹における証明である。簡単のため、文脈  \Gamma \vdash  は省略してある。
{\dfrac {\dfrac {{\begin{matrix}{}\\x:\beta \rightarrow \alpha \end{matrix}}\quad {\dfrac {y:\gamma \rightarrow \beta \quad z:\gamma }{yz:\beta }}}{\dfrac {x\,(yz):\alpha }{\lambda z.x\,(yz):\gamma \rightarrow \alpha }}}{\dfrac {\lambda y.\lambda z.x\,(yz):(\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }{\lambda x.\lambda y.\lambda z.x\,(yz):(\beta \rightarrow \alpha )\rightarrow (\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }}}
この証明が型付きラムダ項  \lambda x.\lambda y.\lambda z.x(yz) と解釈できることは明らかである。なお、前述の   (\beta \to \alpha )\to (\gamma \to \beta )\to \gamma \to \alpha  のヒルベルト流の証明は、自然演繹におけるこの証明に対して抽象の除去とη変換を何度か使用することで得られる。
その他の応用

最近ではカリー＝ハワード対応が遺伝的プログラミングにおける探索空間のパーティションを定義する方法として提案されている。この手法は遺伝子型（システムにより進化するプログラムの木）の集合に対して（種と呼ばれる）カリー＝ハワード対応する証明を索引付ける。
参照文献

↑  Sørenson, Morten; Urzyczyn, Paweł, Lectures on the Curry-Howard Isomorphism, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385
↑  Goldblatt, “7.6 Grothendieck Topology as Intuitionistic Modality”, Mathematical Modal Logic: A Model of its Evolution, pp. 76–81, http://homepages.mcs.vuw.ac.nz/~rob/papers/modalhist.pdf
↑  Benton; Bierman; de Paiva (1998), “Computational types from a logical perspective”, Journal of Functional Programming 8:  177–193
↑  F. Binard and A. Felty, "Genetic programming with polymorphic types and higher-order functions." In Proceedings of the 10th annual conference on Genetic and evolutionary computation, pages 1187 1194, 2008.
参照文献 > 歴史的な文献

Curry, Haskell (1934), “Functionality in Combinatory Logic”, Proceedings of the National Academy of Sciences, 20, pp. 584–590 .
Curry, Haskell B.; Feys, Robert (1958), Craig, William, ed., Combinatory Logic Vol. I, Amsterdam: North-Holland , with 2 sections by William Craig, see paragraph 9E.
De Bruijn, Nicolaas (1968), Automath, a language for mathematics, Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in: Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970, Springer Verlag, 1983, pp. 159–200.
Howard, William A. (September 1980) [original paper manuscript from 1969], “The formulae-as-types notion of construction”, in Seldin, Jonathan P.; Hindley, J. Roger, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston, MA: Academic Press, pp. 479–490, ISBN 978-0-12-349050-6 .
参照文献 > 哲学的解釈

de Queiroz, Ruy J.G.B. (1994), “Normalisation and language-games”, Dialectica, 48, pp. 83–123, http://www3.interscience.wiley.com/journal/119262585/abstract?CRETRY=1&SRETRY=0 . (Early version presented at Logic Colloquium '88, Padova. Abstract in JSL 55:425, 1990.)
de Queiroz, Ruy J.G.B. (2001), “Meaning, function, purpose, usefulness, consequences – interconnected concepts”, Logic Journal of the Interest Group in Pure and Applied Logics, 9, pp. 693–734, http://jigpal.oxfordjournals.org/cgi/content/abstract/9/5/693 . (Early version presented at Fourteenth International Wittgenstein Symposium (Centenary Celebration) held in Kirchberg/Wechsel, August 13–20, 1989.)
de Queiroz, Ruy J.G.B. (2008), “On reduction rules, meaning-as-use and proof-theoretic semantics”, Studia Logica, 90, pp. 211–247, http://www.springerlink.com/content/27nk266126k817gq/ .
参照文献 > 総合的な論文

De Bruijn, Nicolaas Govert (1995), “On the roles of types in mathematics”, in Groote, Philippe de, The Curry–Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain), 8, Academia-Bruyland, pp. 27–54, ISBN 978-2-87209-363-2, http://alexandria.tue.nl/repository/freearticles/597627.pdf , the contribution of de Bruijn by himself.
Geuvers, Herman (1995), “The Calculus of Constructions and Higher Order Logic”, in Groote, Philippe de, The Curry–Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain), 8, Academia-Bruyland, pp. 139–191, ISBN 978-2-87209-363-2 , contains a synthetic introduction to the Curry–Howard correspondence.
Gallier, Jean H. (1995), “On the Correspondence between Proofs and Lambda-Terms”, in Groote, Philippe de, The Curry–Howard isomorphism, Cahiers du Centre de logique (Université catholique de Louvain), 8, Academia-Bruyland, pp. 55–138, ISBN 978-2-87209-363-2, ftp://ftp.cis.upenn.edu/pub/papers/gallier/cahiers.pdf , contains a synthetic introduction to the Curry–Howard correspondence.
参照文献 > 書籍

edited by Ph. de Groote. (1995), De Groote, Philippe, ed., The Curry–Howard Isomorphism, Cahiers du Centre de Logique (Université catholique de Louvain), 8, Academia-Bruylant, ISBN 978-2-87209-363-2 , reproduces the seminal papers of Curry-Feys and Howard, a paper by de Bruijn and a few other papers.
Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998], Lectures on the Curry–Howard isomorphism, Studies in Logic and the Foundations of Mathematics, 149, Elsevier Science, ISBN 978-0-444-52077-7, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385 , notes on proof theory and type theory, that includes a presentation of the Curry–Howard correspondence, with a focus on the formulae-as-types correspondence
Girard, Jean-Yves (1987–90). Proof and Types. Translated by and with appendices by Lafont, Yves and Taylor, Paul. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7), ISBN 0-521-37181-3, notes on proof theory with a presentation of the Curry–Howard correspondence.
Thompson, Simon (1991). Type Theory and Functional Programming Addison–Wesley. ISBN 0-201-41667-0.
Poernomo, Iman; Crossley, John; Wirsing; Martin (2005) [2005], Adapting Proofs-as-Programs: The Curry–Howard Protocol, Monographs in Computer Science, Springer, ISBN 978-0-387-23759-6 , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
F. Binard and A. Felty, "Genetic programming with polymorphic types and higher-order functions." In Proceedings of the 10th annual conference on Genetic and evolutionary computation, pages 1187 1194, 2008.
de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina G.; Gabbay, Dov M. (2011) [2011], The Functional Interpretation of Logical Deduction, Advances in Logic, 5, Imperial College Press / World Scientific, ISBN 978-981-4360-95-1 .
安曇瑠理

安曇 瑠理（あずみ るり）とは、マイクロソフトの技術解説漫画に登場するキャラクターである。
概要

マイクロソフトのクラウドプラットフォーム、Microsoft Windows Azureの技術解説漫画に登場する、キャラクターである。声優は伊藤かな恵
大きな丸めがねと、京都弁がトレードマーク。髪型は姫カット。特技はイラスト制作。
『クラウドガール -碧空にはばたく籠の小鳥-編』で、初登場。クラウディア・窓辺から技術指南をうける、新人のシステムエンジニアである。
2013年12月29日に開催されたコミックマーケット85では、瑠理のシステムボイス入りのテーマパックが同封されたタブレットPCが販売された。
2014年2月26日にMicrosoft Windows Azureに日本データセンターが設立されたのを機に、クラウディアや瑠理が登場するCM動画が公開された。
下九沢

| 下九沢 |
| --- | --- |
 大字
 北緯35度34分32秒 東経139度20分44秒﻿ / ﻿北緯35.575686度 東経139.345631度﻿ / 35.575686; 139.345631
国:   日本
都道府県:   神奈川
市町村:   相模原市
行政区:  中央区・緑区
地区:  横山地区（中央区） 橋本地区・大沢地区（緑区）

 人口情報（2020年（令和2年）10月1日現在）
 人口:  20,039 人
 世帯数:  8,409 世帯

 面積（）
 :  0.876338005 km²
人口密度:  22866.75 人/km²
郵便番号:  252-0254（中央区） 252-0134（緑区）
市外局番:  042（相模原MA）
ナンバープレート:  相模
 ウィキポータル 日本の町・字  ウィキポータル 神奈川県  ウィキプロジェクト 日本の町・字
テンプレートを表示
下九沢（しもくざわ）は、神奈川県相模原市緑区及び中央区の地名である。住居表示未実施区域。
地理

神奈川県相模原市中央区の西部から緑区の東部に位置する。
地理 > 河川

鳩川
地理 > 地価

住宅地の地価は、2023年（令和5年）1月1日の公示地価によれば、緑区下九沢字中宮1868番13の地点で9万8800円/m2となっている。
歴史 > 沿革

1871年（明治4年）11月14日 - 府県統合により神奈川県に編入。
1954年（昭和29年）11月20日 - 相模原町が市制施行、相模原市となる。
2010年（平成22年）4月1日 - 相模原市が政令指定都市に移行。
世帯数と人口

2020年（令和2年）10月1日現在（国勢調査）の世帯数と人口（総務省調べ）は以下の通りである。
| 区・大字 | 世帯数 | 人口 |
| --- | --- | --- |
| 中央区下九沢 | 1,707世帯 | 4,019人 |
| 緑区下九沢 | 6,702世帯 | 16,020人 |
| 計 | 8,409世帯 | 20,039人 |
世帯数と人口 > 人口の変遷

国勢調査による人口の推移。
| 年 | 人口 |
| --- | --- |
1995年（平成7年）: 18,191
2000年（平成12年）: 18,296
2005年（平成17年）: 17,939
2010年（平成22年）: 18,599
2015年（平成27年）: 19,679
2020年（令和2年）: 20,039
世帯数と人口 > 世帯数の変遷

国勢調査による世帯数の推移。
| 年 | 世帯数 |
| --- | --- |
1995年（平成7年）: 6,247
2000年（平成12年）: 6,715
2005年（平成17年）: 6,796
2010年（平成22年）: 7,311
2015年（平成27年）: 8,038
2020年（令和2年）: 8,409
事業所

2021年（令和3年）現在の経済センサス調査による事業所数と従業員数は以下の通りである。
| 大字 | 事業所数 | 従業員数 |
| --- | --- | --- |
| 中央区下九沢 | 127事業所 | 2,796人 |
| 緑区下九沢 | 413事業所 | 4,445人 |
| 計 | 540事業所 | 7,241人 |
事業所 > 事業者数の変遷

経済センサスによる事業所数の推移。なお、中央区と緑区の地域の合算である。
| 年 | 事業者数 |
| --- | --- |
2016年（平成28年）: 535
2021年（令和3年）: 540
事業所 > 従業員数の変遷

経済センサスによる従業員数の推移。なお、中央区と緑区の地域の合算である。
| 年 | 従業員数 |
| --- | --- |
2016年（平成28年）: 6,497
2021年（令和3年）: 7,241
神社・寺院

八坂神社
御嶽神社
横山稲荷神社
公園・施設 > 公園

相模原北公園
相模原北公園スポーツ広場
相模原市立北総合体育館
公園・施設 > 施設

相模原北清掃工場
LCA国際小学校北の丘センター
下九沢分水地
相模原市立作の口小学校
相模原市立内出中学校
上中ノ原団地
大沢団地
下九沢団地
八坂神社
御嶽神社
横山稲荷神社
交通 > 道路

国道129号
神奈川県道63号相模原大磯線
神奈川県道508号厚木城山線
学校・教育 > 幼稚園・保育園

あかね幼稚園
てるて幼稚園
むくどり風の丘こども園
むくどりこども園
学校・教育 > 小学校

相模原市立作の口小学校
学校・教育 > 中学校

相模原市立内出中学校
産業 > 工業

日本電気相模原事業所
産業 > 商業

スーパー公正屋 下九沢店
業務スーパー 橋本店
ヤオコー 相模原下九沢店
オーケー 下九沢店
ina21 相模原下九沢店
セブンイレブン 相模原中ノ原店
セブンイレブン 相模原塚場店
セブンイレブン 相模原宮之上店
セブンイレブン 相模原あじさい通り店
ファミリーマート 相模原下九沢店
ファミリーマート 作の口小学校前
ローソンストア100 相模原中ノ原店
ローソンストア100 下九沢竹ノ内店
ローソン・スリーエフ 南橋本店
相模・下九沢温泉 湯楽の里
クリエイトSD 新相模原下九沢店
ウェルパーク 相模原下九沢店
はま寿司 相模原下九沢店
ガスト 相模原下九沢店
ほっともっと 下九沢店
ホルモン市場 下九沢店
ピザーラ橋本下九沢店
からやま 南橋本店
その他 > 日本郵便

各区の郵便番号、郵便局は、以下の通りである。
| 区 | 郵便番号 | 郵便局 |
| --- | --- | --- |
| 中央区 | 252-0254 | 相模原郵便局 |
| 緑区 | 252-0134 | 橋本郵便局 |
啄木鳥探偵處

| 啄木鳥探偵處 |
| --- | --- |
ジャンル: ミステリ
小説
著者: 伊井圭
出版社: 東京創元社
レーベル: 創元クライム・クラブ 創元推理文庫
アニメ
原作: 伊井圭
総監督: 江崎慎平
監督: 牧野友映
シリーズ構成: 岸本卓
脚本: 岸本卓、宮尾百合香
キャラクターデザイン: 原修一
音楽: 高田龍一、高橋邦幸
アニメーション制作: ライデンフィルム
製作: 「啄木鳥探偵處」製作委員会
放送局: TOKYO MXほか
放送期間: 2020年4月 - 6月
話数: 全12話
テンプレート - ノート
プロジェクト: アニメ
ポータル: 文学・アニメ
『啄木鳥探偵處』（きつつきたんていどころ）は、東京創元社より発売された伊井圭による日本のミステリ小説。収録作の「高塔奇譚」は第3回創元推理短編賞受賞作。
書誌情報

伊井圭『啄木鳥探偵處』東京創元社
創元クライム・クラブ、1999年5月発売、ISBN 4-488-01281-7
創元推理文庫、2008年11月21日発売、ISBN 978-4-488-48301-2
テレビアニメ

2020年4月から6月までTOKYO MXほかにて放送された。
2019年3月23日、AnimeJapan2019において、東北新社の声優オーディション「キミコエ・プロジェクト」がミステリー小説「啄木鳥探偵處」のTVアニメ化を発表。第2回オーディショングランプリ受賞者・林幸矢、準グランプリ受賞者・古沢勇人、オーディションの見届け人を務めた津田健次郎の出演も明かされた。エンディング主題歌は第1回オーディション受賞者ユニット・NOW ON AIRが担当する。
テレビアニメ > スタッフ

原作 - 伊井圭（創元推理文庫）
総監督 - 江崎慎平
監督 - 牧野友映
シリーズ構成 - 岸本卓
キャラクター原案 - 佐木郁
キャラクターデザイン - 原修一
プロップデザイン - 荒木一成
美術監督 - 伊藤友沙
美術設定 - 平澤晃弘
色彩設計 - 辻田邦夫
撮影監督 - 野澤圭輔
編集 - 長谷川舞
CGディレクター - 前島亮太
音響監督 - 清水洋史
音楽 - 高田龍一、高橋邦幸
音楽制作 - MONACA
制作プロデューサー - 伊達毅、大屋光子、後藤満里子
アニメーションプロデューサー - 佐々木悠祐
アニメーション制作 - ライデンフィルム
制作 - 東北新社、ライデンフィルム
製作 - 「啄木鳥探偵處」製作委員会（東北新社、MUSE、クランチロール、TOKYO MX、ビーエスフジ、マーベラス、ハピネット）
テレビアニメ > 放送局

|  放送期間  |  放送時間  |  放送局  |  対象地域  |  備考  |
| --- | --- | --- | --- | --- |
|  2020年4月13日 - 6月29日 |  月曜 23:00 - 23:30 |  TOKYO MX  |  東京都  |  製作参加  |
|  2020年4月14日 - 6月30日 |  火曜 0:00 - 0:30（月曜深夜） |  BSフジ  |  日本全域  |  製作参加 / BS放送 / 『アニメギルド』枠    |
|  |  |  ファミリー劇場  |  日本全域  |  CS放送  |
|  2020年4月18日 - 7月4日 |  土曜 17:00 - 17:30 |  岩手めんこいテレビ  |  岩手県  |   |
|  2020年5月5日 - 7月28日 |  火曜 1:54 - 2:21（月曜深夜） |  長崎文化放送  |  長崎県  |  『あに。』枠      |
|  配信開始日  |  配信時間  |  配信サイト  |
| --- | --- | --- |
|  2020年4月14日 |  火曜 12:00 更新 |  dアニメストア  |
|  2020年4月19日 |  日曜 12:00 更新 |   Amazonプライム・ビデオ  DMM.com  GYAO!  GYAO!ストア  Hulu  music.jp  Paravi  Rakuten TV  U-NEXT  あにてれ  アニメ放題  バンダイチャンネル  ファミリー劇場CLUB  ひかりTV  ビデオマーケット  ミレール   |
|  |  日曜 21:30 - 22:00 |  ニコニコ生放送  |
|  2020年4月20日 |  月曜 0:00（日曜深夜） 更新 |   J:COMオンデマンド  TELASA  みるプラス   |
|  |  日曜 2:00（日曜深夜） 更新 |  ABEMA  |
|  |  月曜 22:00 更新 |   ファミ劇Neo  ファミ劇Neoプラス   |
テレビアニメ > BD / DVD

| 巻 | 発売日 | 収録話 | 規格品番> BD特装版 | 規格品番> BD通常版 |
| --- | --- | --- | --- | --- |
| 一 | 2020年7月3日 | 第1話 - 第3話 | BIXA-1291 | BIBA-3451 |
| 二 | 2020年8月5日 | 第4話 - 第6話 | BIXA-1292 | BIBA-3452 |
| 三 | 2020年9月2日 | 第7話 - 第9話 | BIXA-1293 | BIBA-3453 |
| 四 | 2020年10月2日 | 第10話 - 第12話 | BIXA-1294 | BIBA-3454 |
テレビアニメ > 漫画

テレビアニメのコミカライズ作品が『ヤングマガジンサード』（講談社）にて2020年Vol.7から2021年Vol.5まで連載され、『月刊ヤングマガジン』（同）に移籍して2021年Vol.6にて完結。
伊井圭（原作）・南晋也（漫画）・佐木郁（キャラクター原案）・東北新社（監修）『啄木鳥探偵處』講談社〈ヤンマガKCスペシャル〉、全2巻
2021年2月19日発売、ISBN 978-4-06-522306-2
2021年8月19日発売、ISBN 978-4-06-524338-1
メリッサ・マシスン

メリッサ・マシスン（Melissa Mathison, 1950年6月3日 - 2015年11月4日）は、アメリカ合衆国カリフォルニア州ロサンゼルス出身の脚本家。
人物

1982年の『E.T.』でアカデミー脚本賞にノミネートされた。
私生活では1983年に俳優のハリソン・フォードと結婚し子供を二人もうけたが、2004年に離婚した。
2015年11月4日、病気のためロサンゼルスで死去。65歳没。