Alloyでλ計算（完全版）

Formal Alloy

ついに、Alloy を使って完全な λ計算 (β簡約) を表現できた…。（前回 は中途半端だった。）
なかなか面白いのは、Alloy がうまくノードを使って無駄なくβ簡約しているところ（Ω=(λx.xx)(λx.xx) で Ω→Ωなど。後に載せる）。

(8/22)フレーム条件のバグを直した。

悩んだ点：破壊的なβ簡約と共有

今までに考えたλ式の表現では、項に共有が生じ得る。例えば、 let f=λx.x in f f のような項ができる。 一方、β簡約を定義するとき、次のような 破壊的操作 を伴う：

  1. 関数呼び出しを関数本体に置き換え
  2. 関数本体の仮引数を実引数に置き換え

たとえば、 let f=λx.x in f f → f のように簡約されてほしいのだが、上記の方法だと右手のfも破壊されてしまうので、正しい簡約にならない。

Alloy でグラフのコピーを作るには

共有がある場合にはコピーを作っておくことで、破壊の影響を受けないようにした。 ただし Alloy では、再帰的な関数(fun)や述語(pred)の定義ができないので、グラフをトラバースしてコピーを作るような操作は書けない。どうするか？
ここでAlloyは関係論理をベースにしていることを思い出そう。 t2はt1のコピーである、という関係 copy(t1,t2) を作れば、コピーを得られるはずだ。
具体的には、

sig Term { copy : set Term }

という風にフィールドを宣言すれば、 2項関係を作ったことになるので、あとはファクトで「コピーである」とはどういうことかを書けばいい。
また構文木は簡約により変化してしまうので、「ノードがコピー同士である」というのは状態に依存する一時的な性質だ。そこで

sig Term { copy : set Term -> State }

