全 部 乗 せ 数 式

λ計算からその先へ ── 計算体系の記法カタログ

I. 真面目な「和」

これらの体系は勝手に並んでいるわけではなく、圏論という共通の土俵の上で 「モノイダル圏 + 書き換え関係」 という一つの型に収まります。つまり本当の意味での和は、次の一行です。

𝕊  =  ⟨  𝒞,  ⊗,  I,  →R  ⟩
対象 = 型 / 命題 / 状態  ・  射 = 項 / 証明 / 過程  ・  ⊗ = 並置  ・  →R = 簡約

あとは 𝒞 にどんな公理を足すか、という選択だけで各体系が出てきます。カリー・ハワード・ランベック対応の拡張版です。

体系圏の構造書き換え
λ計算デカルト閉圏（CCC）β簡約
SKIコンビネータCCC の変数なし表示弱簡約
線形論理*-自律圏カット除去
π計算名前の圏 / 前層圏通信簡約
相互作用ネット対称モノイダル圏局所的グラフ書き換え
ZX計算ダガー・コンパクト閉圏スパイダー則
ホモトピー型理論(∞,1)-トポス道の合成・transport
微分λ計算微分圏β + 微分簡約
FRACTRANモノイド ℚ+ の ℕ への部分作用分数の乗算
幾何代数クリフォード代数 Cl(V, q)幾何積
超現実数{L | R} 上の整礎再帰単純化

II. 遊びの「全部乗せ」

記法そのものを一本の式に詰め込むと、こうなります。色は出典ごとに対応しています。

Ω  :=  μX.  !( νa. ( ā⟨X⟩ ∥ a(y).X y ) )  ⊗  𝐒𝐊𝐊  ⊸  {  X ↑↑ X  ∣  X ∧ X  }
[ ⟦∂Ω⟧ZX  ≃refl  ⟦∂Ω⟧ZX ]   ⇓IN ∘ →FRACTRAN
「複製可能な並行プロセスと恒等関数のテンソル積を、超現実数へ線形に写す不動点。
その微分の ZX 図が自分自身と道でつながっているか ── を相互作用ネットで簡約する」
記号出典意味
μX. / 𝐒𝐊𝐊λ計算・コンビネータ論理不動点と、変数を使わない恒等関数
!   ⊗   ⊸線形論理複製の許可・資源の並置・使い捨ての含意
νa. ā⟨X⟩ ∥ a(y).Pπ計算新しいチャネルを作り、送信と受信を並行に走らせる
{ L ∣ R }超現実数（Conway）左右の選択肢から数を生む定義
↑↑Knuth の矢印記法テトレーション（冪の反復）
∧幾何代数外積 ── 面積を持つ量
⟦ − ⟧ZXZX計算・ストリング図項を図式へ翻訳する解釈
≃reflホモトピー型理論等式を「道」とみなす同値
∂微分λ計算プログラムを微分する
[ − ]Iverson 記法命題を 0 / 1 に落とす括弧
⇓IN ∘ →F相互作用ネット・FRACTRAN評価機構と、それを駆動する分数列

III. オチ

この式の値 ── [ … ] が 0 か 1 か ── を決める一般的な手続きは存在しません。左辺が正規形を持つかどうかは停止性問題そのものであり、しかも評価器として据えた FRACTRAN は、まさにコラッツ予想が住んでいる体系です。

記法をいくら足しても、決定不能性は 1 ミリも動かない。最初の問いにそのまま戻ってきます。