Alloyでλ計算（β簡約）する

Alloy Formal

フォロー記事あり

前回 (Alloyでλ式をつくる) では、λ式を表現するグラフをAlloyで構築した。
今回は、λ計算の核となるβ簡約の一部をAlloyで記述してみる。

扱えるλ式の制限

面倒だったので、モデルに次の制限を導入した。 このため、正確にはβ簡約とはいいがたい…

  • 項の共有がない (λ式は木になっている)
    • β簡約のとき，λ抽象を破壊して関数本体に置き換えるため，共有されると困る．
    • 具体的には let f = λx.x in f (f x) のような場合に、 片方のfが簡約されても他方のノードを残しておかなければいけない
  • 変数の共有がない (変数は高々1度しか出現しない)
    • 初期状態においてはこの制限を外せるが、そうすると1回簡約した後に項の共有が生まれる

モデル図

Stateでprojectionしている

λx.(λy.λz.z)x → λx.λz.z


λx.λy.x( (λz.λw.w)(λa.a) ) → λx.λy.x(λw.w)


コード

  • λ抽象の関数本体や関数適用の左手をleft, 関数適用の右手をrightとした
  • 状態遷移を表現するために util/ordering を使った。 これはよくあるやり方で、知らない人は 抽象によるソフトウェア設計 を買うか、がんばって Formally Introducing Alloy Idioms (PDF) を読むといいです。
  • 状態によって構文木が変化するのを表すために、例えば、sig Term1 { left : Term lone -> State } などとしている。
    • こう書くと一見 left は状態を返す関数のように見えるがそうではなく、Term1 * Term * State の3項関係になっている。 lone制約は、状態によっては leftエッジがないことを意図している。
    • 便利なことに、 t.left.s のように書けば、 「状態sにおける tの left側の子」を表すことができる。
    • '.' 演算子が 「結合(join)」であるためにこういうことができる。(t.left) が 2項関係 Term * State を表現するので、さらにStateを左から結合すれば Termが得られる.
  • フレーム条件が必要だった。 具体的には、状態遷移の前後で、β簡約された項以外の木構造は変化していない、ということをファクトで記述している。
open util/ordering[State] as ord // 簡約を、状態の順序で表現

// λ項
abstract sig Term {}
// 変数ノード
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 }

// 状態
some sig State {}

// 循環がない
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 | all v:Var | v.(~(left.s)+ (~(right.s))) in (v.(~bind)).*(left.s+right.s)  }

// 根
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)
}

run {} for 10 but 2 State

/****
  グラフを作る
****/
// 根からたどれるすべての関数適用は引数をもつ
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 }


/**** 
  苦肉の策：共有を防ぐ
****/
// left,rightは木をつくる（各ノードの親は高々1つかつ互いに素）←かなり強い制限になる
fact oneparent { 
  all s : State |
  all t:Term | lone t.(~(left.s+right.s)) && disj [t.~(left.s), t.~(right.s)] 
  }



/****
  動作意味の定義
****/
// 置換
pred subst[s1:State, s2:State, x:Var, v:Term, edge:Term->lone Term->State] {
    all varparent : x.~(edge.s1) | // その変数の親を全てもってきて
    varparent.edge.s2 = v // 次の状態でvに置換する
}

// β簡約
//  簡約対象のAppを指すエッジが leftとrightの場合があるため、 edge としてパラメータ化
pred beta[s1:State, s2:State, a:App, edge:Term->lone Term->State] {
    some f : Abs | f=a.left.s1 and // 左手はλ抽象
    some v : a.right.s1 | // 右手
    some parent : a.~(edge.s1) | //親
    let body = f.left.s1 | //関数本体
    let x = f.bind | // 変数
    parent.edge.s2 = body  and //関数適用の親を関数本体に置き換え
    subst[s1,s2,x,v,left] and subst[s1,s2,x,v,right] // 実引数を仮引数に代入
    // フレーム条件 (残りの項の親に変化はない)
    and all t:Term | (t!=a and t!=f and t!=v and t!=x and t!=body) implies 
    (all parent : t.~(left.s1) | parent = t.~(left.s2)) and
    (all parent : t.~(right.s1) | parent = t.~(right.s2))
}


fact factBeta {
  all s1 : State, s2 : ord/next[s1] {
    some t : App | reachable[s1,t] and // 関数適用を持ってくる
    (beta[s1,s2,t,left] or beta[s1,s2,t,right])
  }
}