カリー／ハワード論理の6つのリーズナーの記法

リーズナー〈reasoner〉は、{定理|証明}コンビネータのこと。

1. ; （二項）
2. （二項）
3. （二項）
4. ◇ （任意項）
5. □ （任意項）
6. Λ （単項）

p, qが{定理|証明}で、Pが{定理|証明}のインデックス族とするときの適用結果は：

1. p;q
2. pq
3. pq
4. ◇P
5. □P
6. Λp

ただし、は'∧'に輪（丸囲み）、は'∨'に輪の記号がふさわしい。書けないので代用した。記号のオーバーロードを許すなら：

• ∧, , ◇ に同じ記号∧
• ∨, , □ に同じ記号∨

ただし、ウェッジとビッグラムダ（アッパーケース・ギリシャ文字のラージサイズ）が区別できない。手書きのときは、ビッグラムダの右脚を真っ直ぐに書く。（フォントと視認性の問題）

演算子の記法の多様性を避けるために、結合的演算に関して二項中置記法とタプル・ポーランド記法〈tuppled Polish notation〉を暗黙セクション規約（混乱がないなら、セクション括弧を付けなくてもセクションとみなす）で運用する。

1. p;q = ;(p, q)
2. pq = (p, q)
3. pq = (p, q)
4. p◇q = ◇(p, q)
5. p□q = □(p, q)
6. Λp = Λ(p)

";(p, q)" はさすがにヤバいので (;)(p, q) か comp(p, q) か SeqComp(p, q)。

[追記]

Λ〈大きなラムダ | カリー化 | 関数抽象 | ラムダ抽象 | 含意導入 | 指数転置〉は除いて、他の5つのコンビネータをまとめる。

番号	名前	記号	二項	n項
1	直列結合	;	f;g	f1;f2;...;fn
2	並列結合		fg	f1f2...;fn
3		？		fg	f1f2...fn
4	？タプリング	◇	f◇g	f1◇f2◇...◇fn
5	？コタプリング	□	f□g	f1□f2□...□fn

定義：

1. (f₁;f₂;...;f_n)(x) := f_n(...(f₂(f₁(x)))...)
2. (f₁f₂...;f_n)(x₁, x₂, ..., x_n) := (f₁(x₁), f₂(x₂), ..., f_n(x_n))
3. f₁f₂...f_n := case x of x∈X₁ => f₁(x), x∈X₂ => f₂(x), ..., x∈X_n => f_n(x) end
4. (f₁◇f₂◇...◇f_n)(x) := (f₁(x), f₂(x), ..., f_n(x))
5. f₁□f₂□...□f_n := case x of x∈X₁ => f₁(x), x∈X₂ => f₂(x), ..., x∈X_n => f_n(x) end

前置記法：

番号	n項	前置記法	項数
1	f1;f2;...;fn	(;)(f1, f2, ..., fn)	有限項
2	f1f2...;fn	()(f1, f2, ..., fn)	有限項
3	f1f2...fn	()(f1, f2, ..., fn)	有限項
4	f1◇f2◇...◇fn	(◇)(f1, f2, ..., fn)	有限項、無限項
5	f1□f2□...□fn	(□)(f1, f2, ..., fn)	有限項、無限項

[/追記]