カリー／ハワード／ジラール対応の陳述

次のように述べることができるだろう。

1. 前もって、命題変数と型名（型記号、型変数）の対応があるとする。
2. 命題論理式と型表現（type expression）の翻訳をτで示す。
3. 命題論理式Pの（仮定なし）証明と、τ(P)で型付けされた閉じたラムダ式が対応する。
4. 証明の中間に出てくる各論理式Qには、型がτ(Q)の変数が対応する。
5. 証明の各推論には、項の構成規則と型推論が対応する。（項の構成規則と型推論は一体）
6. 証明の簡約とラムダ式の計算が対応する。
7. 簡約済みの証明は正規形ラムダ式に対応する。

注意

1. true, falseの定数は入れない。
2. ∨や¬も入らない。
3. 2成分以上のタプルを扱ってもよい。

タプルに関する変型

1. (t.1, t.2) ⇒ t
2. (x, y).1 ⇒ x
3. (x, y).2 ⇒ y

       t

 --------------[Dup]

  t         t

 ---[Sel1] ----[Sel2]

  t.1      t.2

 --------------[And]

     t.1∧t.2

これをストレートに。雰囲気は ◇⇒｜ 。

  x     y

 ---------[And]

   x∧y

  -----[Sel1]

    x

これをストレートに。雰囲気は Y ⇒ ＼ ⇒ ｜、 Y ⇒ ／ ⇒ ｜ 。

[追記]
引き伸ばし変型のまとめ：

1. ∩∪ ⇒ ｜ （β）
2. ∪∩ ⇒ ｜ or ｜⊃ ⇒ ｜ （η）
3. ◇ ⇒ ｜
4. Y ⇒ ＼
5. Y ⇒ ／

[/追記]