syntax API

syntax パッケージは束縛子を持つ名前付き構文を定義する。汎用の項型 Term[T]、その上の解析（自由変数、全名前、α同値）、名前の付け替え、そしてオープンなトレイト BindingSyntax である。下流の AST はこのトレイトを通じて同じ解析と、他のパッケージの汎用代入・書き換えを利用できる。

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
}

これらの関数の背後にある定義とその法則の証明は構文の設計にある。

項

`Term`

Term[T] は、ドメイン値、変数、n 項適用、単一変数の束縛を持つ名前付き構文である。

pub(all) enum Term[T] {
  Value(T)
  Variable(@core.Name)
  Apply(Term[T], Array[Term[T]])
  Bind(@core.Name, Term[T])
} derive(Eq, @debug.Debug)

Value(v) はドメイン定数である。そのペイロード T は不透明であり、閉じたものとして扱われるため、どの解析もその内部を見ない。
Variable(x) は名前 x の出現である。
Apply(head, args) は head を引数の列に適用する。ラムダ計算のパッケージはこれをカリー化された適用 $head\ a_1\ \cdots\ a_n$ と読む。
Bind(x, body) は body の中で x を束縛する。ラムダ計算ではこれは $\lambda x.\,body$ である。下流の言語はこれを任意の一変数束縛子として読んでよい。

==（Term::equal）は構造的等価性であり、束縛子の名前は字面どおり一致しなければならない。束縛変数の名前の付け替えを除いて項を比較するには alpha_equal を使う。

test "build the term λx. f x 1" {
  let x = @core.Name::new("x")
  let f = @core.Name::new("f")
  let term : @syntax.Term[Int] = Bind(
    x,
    Apply(Variable(f), [Variable(x), Value(1)]),
  )
  assert_true(term is Bind(_, Apply(_, [_, Value(1)])))
}

`Term::equal`

Term::equal は二つの項を構造的に比較する。

pub fn[T : Eq] Term::equal(Self[T], Self[T]) -> Bool

これは昇格された Eq の実装である。λx.x と λy.y は equal ではない。

`Term::map_values`

Term::map_values はすべてのドメイン値に関数を適用し、変数と束縛子はそのまま保つ。

pub fn[T, U] Term::map_values(Self[T], (T) -> U) -> Self[U]

これは関手の写像である。t.map_values(v => v) は t であり、f を写してから g を写すことは v => g(f(v)) を写すことに等しい。自由変数は変わらない。

test "map domain values" {
  let x = @core.Name::new("x")
  let term : @syntax.Term[Int] = Apply(Value(2), [Variable(x), Value(3)])
  let shown = term.map_values(v => v.to_string())
  assert_eq(shown, Apply(Value("2"), [Variable(x), Value("3")]))
}

解析

`free_variables`

free_variables は項に自由に出現する名前を返す。

pub fn[T] free_variables(Term[T]) -> @hashset.HashSet[@core.Name]

x の出現は、それを束縛する外側の Bind(x, _) がないとき自由である。値は名前を一切もたらさない。コスト：サイズ $n$ の項に対して $O(n)$ 回の集合演算。

`all_names`

all_names は項に含まれるすべての名前を返す。自由変数、束縛された出現、束縛子の名前である。

pub fn[T] all_names(Term[T]) -> @hashset.HashSet[@core.Name]

項に対して新しい名前を選ぶときの「使用済み」集合として使う。

test "free and all names" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let term : @syntax.Term[Int] = Bind(x, Apply(Variable(x), [Variable(z)]))
  let fv = @syntax.free_variables(term)
  assert_true(fv.contains(z))
  assert_false(fv.contains(x))
  assert_true(@syntax.all_names(term).contains(x))
  assert_false(@syntax.all_names(term).contains(y))
}

`alpha_equal`

alpha_equal は二つの項が束縛変数の名前を除いて等しいかどうかを判定する。

pub fn[T : Eq] alpha_equal(Term[T], Term[T]) -> Bool

値は == で、自由変数は名前で、束縛変数は参照する束縛子で比較される。この関係は同値関係であり、二つの項を同時に一度走査することで判定される。

test "alpha-equivalence ignores binder names" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let left : @syntax.Term[Int] = Bind(x, Apply(Variable(x), [Variable(z)]))
  let right : @syntax.Term[Int] = Bind(y, Apply(Variable(y), [Variable(z)]))
  assert_true(@syntax.alpha_equal(left, right))
  assert_false(left == right)
  let other : @syntax.Term[Int] = Bind(y, Apply(Variable(y), [Variable(y)]))
  assert_false(@syntax.alpha_equal(left, other))
}

名前の付け替え

`Term::rename_free`

Term::rename_free は項の自由変数に名前の付け替えを適用し、捕獲を避けるために必要に応じて束縛子の名前を変える。

pub fn[T] Term::rename_free(Self[T], @core.Renaming) -> Self[T]

Bind(x, body) の下では、束縛された x は別の変数なので、名前の付け替えから x の項目が失われる。付け替えの残りの対象のいずれかが x に等しい場合は、まず束縛子を新しい名前に変える。結果は教科書的な捕獲回避の名前の付け替えと α同値である。

test "rename a free variable without capture" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let term : @syntax.Term[Int] = Bind(y, Variable(x))
  let renamed = term.rename_free(@core.Renaming::singleton(x, y))
  let expected : @syntax.Term[Int] = Bind(@core.Name::new("y_1"), Variable(y))
  assert_eq(renamed, expected)
}

