カリー／ハワード・スタイル論理

言語・習慣・文化のせいで、せっかくの原則がうまく使えない例がカリー／ハワード対応。なんとかしてキレイに整理する。

演繹システムでは不明瞭で、プログラミング・システムでは明瞭な概念：

1. システム組み込み vs ユーザー定義
2. ライブラリによるシステムの拡張、S から S+L へ。
3. 「システム vs ユーザー」と実装責務の境界や分担
4. ライブラリにより拡張されたシステムにおける組み込み機能とは何か？
5. ライブラリのパッケージ／モジュール化
6. ライブラリ（であるパッケージ／モジュール）のロード
7. 冗長性が罪ではないこと。むしろ冗長性が機能性として歓迎される。
8. オペレータとオペランドの区別。プロセス全体のロギング。

プログラミングのレベル：

レベル	オペランド	オペレータ
値レベル	値／データ	関数
型レベル	型	型コンビネータ／コンストラクタ
関数レベル	関数	関数コンビネータ

ポイントフリースタイルは、値レベル・プログラミングから関数レベル・プログラミングへの移行のこと。

カリー／ハワード対応が言葉の問題できれいに対応しないところ： '？'は対応がビミョー、'！'は無理に造語してみた。

型パラメータ	？命題変数、！命題パラメータ
総称型	？真理関数、！総称命題
インデックス付き型	？命題関数、！インデックス付き命題
型コンビネータ	？論理結合子、！命題コンビネータ
依存型コンビネータ	限量子〈量化子 | 限定作用素〉
総称関数	？推論規則、！総称定理
関数コンビネータ	？推論規則、！〈定理 | 証明〉コンビネータ
関数のプロファイル	？定理のステートメント、！〈定理 | 証明〉のプロファイル
関数の定義ボディ	？定理の証明、！定理のボディ
無名関数	？証明

タプル〈リスト | 配列〉もマップも、ファミリーとも言える。ファミリーの書き方は、

• (i∈I |→ F_i)
• (F_i ←| i∈I)

インデックス付き型＝型スキーマ＝型ファミリーだとして、型ファミリーと関数ファミリーに対して、依存型コンビネータ＝インデックス付き型からのコンビネータと、インデックス付き関数からのコンビネータが定義できる。

型コンビネータ	結合子／限量子
Prod, ×	∧
Sum, +	∨
Fun, ⇒	⇒
IProd, Σ	∀
ISum, Π	∃

関数コンビネータの対応物は、型コンビネータに比べて整理されてない。

関数コンビネータ	証明図操作
SeqComp, ;	スタック〈積み〉
ParComp,	併置
Pair, < , >	∧導入規則
Copair, [ , ]	∨除去規則
Tupple, < | ∈ >	∀導入規則
Cotupple, [ | ∈ ]	∃除去規則

残念ながら、総称関数に対応するモノも推論規則と呼んでいるので、推論規則の対応物が曖昧になってしまっている。以下は、推論規則とは呼ばないで組み込み総称定理と呼ぶべきだろう。

組み込み総称関数	組み込み総称定理	備考
id[A]	--id[A]
π[A, B](i),i=1,2	--π[A, B](i),i=1,2	射影
ι[A, B](i),i=1,2	--ι[A, B](i),i=1,2	入射
![A]	--![A]	終射
θ[A]	--θ[A]	始射
ε[A, B]	--ε[A, B]	評価、適用
π[F](a),a∈X	--π[F](a),a∈X	依存積射影
ι[F](a),a∈X	--ι[F](a),a∈X	依存和入射

リーズニングは：

1. 組み込み総称関数〈論理的公理〉を自由に選んでよい。
2. 選んだ組み込み総称関数を具体化してよい。
3. 定理コンビネータ＝リーズナーを自由に選んでよい。
4. リーズナーに命題パラメータが入っているので、自由に具体化してよい。
5. 分野特有の組み込み定理〈理論の公理〉を自由に選んでよい。
6. 選んだり具体化した公理・定理に対して、リーズナーによる操作をしてよい。
7. 操作の過程はリーズニング図として記録する。

一般に、オペランド〈入力〉にオペレーションしてリザルト〈出力〉が得られ、それの繰り返しがプロセス〈過程〉記録になる。

最終結果〈ファイナルリザルト〉から、プロセスを再現できるかどうかは。式からパーズツリーを得ることと同じ。