← カタログへ戻る #186

線形型工房

線形リソースを「ちょうど1度だけ」使い切る制約パズル。複製も廃棄も禁止。

線形論理 (Girard 1987): 各リソースは 使用1回限り。捨てる (weakening) も複製する (contraction) も禁止。Rust の所有権 / 線形 λ 計算 / 可逆計算における資源管理の理論的基盤。
画面上の 資源 (●)消費ノード (◇) へ運び、すべてを 過不足なく 1対1で消費せよ。
Level 1 Resources 0/0 Sinks 0/0 Moves 0

レベル選択

線形型ルール

  • OK 1リソース → 1消費
  • NO Weakening (廃棄)
  • NO Contraction (複製)
  • NO 同一sinkへ2回
A ⊸ B

判定ログ

操作

クリックで資源を選択 → 消費ノードをクリックで配線。配線済みの線をクリックで切断。判定ですべての資源が「ちょうど1回ずつ」使われているか検証。Undo で1手戻る。
使用しない資源 (weakening) や、同じ資源を2度配線する (contraction) のはどちらも禁止。線形論理では証明木の各仮定を1度ずつ消費する必要がある。