回路図と大きなラムダ計算がキモかな

僕には、既存のコースや教科書を踏襲する必然性も制約もない。だから、ようするに分かりやすくて短時間で説明が完了すればソレデイイノダ。手段は選ばん！

となると、回路メタファーを使うのが早いだろうし、現実世界を記述する道具として位置づけた大きなラムダ式を活用すべきだろう。

ジャンクション（接合器）と回路素子（circuit element）のセットを回路キットと呼んで、特定の回路キットから作れる回路を考えることになる。入り口は算術回路かな。

本来(?)の用語	比喩的な用語
指標	回路キット
プロファイル付き記号	回路素子
パラメータ付きプロファイル付き記号	ジャンクション
ソート	ワイヤーのラベル
変数／値	ワイヤーを流れるデータ／記号的トレーサ
同値	回路の同値

回路キットの雰囲気は、ラキュー（LaQ）の写真でも使うか。電子ブロックが本家か。

命題論理の回路とラムダ計算の回路の場合：

命題論理	ラムダ計算
命題変数	基本型、ソート
論理式	型表現
証明	式（自由変数あり）
前提なしの証明	閉じた式
演繹定理	ラムダ抽象
モダスポネンス	適用
モダスポネンス消去	βη変換

これを使えば、ジラール対応まで説明できるだろう。