Luna Flow
日本語

research_rewrite API

research_rewrite パッケージ（Luna-Flow/QED/research_rewrite）は、証明ゴールの書き換えと簡約を行う研究用プロトタイプである。ゴールの結論を選んだ位置で書き換え、各ステップをカーネル規則でどのようにリプレイできるかを記録し、その記録を再検査できる。依存するのは kernel と logic のみである。

research_rewrite の設計ではリプレイモデルを説明し、research_rewrite のチュートリアルでは書き換えを実行する。

リクエスト

RewriteWitness、ConnectorKind とそのコンストラクタ関数

RewriteWitness は、どの等式が書き換えを正当化するかを表す。ゴールのローカル仮定（名前で指定）、明示的な定理、結合子の定義、または β 正規化のいずれかである。

pub enum RewriteWitness {
  LocalEquality(String)
  ExplicitTheorem(@kernel.Thm)
  CanonicalUnfold(ConnectorKind)
  BetaNormalization
}

pub enum ConnectorKind {
  Not
  Imp
  And
  Or
}

pub fn research_local_equality(String) -> RewriteWitness
pub fn research_explicit_theorem(@kernel.Thm) -> RewriteWitness
pub fn research_canonical_unfold_not() -> RewriteWitness
pub fn research_canonical_unfold_imp() -> RewriteWitness
pub fn research_canonical_unfold_and() -> RewriteWitness
pub fn research_canonical_unfold_or() -> RewriteWitness
pub fn research_beta_normalization() -> RewriteWitness

ローカルまたは明示的なウィットネスは、等式 l=rl = r を結論としなければならない。結合子の展開は、プレリュード定数の適用を、β 正規化された定義へ書き換える。

RewriteDirection、research_left_to_right、research_right_to_left

RewriteDirection は、ll を rr に置き換えるか、rr を ll に置き換えるかを表す。

pub enum RewriteDirection {
  LeftToRight
  RightToLeft
}

pub fn research_left_to_right() -> RewriteDirection
pub fn research_right_to_left() -> RewriteDirection

右から左への書き換えは、ローカルおよび明示的なウィットネスでのみサポートされる。定義の畳み込みや β 展開は正直に失敗する。

RewriteSiteStep とそのコンストラクタ関数

サイトとは、結論のルートから書き換え対象の部分項へ至るパスである。適用の関数部または引数部へ、あるいは抽象の本体へ進む。

pub enum RewriteSiteStep {
  CombFun
  CombArg
  AbsBody
}

pub fn research_site_comb_fun() -> RewriteSiteStep
pub fn research_site_comb_arg() -> RewriteSiteStep
pub fn research_site_abs_body() -> RewriteSiteStep

空のパスは結論全体を指す。抽象の下（AbsBody）での書き換えはサポートされず、正直に失敗する。

RewriteRequest と research_rewrite_request

リクエストは、ウィットネス、方向、サイトを組み合わせたものである。

pub struct RewriteRequest {
  witness : RewriteWitness
  direction : RewriteDirection
  site : Array[RewriteSiteStep]
}

pub fn research_rewrite_request(RewriteWitness, RewriteDirection, Array[RewriteSiteStep]) -> RewriteRequest

書き換え

research_rewrite_term_concl

research_rewrite_term_concl(state, prelude, locals, concl, request) は、命題 concl に対して書き換えを一度行う。locals は LocalEquality が参照できる名前付き仮定である。

pub fn research_rewrite_term_concl(@kernel.KernelState, @logic.PropPrelude, Array[(String, @kernel.Term)], @kernel.Term, RewriteRequest) -> RewriteResult

1 セグメントのリプレイ義務を伴う書き換え後の結論を返す。または正直な失敗を返す。失敗の原因は、結論が命題でない、サイトが存在しない、ウィットネスが未知であるかサイトの部分項と一致しない、カーネルのステップが失敗する、のいずれかである。

research_simplify_term_concl と SimplifyConfig

