rewrite API

rewrite パッケージは項の 1 つの位置で書き換え規則を適用し、何が起きたかを正確に報告する：前後の項、規則の名前、根から書き換えられた位置までのパスである。上限付き正規化とトレースは、このような単一ステップを繰り返して構築される。各関数には Term[T] 版があり、注記のある場合は任意の @syntax.BindingSyntax AST 向けの版もある。

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

規則とは関数 (Term[T]) -> Term[T]? であり、項全体に適用できるときは Some(result) を、そうでなければ None を返す。走査関数は規則をどこで試すかを決める。理論は rewrite の設計にある。

規則名

RuleName

RuleName は簡約規則の空でない識別子である。

pub struct RuleName {
  value : String
} derive(Compare, Eq, Hash, @debug.Debug)

規則名は結果やトレースでステップにラベルを付ける。テキストによって比較・順序付け・ハッシュされ、順序は String のもの、すなわち短いテキストが先、次に UTF-16 コード単位による。

RuleName::new

RuleName::new は規則名を検証して作成する。

pub fn RuleName::new(String) -> Result[Self, RuleNameError]

空文字列に対しては Err(RuleNameError::Empty) を、それ以外では Ok(name) を返す。

RuleName::unsafe_new

RuleName::unsafe_new は空でないとわかっている文字列から規則名を作成する。

pub fn RuleName::unsafe_new(String) -> Self

空文字列に対しては中断する。"beta" のように不変条件が明らかなリテラルに使い、入力から来る名前には RuleName::new を使うこと。

RuleName::value

RuleName::value は規則名のテキストを返す。

pub fn RuleName::value(Self) -> String

RuleName::equal, RuleName::compare, RuleName::hash

これらのメソッドは昇格された Eq、Compare、Hash の実装である。

pub fn RuleName::equal(Self, Self) -> Bool
pub fn RuleName::compare(Self, Self) -> Int
pub fn RuleName::hash(Self) -> Int

test "rule names" {
  assert_eq(@rewrite.RuleName::new(""), Err(@rewrite.RuleNameError::Empty))
  match @rewrite.RuleName::new("beta") {
    Ok(name) => inspect(name.value(), content="beta")
    Err(_) => fail("non-empty name rejected")
  }
  // shortlex order: shorter names first
  let eta = @rewrite.RuleName::unsafe_new("eta")
  assert_true(eta < @rewrite.RuleName::unsafe_new("beta"))
}

RuleNameError

RuleNameError は規則名が無効である理由を列挙する。

pub(all) enum RuleNameError {
  Empty
} derive(Eq, @debug.Debug)
pub fn RuleNameError::equal(Self, Self) -> Bool

Empty が唯一のケースである：規則名は空であってはならない。

位置

ReductionFrame

ReductionFrame はノードからその子の 1 つへの 1 ステップである。

pub(all) enum ReductionFrame {
  BinderBody
  ApplyHead
  ApplyArgument(Int)
} derive(Eq, @debug.Debug)
pub fn ReductionFrame::equal(Self, Self) -> Bool

BinderBody は Bind の本体に、ApplyHead は Apply の先頭に、ApplyArgument(i) は 0 から数えて i 番目の引数に入る。

ReductionPath

ReductionPath は根からある位置までのフレームの列である。

pub struct ReductionPath {
  frames : Array[ReductionFrame]
} derive(Eq, @debug.Debug)

空のパスは根を表す。

ReductionPath::root, ReductionPath::prepend, ReductionPath::to_array

これらの関数はパスを構築・読み取りする。

pub fn ReductionPath::root() -> Self
pub fn ReductionPath::prepend(Self, ReductionFrame) -> Self
pub fn ReductionPath::to_array(Self) -> Array[ReductionFrame]

prepend(frame) は根の側にフレームを追加する。走査はこれによって子でのステップのパスを親へ持ち上げる。to_array は根から順にフレームを返す。

ReductionPath::equal

ReductionPath::equal は 2 つのパスをフレームごとに比較する。

pub fn ReductionPath::equal(Self, Self) -> Bool

