ラムダバブルを二重丸、三重丸で描くと少し図が簡略になる。そのとき、もとの（カリー化する前の）関数のアリティ（引数の個数）を知りたいなら、丸の数を0, 1, 2, ... と勘定し、それと、上に出ている線の本数を足す。丸の数は0から勘定する、なぜなら一番…

備忘。

まず、コンパクトシーケントとは、コンパクト論理のシーケントで、左辺と右辺のカンマの解釈が同じもの。古典論理のシーケントとは違う。次のような規則を使う。 Γ ⇒ Δ,Δ' Δ',Ψ ⇒ Φ ----------------------------[右Cut] Γ,Ψ ⇒ Δ,Φ Γ ⇒ Δ',Δ Ψ,Δ' ⇒ Φ ------…

自然演繹とシーケント計算の関係は圏の圏化になっているような気がする。圏化とは、イコールを同型で置き換えることだが、一般化すると、nセルのイコールを(n+1)の可逆セルで置き換えることだ。書き換えルールや書き換え系が重要な例。書き換えルールの適用…