このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

Cオペレーターとラムダミュー計算

プログラム意味論 トレース／コンパクト閉圏

フェライゼン（Felleisen）のCオペレーターというのがある。Cオペレーターを入れたラムダ計算をλC と書くことがある。それとパリゴ（Parigot）のラムダミュー計算λμの関係は以下のようだ。

λμからλCへの変換＝C変換： M |→ MC

  • μa.M → C(λa.MC) Cにλa.MC を渡す
  • [a]M → (a MC) a に MC を渡す

その他は構文を保って自明な変換。

λCからλμへの変換＝逆C変換： M |→ M-

  • CM → μa.M-(λf.[a]f)
  • 補助的に AM ≡ C(λz.M) zはダミー変数

Aはabortオペレーターと呼ばれる。

callccは、

  • callcc ≡ λf.μa.[a](f(λg.μb.[b]g))