Alloyでλ式をつくる

Alloyでλ式を作ってみた。 フォロー記事あり
あまり役に立たない気はするけど、関係の逆(~)を取ったり(反射)推移閉包(*,^)を使う良い練習になった。

（バグがみつかり次第、色々修正している。以下のモデル図はソースを修正しながら作っているので、エンバグされて出なくなっているものもあるかもしれない）

追記(8/20)：簡単な説明

sigで構文木のノードを，sigのフィールドで構文木のエッジを表現した． また，束縛変数を示す bind というエッジを付加した．
さらに，ファクトを用いて

• 循環がない
• 変数以外の項は複数の親に共有されない
• α変換不要 (変数名が衝突しない)
• 変数のスコープが正しい (スコープの外から変数を参照できない)

という制約を記述することで，それらしいグラフを得ることができた．

λx.x

(λxy.yx)(λx.x)

(λx.(λy.y)x)

λx.λy.y(xy)

λx.λy.(x(xx))(yy)

ソース

（うまい人はもっとすっきり書くような気がする）

// λ項
abstract sig Term {}
// 変数ノード
sig Var extends Term {}
// λ抽象ノードと関数適用ノード
abstract sig Term1 extends Term { t1 : Term }
sig Abs extends Term1 { bind : Var }
sig App extends Term1 { t2 : Term }

// 循環がない
fact nocycle { no t: Term | t in t.^(t1+t2)  }
// λ抽象・関数適用は木をつくる（λ抽象・関数適用ノードの親は高々1つかつ互いに素）
fact oneparent { all t:Term1 | lone t.(~(t1+t2)) && disj [t.~t1, t.~t2] }
// 自由変数はない/λ式の束縛変数は衝突しない（変数を束縛しているλ抽象はただ1つ）
fact oneparent_var { all v:Var | one v.(~bind) }
// スコープを守る（変数ノードの親はλ抽象の子孫ノードのどれか）
fact nofreevar { all v:Var | v.((~t1)+(~t2)) in (v.(~bind)).*(t1+t2)  }

// 根
one sig Root { root : Term }
fact rooted { all t:Term | t in (Root.root).*(t1+t2) } // すべての項は根からたどれる

run {} for 10