test "paths are built from the redex up" {
  let path = @rewrite.ReductionPath::root()
    .prepend(@rewrite.ApplyArgument(1))
    .prepend(@rewrite.BinderBody)
  assert_eq(path.to_array(), [@rewrite.BinderBody, @rewrite.ApplyArgument(1)])
  assert_eq(@rewrite.ReductionPath::root().to_array(), [])
}

Term 上の単一ステップ

StepResult

StepResult[T] は簡約を 1 回試みた結果である。

pub(all) enum StepResult[T] {
  NoStep
  Reduced(before~ : @syntax.Term[T], after~ : @syntax.Term[T], rule~ : RuleName, path~ : ReductionPath)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] StepResult::equal(Self[T], Self[T]) -> Bool

NoStep は走査が規則の適用できる位置を見つけられなかったことを意味する。Reduced は項全体 before、項全体 after、規則、書き換えられた位置のパスを記録する。書き換えられた位置はちょうど 1 つである：path における before の部分項はその規則の簡約基であり、after はその部分項を規則の結果で置き換えた before である。

top_down_once

top_down_once は前順で規則が適用できる最初の位置を書き換える。

pub fn[T] top_down_once(@syntax.Term[T], RuleName, (@syntax.Term[T]) -> @syntax.Term[T]?) -> StepResult[T]

規則はノード自身で子より先に試される。子はまず頭部、次に引数を左から右へと訪問され、束縛子の本体にも入る。選ばれる位置は最左最外の簡約基である。NoStep は規則が項のどこにも適用できないことを表す。

bottom_up_once

bottom_up_once は、後行順で規則が適用できる最初の位置を書き換える。

pub fn[T] bottom_up_once(@syntax.Term[T], RuleName, (@syntax.Term[T]) -> @syntax.Term[T]?) -> StepResult[T]

子は親より先に、同じく左から右の順で試される。選ばれる位置は最左最内の簡約基である。NoStep はここでも規則がどこにも適用できないことを表す。

fn drop_zero(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match t {
    Apply(Value("+"), [Value("0"), other]) => Some(other)
    _ => None
  }
}

test "outermost versus innermost" {
  let rule = @rewrite.RuleName::unsafe_new("drop_zero")
  let inner : @syntax.Term[String] = Apply(Value("+"), [Value("0"), Value("1")])
  let outer : @syntax.Term[String] = Apply(Value("+"), [Value("0"), inner])
  match @rewrite.top_down_once(outer, rule, drop_zero) {
    Reduced(after~, path~, ..) => {
      assert_eq(after, inner)
      assert_eq(path.to_array(), [])
    }
    NoStep => fail("expected a step")
  }
  match @rewrite.bottom_up_once(outer, rule, drop_zero) {
    Reduced(after~, path~, ..) => {
      assert_eq(after, Apply(Value("+"), [Value("0"), Value("1")]))
      assert_eq(path.to_array(), [@rewrite.ApplyArgument(1)])
    }
    NoStep => fail("expected a step")
  }
}

Term 上でのステップの反復

NormalizationResult

NormalizationResult[T] はステップ関数を有界回数反復した結果である。

pub(all) enum NormalizationResult[T] {
  NormalForm(term~ : @syntax.Term[T], steps~ : Int)
  StepLimitReached(term~ : @syntax.Term[T], steps~ : Int)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] NormalizationResult::equal(Self[T], Self[T]) -> Bool

NormalForm(term, steps)：ステップ関数が term に対して NoStep を返した。この項は steps ステップ後に到達したものである。StepLimitReached(term, steps)：steps ステップの上限を使い切り、term はまだ簡約可能である。

normalize

normalize は、ステップ関数が NoStep を返すかステップ上限に達するまで、ステップ関数を適用し続ける。

pub fn[T] normalize(@syntax.Term[T], (@syntax.Term[T]) -> StepResult[T], Int) -> NormalizationResult[T]

normalize(term, step, max_steps) は成功するステップを高々 max_steps 回実行し、step を高々 max_steps + 1 回呼び出す。許された最後のステップの後、NormalForm と StepLimitReached のどちらであるかを判定するために step をもう一度呼び出す。max_steps <= 0 の場合はステップを一切実行せず、term の分類だけを行う。簡約戦略はステップ関数が決める。既製のものについては eval を参照。

