Call-By-Valueのlet束縛に関する公理、http://www.cs.bham.ac.uk/~pbl/papers/universalcbv.pdf より： (let val x = x in M) ≡ M (let val x = N in x) ≡ N (xはフレッシュ） (let val x = M in (let val y = N in L)) ≡ (let val y = (let val x = M in N)…

http://d.hatena.ne.jp/m-hiyama-memo/20150318/1426651739 Cオペレーターを入れたラムダ計算をλC と書くことがある。 λCはモッジ（Moggi）のcomputationalラムダ計算のことでもあるな。λμがパリゴ（Parigot）、λμνというのもある。セリンガーの論文に出てい…

フェライゼン（Felleisen）のCオペレーターというのがある。Cオペレーターを入れたラムダ計算をλC と書くことがある。それとパリゴ（Parigot）のラムダミュー計算λμの関係は以下のようだ。λμからλCへの変換＝C変換： M |→ MC μa.M → C(λa.MC) Cにλa.MC を渡…

次の論文をチラ見した。 Title: Synchronous Machines: a Traced Category Authors: Marc Bagnol & Adrien Guatto URL:http://iml.univ-mrs.fr/~bagnol/drafts/synchronous-machines.pdf Marc BagnolとAdrien Guatto（以下、BG）は二人とも博士課程の学生さ…

パリゴ（Parigot）のラムダ・ミュー計算は、なんだか分からなかったが、純関数の計算であるラムダ計算に、コマンドの計算を足したものだと思えばいいかもしれない。コマンドは値を持たず副作用を持つかもしれない。関数の値を捨てればコマンドとなる。コマン…