`Term::alpha_rename_bound`

Term::alpha_rename_bound は外側の束縛子によって束縛された変数の出現の名前を変え、捕獲されうる対象名は拒否する。

pub fn[T] Term::alpha_rename_bound(Self[T], @core.Name, @core.Name) -> Self[T]?

束縛子の本体に対して呼び出す。body.alpha_rename_bound(from, to_) は、body の中で自由な（したがって外側の Bind(from, body) に束縛された）from の出現を to_ で置き換える。from という名前の内側の束縛子があると、そこで名前の付け替えは止まる。to_ が body のどこかに出現する場合、結果は None であり、from == to_ の場合は Some(body) である。成功した場合、Bind(from, body) と Bind(to_, result) は α同値である。

test "checked bound renaming" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let body : @syntax.Term[Int] = Bind(y, Variable(x))
  assert_true(body.alpha_rename_bound(x, y) is None)
  let expected : @syntax.Term[Int] = Bind(y, Variable(z))
  assert_eq(body.alpha_rename_bound(x, z), Some(expected))
}

束縛を扱う AST

`BindingView`

BindingView[N] は、汎用アルゴリズムが調べるノードの一層分のビューである。

pub(all) enum BindingView[N] {
  Opaque
  Variable(@core.Name)
  Apply(N, Array[N])
  Bind(@core.Name, N)
}

Opaque はリテラルのように内部に変数を含まないノードを表す。他のケースは Term のコンストラクタに対応し、子は下流の型 N のまま残される。

`BindingSyntax`

BindingSyntax はオープンなトレイトであり、下流の AST はこれを実装することで汎用の束縛アルゴリズムを利用できる。

pub(open) trait BindingSyntax {
  fn project(Self) -> BindingView[Self]
  fn variable(@core.Name) -> Self
  fn apply(Self, Array[Self]) -> Self
  fn bind(@core.Name, Self) -> Self
}

project(node) はノードが何であるかをアルゴリズムに伝える。
variable、apply、bind はそれぞれの種類のノードを再構築する。

実装は project と三つのコンストラクタを整合させなければならない。project(variable(x)) は Variable(x)、project(apply(h, args)) は Apply(h, args)、project(bind(x, b)) は Bind(x, b) であり、射影した Apply または Bind ノードを再構築すると同等のノードが得られる。Opaque ノードは変数を含んではならない。アダプタの設計がこれらの法則を説明し、アダプタのチュートリアルが小さな AST に対してそれらを実装している。

トレイトのメソッドはトレイト経由で呼び出す。例えば @syntax.BindingSyntax::project(node) のようにする。

`impl BindingSyntax for Term`

Term[T] は自明な射影で BindingSyntax を実装している。

pub impl[T] BindingSyntax for Term[T]

Value は Opaque に射影され、他のコンストラクタはすべて同名のケースに射影される。そのため、以下の汎用関数は Term 値に対して Term 版と一致する。

test "project a term" {
  let x = @core.Name::new("x")
  let term : @syntax.Term[Int] = Bind(x, Variable(x))
  match @syntax.BindingSyntax::project(term) {
    Bind(name, _) => assert_eq(name, x)
    _ => fail("expected a binder")
  }
}

`generic_free_variables`, `generic_all_names`

以下の関数は任意の BindingSyntax 型について自由変数と全名前を計算する。

pub fn[N : BindingSyntax] generic_free_variables(N) -> @hashset.HashSet[@core.Name]
pub fn[N : BindingSyntax] generic_all_names(N) -> @hashset.HashSet[@core.Name]

Term[T] 上では、これらは free_variables および all_names と同じ集合を返す。

`generic_alpha_rename_bound`

generic_alpha_rename_bound は任意の BindingSyntax 型向けの Term::alpha_rename_bound である。

pub fn[N : BindingSyntax] generic_alpha_rename_bound(N, @core.Name, @core.Name) -> N?

対象名がノードに出現する場合は None を返す。名前を付け替えたノードは variable、apply、bind を通じて再構築される。

test "generic analyses on a term" {
  let x = @core.Name::new("x")
  let z = @core.Name::new("z")
  let term : @syntax.Term[Int] = Apply(Variable(x), [Bind(z, Variable(z))])
  assert_true(@syntax.generic_free_variables(term).contains(x))
  assert_false(@syntax.generic_free_variables(term).contains(z))
  let renamed = @syntax.generic_alpha_rename_bound(term, x, @core.Name::new("w"))
  assert_true(renamed is Some(Apply(Variable(_), [_])))
}

非推奨

非推奨	代替
`term.project()`	`@syntax.BindingSyntax::project(term)`
`Term::variable(name)` メソッド形式	`Term::Variable(name)`
`Term::apply(head, args)` メソッド形式	`Term::Apply(head, args)`
`Term::bind(name, body)` メソッド形式	`Term::Bind(name, body)`
`term.not_equal(other)`	`term != other`
`term.to_repr()`	`Repr(term)` または `@debug.to_string(term)`

これらのメソッド形式はトレイトメソッドの暗黙の昇格であった。古い呼び出し側が引き続きコンパイルできるよう、隠された非推奨のものとして残されている。

syntax API

項

Term

Term::equal

Term::map_values

解析

free_variables

all_names

alpha_equal

名前の付け替え

Term::rename_free

Term::alpha_rename_bound