research_simplify_term_concl は、何も変わらなくなるまで繰り返し書き換える。各ラウンドで、allow_unfold なら結合子を展開し、allow_beta なら β 正規化を行い、rewrite_requests のうち一致する各リクエストを適用する。step_limit はセグメント数の上限を定める。

pub struct SimplifyConfig {
  step_limit : Int
  allow_unfold : Bool
  allow_beta : Bool
  rewrite_requests : Array[RewriteRequest]
}

pub fn research_simplify_config(Int, Bool, Bool, Array[RewriteRequest]) -> SimplifyConfig
pub fn research_simplify_term_concl(@kernel.KernelState, @logic.PropPrelude, Array[(String, @kernel.Term)], @kernel.Term, SimplifyConfig) -> RewriteResult

適用できるステップがなければ NoChange を返す。step_limit を超えるセグメントが必要になる場合は「step limit exceeded」で、step_limit が負の場合は「step limit must be non-negative」で、正直に失敗する。

RewriteResult

RewriteResult は、書き換えまたは簡約の結果である。

pub enum RewriteResult {
  Rewritten(@kernel.Term, ReplayObligation)
  NoChange
  HonestFailure(String)
}

結果は項と記録であり、定理ではない。書き換え後のゴールを証明するものは、ここには何もない。

リプレイ義務

ReplayStepKind と research_step_name

ReplayStepKind は、セグメントが必要とするカーネルレベルのステップに名前を付ける。ウィットネスの解決、対称性、合同（サイトのステップごとに一つ）、定義の展開、β 正規化である。research_step_name はコンストラクタ名を文字列として返す。

pub enum ReplayStepKind {
  ResolveWitness
  Symmetry
  Congruence
  Unfold
  BetaNormalize
}

pub fn research_step_name(ReplayStepKind) -> String

ReplaySegment、ReplayObligation とそのコンストラクタ関数

セグメントは一回の書き換えを記録する。リクエスト、書き換え前後の結論、そのステップである。義務は、最初の結論から最後の結論までセグメントを連鎖させたものである。

pub struct ReplaySegment {
  request : RewriteRequest
  before_concl : @kernel.Term
  after_concl : @kernel.Term
  steps : Array[ReplayStepKind]
}

pub struct ReplayObligation {
  before_concl : @kernel.Term
  after_concl : @kernel.Term
  segments : Array[ReplaySegment]
}

pub fn research_replay_segment(RewriteRequest, @kernel.Term, @kernel.Term, Array[ReplayStepKind]) -> ReplaySegment
pub fn research_replay_obligation(@kernel.Term, @kernel.Term, Array[ReplaySegment]) -> ReplayObligation

research_validate_replay_obligation

research_validate_replay_obligation(state, prelude, locals, obligation) は、各セグメントをそのリクエストからカーネル規則で再構築し、結果、ステップ、連鎖を義務の記録と比較することで、義務を検査する。

pub fn research_validate_replay_obligation(@kernel.KernelState, @logic.PropPrelude, Array[(String, @kernel.Term)], ReplayObligation) -> Result[Unit, @kernel.LogicError]

手作りの義務や古くなった義務は LogicError で失敗する。

test "rewrite" {
  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())]
  // rewrite the argument of f p with h : p = q
  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(after, obligation) else {
    fail("expected a rewrite")
  }
  inspect(@kernel.term_to_string(after), content="Comb(Var(f : fun(bool, bool)), Var(q : bool))")
  let steps = obligation.segments[0].steps.map(@research_rewrite.research_step_name)
  inspect(steps.join(", "), content="ResolveWitness, Congruence")
  inspect(@research_rewrite.research_validate_replay_obligation(st, pre, locals, obligation) is Ok(_), content="true")
  // without the hypothesis h the obligation does not replay
  inspect(@research_rewrite.research_validate_replay_obligation(st, pre, [], obligation) is Err(_), content="true")
}