ラムダ式と二分木

• V を変数の集合とする．
• 二分木から V∪{*} への写像 e で
  e(σ)∈V ( val(σ) = 0, 1 ), e(σ) = * ( val(σ) = 2 )
  をみたすものはλ式と1対1に対応する．
  • 価数0の頂点が変数，価数1の頂点が抽象，価数2の頂点が適用に対応する．
  • 二分木は変数が1種類のλ式と1対1に対応する．
• val(σ) = 2，val(σ0) = 1 のとき，σ∈dom e を redex という．
  • redex を元とする集合を redex 集合とよぶ．
• λ式 e の redex σに対し，σでβ簡約して得られるλ式を θ_σ(e) と書く．
• λ式 e の redex σ, τに対し，
  • σ≤τ でないならば，τはθ_σ(e) の redex になる．
  • σ, τ が比較可能でないならば， θ_σ(θ_τ(e) ) = θ_τ(θ_σ(e) )．
  • σ0≤τ ならば，θ_σ(e) の redex τ' が存在して， θ_σ(θ_τ(e) ) = θ_τ'(θ_σ(e) )．

• 問題は次が成立しないこと．(λx . M)N をβ簡約するとき，Nの中の redex がコピーされることに注意．
  • σ1≤τ ならば，θ_σ(e) の redex τ' が存在して， θ_σ(θ_τ(e) ) = θ_τ'(θ_σ(e) )．

• もう一つの問題は，たとえば (λx . xN)(λy . M) をβ簡約すると，(λy . M)N となって新たな redex が生じること（N は x を含まないとする）．

そこで，「最初に見えている redex の一部を正しい順番に従ってβ簡約する」という操作をあらわす記号を準備する．

λ式 e の redex 集合 A に対し，A のすべての元に対して順序のより大きい方が先になるような順番でβ簡約したものを θ_A(e) とする．

• • これは well-defined．「正しい順番」は一意ではないが，β簡約した結果は一意的．

• 注意　A としてすべての redex の集合をとった場合でも，θ_A(e) から redex がなくなっているとは限らない．
  • 例　(λx . xx)(λx . xx)

• これを用いると次が言える．

Claim. σ1≤τ ならば，θ_σ(e) の redex 集合 B が存在して， θ_σ(θ_τ(e) ) = θ_B(θ_σ(e) )．

補題

1. λ式 e の redex 集合 A⊂σ↓ に対し，σ∉A ならば，θ_σ(e) の redex 集合 B が存在して，
   θ_σ(θ_A(e) ) = θ_B(θ_σ(e) )．
   • したがって，λ式 e の redex 集合 A⊂σ↓ に対し，σ∈A ならば，θ_σ(e) の redex 集合 B が存在して，
     θ_A(e) = θ_σ(θ_A-{σ}(e) ) = θ_B(θ_σ(e) )．
2. λ式 e の redex 集合 A⊂U - (σ↓) に対し，θ_A(e) の redex 集合 C が存在して，
   θ_A(θ_σ(e) ) = θ_C(θ_A(e) )．

• 証明は，A の元の個数に関する帰納法による．