Luna Flow
日本語

syntax チュートリアル

このチュートリアルでは、Term[T] で束縛子を持つ項を構築し、表示し、どの変数が自由かを調べ、束縛変数の名前を除いて項を比較し、捕獲なしに変数をリネームする。最後に、BindingSyntax を実装する任意の AST で動く解析を書く。

クイックスタート

moon add Luna-Flow/type_theory@0.2.0
import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
}

恒等関数 λx. x\lambda x.\,x は自由変数を持たず、λx. y\lambda x.\,y は 1 つ持つ。

test "quick start: free variables" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let id : @syntax.Term[Int] = Bind(x, Variable(x))
  let k : @syntax.Term[Int] = Bind(x, Variable(y))
  assert_eq(@syntax.free_variables(id).length(), 0)
  assert_true(@syntax.free_variables(k).contains(y))
}

日常的な作業

小さなヘルパーで項を構築する

@core.Name::new をあちこちに書くと煩雑になる。ヘルパーを一度定義しておく。

fn v(name : String) -> @syntax.Term[Int] {
  @syntax.Variable(@core.Name::new(name))
}

fn lam(name : String, body : @syntax.Term[Int]) -> @syntax.Term[Int] {
  @syntax.Bind(@core.Name::new(name), body)
}

fn app(f : @syntax.Term[Int], args : Array[@syntax.Term[Int]]) -> @syntax.Term[Int] {
  @syntax.Apply(f, args)
}

test "the K combinator" {
  let k = lam("x", lam("y", v("x")))
  assert_true(k is Bind(_, Bind(_, Variable(_))))
  assert_eq(app(k, [v("a")]), @syntax.Apply(k, [v("a")]))
}

Term は独自のテキスト形式を持たない。適切な記法はそれがエンコードする言語によって決まるからである。ラムダ記法のプリンタは短い再帰関数で書ける。

fn show(t : @syntax.Term[Int]) -> String {
  match t {
    Value(n) => n.to_string()
    Variable(x) => x.text()
    Apply(f, args) => {
      let parts = [show(f), ..args.map(show)]
      "(" + parts.join(" ") + ")"
    }
    Bind(x, body) => "λ" + x.text() + ". " + show(body)
  }
}

test "print λf. f 1" {
  let f = @core.Name::new("f")
  let t : @syntax.Term[Int] = Bind(f, Apply(Variable(f), [Value(1)]))
  inspect(show(t), content="λf. (f 1)")
}

束縛された名前を除いて項を比較する

== は項を字面どおりに比較する。alpha_equal は束縛変数の名前を無視し、ほとんどの場合こちらが望む比較である。

test "λx. x and λy. y" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let a : @syntax.Term[Int] = Bind(x, Variable(x))
  let b : @syntax.Term[Int] = Bind(y, Variable(y))
  assert_false(a == b)
  assert_true(@syntax.alpha_equal(a, b))
}

自由変数を安全にリネームする

λy. x\lambda y.\,x で x を y にリネームしたとき、λy. y\lambda y.\,y になってはならない。rename_free はまず束縛子をリネームする。

test "renaming avoids capture" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let t : @syntax.Term[Int] = Bind(y, Apply(Variable(x), [Variable(y)]))
  let r = t.rename_free(@core.Renaming::singleton(x, y))
  let y1 = @core.Name::new("y_1")
  let expected : @syntax.Term[Int] = Bind(y1, Apply(Variable(y), [Variable(y1)]))
  assert_eq(r, expected)
}

自由な x は y になり、束縛子は y_1 になったので、新しい y は自由なままである。

定数の型を変える

map_values は定数を変換し、束縛構造には手を触れない。ここでは整数リテラルが浮動小数点リテラルになる。

test "map Int constants to Double" {
  let x = @core.Name::new("x")
  let t : @syntax.Term[Int] = Bind(x, Apply(Variable(x), [Value(2)]))
  let d : @syntax.Term[Double] = t.map_values(n => n.to_double())
  assert_true(d is Bind(_, Apply(_, [Value(2.0)])))
}

さらに進んで

束縛を扱うすべての AST に対する解析を書く

BindingSyntax に対して書いた関数は、Term[T] にも、このトレイトを実装する任意の下流 AST にも使える。次の関数は束縛子を数える。

fn[N : @syntax.BindingSyntax] count_binders(node : N) -> Int {
  match @syntax.BindingSyntax::project(node) {
    Opaque | Variable(_) => 0
    Apply(head, args) =>
      args.fold(init=count_binders(head), (acc, a) => acc + count_binders(a))
    Bind(_, body) => 1 + count_binders(body)
  }
}

test "count binders generically" {
  let x = @core.Name::new("x")
  let t : @syntax.Term[Int] = Bind(x, Apply(Bind(x, Variable(x)), [Value(0)]))
  assert_eq(count_binders(t), 2)
}

adapter チュートリアルでは独自の AST に BindingSyntax を実装する。そうすれば count_binders、汎用の代入、汎用の書き換えがすべて適用できる。

束縛子を手動でリネームする

部品から束縛子を構築する場合、alpha_rename_bound はその変数の名前を変更し、本体ですでに使われている名前は拒否する。

test "rename the variable of a binder" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let body : @syntax.Term[Int] = Apply(Variable(x), [Variable(y)])
  assert_true(body.alpha_rename_bound(x, y) is None)
  match body.alpha_rename_bound(x, z) {
    Some(renamed) => {
      let before : @syntax.Term[Int] = Bind(x, body)
      let after : @syntax.Term[Int] = Bind(z, renamed)
      assert_true(@syntax.alpha_equal(before, after))
    }
    None => fail("z is unused")
  }
}

よくある落とし穴

  • == は α同値ではない。 代入や正規化の結果には y_1 のようにリネームされた束縛子が含まれうる。alpha_equal で比較すること。
  • 値の内部の変数。 Value(T) の中身は決して調べられない。定数が変数を含むなら、Term で包むのではなく、独自の AST に BindingSyntax を実装すること。
  • 束縛子に対して alpha_rename_bound を呼ぶ。 これは本体を期待する。Bind(x, body).alpha_rename_bound(...) ではなく body.alpha_rename_bound(x, z) と書く。前者ではリネームすべき自由な x が見つからない。
  • メソッド形式のトレイト呼び出し。 term.project() は非推奨である。@syntax.BindingSyntax::project(term) と書くこと。

次のステップ