Luna Flow
日本語

research_rewrite チュートリアル

このチュートリアルでは、research_rewrite パッケージの書き換えプロトタイプを実行する。ローカルの等式で部分項を一つ書き換え、記録されたリプレイ義務を検査し、結合子の適用を簡約する。このパッケージは研究専用で、出荷される prover には含まれないため、実験に使うにとどめ、その上に構築しないこと。

クイックスタート

moon.pkg でパッケージをインポートする。

import {
  "Luna-Flow/QED/kernel",
  "Luna-Flow/QED/logic",
  "Luna-Flow/QED/research_rewrite",
}

ローカルの仮定 h : p = q を使って f p を f q に書き換える。

test "quick start" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let bool = @kernel.bool_ty()
  let p = @kernel.mk_var("p", bool)
  let q = @kernel.mk_var("q", bool)
  let f = @kernel.mk_var("f", @kernel.fun_ty(bool, bool))
  let locals = [("h", @kernel.mk_eq(p, q).unwrap())]
  let req = @research_rewrite.research_rewrite_request(
    @research_rewrite.research_local_equality("h"),
    @research_rewrite.research_left_to_right(),
    [@research_rewrite.research_site_comb_arg()], // the argument of f p
  )
  match @research_rewrite.research_rewrite_term_concl(st, pre, locals, @kernel.mk_comb(f, p), req) {
    Rewritten(after, _) => inspect(@kernel.term_to_string(after), content="Comb(Var(f : fun(bool, bool)), Var(q : bool))")
    _ => fail("expected a rewrite")
  }
}

リクエストは、等式（名前で指定するローカル）、方向、置き換える部分項へのパスを指定する。

日常的な作業

リプレイ義務を検査する

各書き換えには、その裏にあるカーネルのステップの記録が付いている。検証はそれらのステップを再構築し、それらが依存していた文脈が欠けていれば失敗する。

test "obligation" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let bool = @kernel.bool_ty()
  let p = @kernel.mk_var("p", bool)
  let q = @kernel.mk_var("q", bool)
  let f = @kernel.mk_var("f", @kernel.fun_ty(bool, bool))
  let locals = [("h", @kernel.mk_eq(p, q).unwrap())]
  let req = @research_rewrite.research_rewrite_request(
    @research_rewrite.research_local_equality("h"),
    @research_rewrite.research_left_to_right(),
    [@research_rewrite.research_site_comb_arg()],
  )
  guard @research_rewrite.research_rewrite_term_concl(st, pre, locals, @kernel.mk_comb(f, p), req)
    is Rewritten(_, obligation) else {
    fail("expected a rewrite")
  }
  inspect(@research_rewrite.research_validate_replay_obligation(st, pre, locals, obligation) is Ok(_), content="true")
  inspect(@research_rewrite.research_validate_replay_obligation(st, pre, [], obligation) is Err(_), content="true")
}

結合子を簡約する

research_simplify_term_concl は、何も変わらなくなるまで結合子定数を展開し β 正規化する。

test "simplify" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let not_p = @kernel.mk_comb(@kernel.ks_mk_const(st, "not").unwrap(), p) // the constant `not` applied to p
  let cfg = @research_rewrite.research_simplify_config(10, true, true, [])
  match @research_rewrite.research_simplify_term_concl(st, pre, [], not_p, cfg) {
    Rewritten(after, obligation) => {
      inspect(@kernel.term_alpha_eq(after, @logic.prop_mk_not(st, pre, p).unwrap()), content="true")
      inspect(obligation.segments.length(), content="1")
    }
    _ => fail("expected a simplification")
  }
  // a variable has nothing to simplify
  inspect(@research_rewrite.research_simplify_term_concl(st, pre, [], p, cfg) is NoChange, content="true")
}

正直な失敗を見る

サポートされないリクエストは、失敗の理由を示す。

test "failures" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let not_p = @kernel.mk_comb(@kernel.ks_mk_const(st, "not").unwrap(), p)
  // a step limit of 0 allows no segment
  let tight = @research_rewrite.research_simplify_config(0, true, true, [])
  match @research_rewrite.research_simplify_term_concl(st, pre, [], not_p, tight) {
    HonestFailure(msg) => inspect(msg, content="step limit exceeded")
    _ => fail("expected a failure")
  }
  // the path asks for an abstraction where there is an application
  let req = @research_rewrite.research_rewrite_request(
    @research_rewrite.research_beta_normalization(),
    @research_rewrite.research_left_to_right(),
    [@research_rewrite.research_site_abs_body()],
  )
  match @research_rewrite.research_rewrite_term_concl(st, pre, [], not_p, req) {
    HonestFailure(msg) => inspect(msg, content="rewrite site expected a lambda abstraction")
    _ => fail("expected a failure")
  }
}

さらに進む

定理で書き換える。 research_explicit_theorem(th) は任意の等式の定理をウィットネスとして使う。たとえば @logic.logic_eq_sym で得た定理である。research_right_to_left() と組み合わせると逆方向に書き換えられる。

リクエストを連鎖させる。 複数のリクエストを SimplifyConfig.rewrite_requests に入れる。各ラウンドでは一致するものが適用され、義務には適用されたステップごとに一つのセグメントが記録される。

研究ノートを読む。 設計と昇格ゲートは research/rewrite-simplify/ にある。昇格に何が足りないかは research_rewrite 設計がまとめている。

よくある落とし穴

  • 定理を期待する。 書き換えが返すのは項と義務である。元のゴールを証明するものは何もない。
  • λ の下で書き換える。 AbsBody のサイトは拒否される。
  • 定義を畳み込む。 CanonicalUnfold と BetaNormalization は左から右にしか働かない。
  • パッケージに依存する。 これは研究専用であり、変更または削除される可能性がある。

次のステップ