ついに、Alloy を使って完全な λ計算 (β簡約) を表現できた…。（前回 は中途半端だった。） なかなか面白いのは、Alloy がうまくノードを使って無駄なくβ簡約しているところ（Ω=(λx.xx)(λx.xx) で Ω→Ωなど。後に載せる）。(8/22)フレーム条件のバグを直した。 悩んだ点：破壊的なβ簡約と共有 今までに考えたλ式の表現では、項に共有が生じ得る。例えば、 let f=λx.x in f f のような項ができる。 一方、β簡約を定義するとき、次のような…

…ロー記事あり前回 (Alloyでλ式をつくる) では、λ式を表現するグラフをAlloyで構築した。 今回は、λ計算の核となるβ簡約の一部をAlloyで記述してみる。 扱えるλ式の制限 面倒だったので、モデルに次の制限を導入した。 このため、正確にはβ簡約とはいいがたい… 項の共有がない (λ式は木になっている) β簡約のとき，λ抽象を破壊して関数本体に置き換えるため，共有されると困る． 具体的には let f = λx.x in f (f x) のような場合に、 片方のfが簡…

Alloyでλ式を作ってみた。 フォロー記事あり あまり役に立たない気はするけど、関係の逆(~)を取ったり(反射)推移閉包(*,^)を使う良い練習になった。（バグがみつかり次第、色々修正している。以下のモデル図はソースを修正しながら作っているので、エンバグされて出なくなっているものもあるかもしれない） 追記(8/20)：簡単な説明 sigで構文木のノードを，sigのフィールドで構文木のエッジを表現した． また，束縛変数を示す bind というエッジを付加した． さらに，ファク…

Alloyの言語仕様をゴリゴリ読み進めていた。 非常に勉強になります。Software Abstractions (1st ed., p.288): So although a quantified constraint with multiple declarations may be regarded, for some quantifiers, as a shorthand for nested constraints, each with one declaratio…

Alloyを使ってみた。 数年前に使ったときはなんでこんなの使うのと思っていたけど考えが変わったのだ。 ちょっとした規模のプログラムを書くには設計が必要だ。 コードを書く前に、問題の本質的な部分を知っておこう。 本質がわかっていれば、 適切な部分にモジュール分割したり、適切なライブラリを選択したり、アルゴリズムを書いたりできるはずだ。 もちろんお絵描きツールでもいいのだけど、動いたりチェックしたりできれば、設計で得られる知見はより多くなるはず。 述語論理で書くけれど、モデルが…