ラムダ項近況
前回の記事の要約:
- (A): M →1β N, M ≡α M' ⇒ M' →1β N
- (B): M ▷1β N ⇒ [t/s]M →1β [t/s]N
という二つの命題を証明しようとしたが(A)と(B)の証明が相互依存になってしまって、それを二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法をとった。
その後、定理1.2.37の前提条件を弱めた以下の命題を使えば(A)に依存しない(B)の証明ができると気づいた。
また、証明は証明図の高さに関する帰納法ではなく、Mの長さに関する帰納法にしておけば、帰納法で証明する述語を「…に長さn+1の証明図がある」というように変更しておく必要もなくなる。
とこの問題はまともな方法で相互依存を解消することに成功した。
だけど実は補助定理1.2.36と定理1.2.37はうまく証明できず飛ばしていたのだ。
これもまた相互依存である。補助定理1.2.36と定理1.2.37と以下の代入の交換可能性の3つが絡み合ってしまっている。
この問題の探検において今のところ得られた成果:
- M ≡α N, v ∉ V(MN) ⇒ [v/x]M ≡α [v/y]Nが成立する。
これは1.2.36(2)を弱めたもの。
- M ≡α N ⇒ λx.M ≡α λx.N
ひとつ前の命題の系。
- 1.2.36(2)を証明すれば1.2.36(1)も得られる
短いので証明を書いてみる。
既知とする命題: FV(Q) ∩ BV(M) = ∅, z ∉ V(M) ⇒ [Q/z][z/x]M ≡ [Q/x]M
次の命題を証明する。
M ≡α M', BV(M') ∩ FV(zQ) = ∅となる項M'をとる。
すると上記の既知の命題から、
ここで1.2.36(2)より
よって
□
