capture avoiding substitution

• egg/lambda.rs at main · egraphs-good/egg · GitHub の書き換えルールでわからなかった
• (λx.λy.xy) y は λy.yy を得るけどこの y は違う(shadowingしている) のでそれを避けたい = capture avoiding substitution という.
• 方法
  • かぶらないようにrenameする

(λx.λy.xy) y ->
λy.x y{y\x} ->
λz.x z{y\x} ->
λz.(x z{y\x}) ->
λz.yz

ルール

• v1{e\v2} -> e if v1 == v2 else v1
• e1 e2{e3\v} -> {e1 {e3\v}} {e2{e3\v}}
• λv1.e1 {e2\v2} -> λv1.(e1{e2\v2}) if v1 != v2 && v1 nin free(e2)

let <v> <e> <succ>

<succ> に後続の式を書く

>> (app (lam ?x (lam ?y (app ?x ?y))) ?y)
best cost: 8
(Explanation
(app (lam ?x (lam ?y (app ?x ?y))) ?y)
(Rewrite=> beta (let ?x ?y (lam ?y (app ?x ?y))))
(Rewrite=> let-lam-diff (lam ?y (let ?x ?y (app ?x ?y))))) # not-free
(lam ?y (let ?x ?y (app ?x ?y)))

参考文献

• A Brief Explanation of Capture-Avoiding Substitution