のようにして、状態が決まるとコピーか否かが決まるようにしておく。 (更に書くと、 copy(t1,t2,s) という述語を、 状態sの一つ前の状態におけるt1のコピーを、状態sのt2とする、という意味になるようファクトを書いた）。

モデル図

例のごとくStateでprojectしている。 copy のエッジを無視すれば、正しいβ簡約ができていることがわかるはず。

let f=λx.xx in f f (いわゆる Ω→Ω )

ノード数に無駄がないことに注目。

let f=λxy.x in f f → λzxy.x


コード

open util/ordering[State] as ord // 簡約を、状態の順序で表現

// 状態
some sig State {}

// λ式 (コピー機能つき)
abstract sig Term {
  // t1 -> t2 -> s2 in copy で，状態s2の直前のs1におけるt1の構造を状態s2のt2にコピー
  // (自分自身を指す場合もある)
  copy : Term set -> State 
}

// 変数ノード
sig Var extends Term {}
// λ抽象ノードと関数適用ノード
abstract sig Term1 extends Term { left : Term lone -> State }
sig Abs extends Term1 { bind : Var }
sig App extends Term1 { right : Term lone -> State }

// 項に循環がない (DAGをつくる)
fact nocycle { all s:State | no t: Term | t in t.^(left.s+right.s)  }
// 自由変数はない/λ式の束縛変数は衝突しない（変数を束縛しているλ抽象はただ1つ）
fact oneparent_var { all v:Var | one v.~bind }
// スコープを守る（λ抽象ノードを経由せず辿り着ける変数は存在しない）
fact nofreevar { all s:State | 
  no v:Var | 
   let abs=v.~bind | // 変数を束縛しているλ抽象
   let path = (Term-abs) <: (left.s+right.s) | // このλ抽象を経由しないすべてのパス
   v in Root.^path  
}

// 根
one sig Root extends Term1 { }
// 根は他のノードの子にならない
fact rootIsRoot { no t:Term | some s:State | Root in t.(left.s+right.s) }

// 述語：根からたどれる
pred reachable(s:State, t:Term) {
  t in Root.*(left.s+right.s)
}


/****
  根からたどれるλ式を作る
****/
// 根からたどれるすべての関数適用は引数をもつ
fact appHasChild { all s:State | all t:App | 
  reachable[s,t] iff
  one l2:Term | t.right.s=l2 } 
// 根からたどれるすべての子持ち項は子をもつ
fact term1HasChild { all s:State | all t:Term1 |
  reachable[s,t] iff
  one l1:Term | t.left.s=l1 }


/****
  コピーの定義
****/
fact factCopy {
  // 状態s1における項tをコピーしたものが状態s2における項cである、とは、
 (all s2:State, t,c : Term | t -> c -> s2 in copy =>
  some s1:ord/prev[s2] | // 直前の状態をs1とする
  // 変数の場合、それを束縛するλ式同士がコピーであればよい
  (t in Var => c in Var and ((t.~bind) -> (c.~bind) -> s2 in copy))  and
  // その他の場合、ノード種が同じ、かつ子要素同士がコピーであればよい
  (t in Abs => 
   c in Abs and
   some l1:t.left.s1, l2:c.left.s2 | (l1 -> l2 -> s2) in copy) and
  (t in App => 
   c in App and
   some l1:t.left.s1, l2:c.left.s2 | (l1 -> l2 -> s2) in copy and
   some r1:t.right.s1, r2:c.right.s2 | (r1 -> r2 -> s2) in copy)) and
 // 根のコピーはない
 all s2:State | Root.copy.s2 = none 
}


/****
  動作意味の定義
****/
// 置換
pred replace[s1,s2:State, x:Term, v:Term] {
    all parent : x.~(left.s1+right.s1) | // その変数の親を全てもってきて
    // 次の状態でvに置換する
    (parent.left.s1=x implies parent.left.s2 = v) and
    (parent.right.s1=x implies parent.right.s2 = v)
}

// s1におけるtのコピーを,s2につくる(tにexceptFor以外の親がある場合のみ)
pred makeCopyIfShared[s1,s2:State, t:Term, exceptFor:Term] {
  all parent : t.~(left.s1+right.s1) - exceptFor |
  one c : t.copy.s2 | 
  (parent.left.s1=t implies parent.left.s2=c) and
  (parent.right.s1=t implies parent.right.s2=c)
}

// parentとtの間のエッジに変化がない
pred notChange[s1,s2:State, parent:Term, t:Term] {
  (parent.left.s1=t => parent.left.s2=t) and
  (parent.right.s1=t => parent.right.s2=t)
}

// β簡約の定義
pred beta[s1,s2:State, a:App] {
    some f : Abs | f=a.left.s1 and // 左手はλ抽象
    // 簡約される関数が複数の親をもっていた場合コピー
    makeCopyIfShared[s1, s2, f, a] and
    //関数適用の親を関数本体に置換
    let body = f.left.s1 | //関数本体
    replace[s1, s2, a, body] and
    // 仮引数を実引数(のコピー)に置換
    some v : a.right.s1 | // 右手(実引数)
    let x = f.bind | // 変数
    some v.copy.s2 and // let f = .. in f f のときに項が破壊されるのでコピーを使う
    replace[s1, s2, x, v.copy.s2] and

    // フレーム条件 (ノードとその親を結ぶエッジに変化はない)
    all t:Term | reachable[s1,t] =>
     // 関数適用(全て関数本体に置換)とλ抽象(共有があれば必ずコピーされる)と
     // 変数ノード(全て実引数に置換)は消えるので除外
     !(t=a or t=f or t=x) => 
     all parent : t.~(left.s1+right.s1) | 
      // 簡約で消えるエッジ (関数適用,実引数)と(λ抽象,関数本体)を除外
      !((t=v and parent=a) or (t=body and parent=f)) => 
      notChange[s1,s2,parent,t]
}

// 必ずどこかでβ簡約する
fact factBeta {
  all s1 : State, s2 : ord/next[s1] {
    // 根からたどれる関数適用を持ってくる
    some t : App | reachable[s1,t] and 
    // tをβ簡約
    beta[s1,s2,t]
  }
}

run {} for 8 but 2 State, 2 App // 速い
//run {} for 10 but 3 State, 2 App
//run {} for 10 but 2 State

//Ω→Ωのような項を発見するのに使う
//fact { let s1 = ord/first[] | let s2 = ord/next[s1] | Root.left.s1 -> Root.left.s2 -> s2 in copy}

/**** 
  初期状態で項の共有を防ぐ場合
****/
// left,rightはAbs,Appについて木をつくる（各ノードの親は高々1つかつ互いに素）
/*fact oneparent { 
  let s=ord/first[] |
  all t:Term1 | lone t.(~(left.s+right.s)) && disj [t.~(left.s), t.~(right.s)] 
}*/