ReductionTrace

ReductionTrace[T] は有界な実行を記録する。初期項、成功した各ステップ、および最終結果である。

pub struct ReductionTrace[T] {
  initial : @syntax.Term[T]
  steps : Array[StepResult[T]]
  result : NormalizationResult[T]
} derive(Eq, @debug.Debug)
pub fn[T] ReductionTrace::initial(Self[T]) -> @syntax.Term[T]
pub fn[T] ReductionTrace::steps(Self[T]) -> Array[StepResult[T]]
pub fn[T] ReductionTrace::result(Self[T]) -> NormalizationResult[T]
pub fn[T : Eq] ReductionTrace::equal(Self[T], Self[T]) -> Bool

steps の各要素は Reduced 値である。連続するステップは連鎖しており、あるステップの after が次のステップの before となる。steps().length() は result の steps 数に等しい。steps() はコピーを返す。

trace

trace は normalize と同じループを実行し、各ステップを記録する。

pub fn[T] trace(@syntax.Term[T], (@syntax.Term[T]) -> StepResult[T], Int) -> ReductionTrace[T]

fn decrement(t : @syntax.Term[Int]) -> @syntax.Term[Int]? {
  match t {
    Value(n) if n > 0 => Some(Value(n - 1))
    _ => None
  }
}

test "normalize and trace" {
  let rule = @rewrite.RuleName::unsafe_new("decrement")
  let step = (t : @syntax.Term[Int]) => @rewrite.top_down_once(t, rule, decrement)
  assert_eq(
    @rewrite.normalize(Value(3), step, 10),
    NormalForm(term=Value(0), steps=3),
  )
  let run = @rewrite.trace(Value(3), step, 2)
  assert_eq(run.steps().length(), 2)
  assert_eq(run.result(), StepLimitReached(term=Value(1), steps=2))
  assert_eq(run.initial(), Value(3))
}

束縛を扱う AST

GenericStepResult

GenericStepResult[N] は下流の AST N 向けの StepResult である。

pub(all) enum GenericStepResult[N] {
  NoStep
  Reduced(before~ : N, after~ : N, rule~ : RuleName, path~ : ReductionPath)
} derive(Eq, @debug.Debug)
pub fn[N : Eq] GenericStepResult::equal(Self[N], Self[N]) -> Bool

generic_top_down_once

generic_top_down_once は任意の BindingSyntax AST 向けの top_down_once である。

pub fn[N : @syntax.BindingSyntax] generic_top_down_once(N, RuleName, (N) -> N?) -> GenericStepResult[N]

走査は BindingSyntax::project を使って子を見つけ、トレイトのコンストラクタを使って書き換えられたノードの親を再構築する。Opaque ノードと変数ノードには子がないが、規則はそれらに対しても試される。

GenericNormalizationResult

GenericNormalizationResult[N] は下流の AST 向けの NormalizationResult である。

pub(all) enum GenericNormalizationResult[N] {
  NormalForm(term~ : N, steps~ : Int)
  StepLimitReached(term~ : N, steps~ : Int)
} derive(Eq, @debug.Debug)
pub fn[N : Eq] GenericNormalizationResult::equal(Self[N], Self[N]) -> Bool

generic_normalize

generic_normalize は一つの規則で generic_top_down_once を、適用できるステップがなくなるかステップ上限に達するまで繰り返す。

pub fn[N : @syntax.BindingSyntax] generic_normalize(N, RuleName, (N) -> N?, Int) -> GenericNormalizationResult[N]

ステップ数に関する約束は normalize と同じで、戦略はトップダウンに固定されている。

test "generic rewriting on Term" {
  let rule = @rewrite.RuleName::unsafe_new("drop_zero")
  let inner : @syntax.Term[String] = Apply(Value("+"), [Value("0"), Value("1")])
  let outer : @syntax.Term[String] = Apply(Value("+"), [Value("0"), inner])
  assert_eq(
    @rewrite.generic_normalize(outer, rule, drop_zero, 10),
    NormalForm(term=Value("1"), steps=2),
  )
}

下流の AST についてはアダプタのチュートリアルを参照。