keigoi https://blog.hatena.ne.jp/keigoi/ keigoiの日記 https://keigoi.hatenadiary.org/ Formal Alloy ついに、Alloy を使って完全な λ計算 (β簡約) を表現できた…。（前回 は中途半端だった。） なかなか面白いのは、Alloy がうまくノードを使って無駄なくβ簡約しているところ（Ω=(λx.xx)(λx.xx) で Ω→Ωなど。後に載せる）。(8/22)フレーム条件のバグを直した。 悩んだ点：破壊的なβ簡約と共有 今までに考えたλ式の表現では、項に共有が生じ得る。例えば、 let f=λx.x in f f のような項ができる。 一方、β簡約を定義するとき、次のような 破壊的操作 を伴う： 関数呼び出しを関数本体に置き換え 関数本体の仮引数を実引数に置き換え たとえば、 let f=λ… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fkeigoi.hatenadiary.org%2Fentry%2F20110821%2F1313906553" title=" Alloyでλ計算（完全版） - keigoiの日記" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> https://cdn-ak.f.st-hatena.com/images/fotolife/k/keigoi/20110821/20110821144543.png Hatena Blog https://hatena.blog 2011-08-21 15:02:33 rich https://keigoi.hatenadiary.org/entry/20110821/1313906553 1.0 100%