脱関数化を実用する B - shiatsumat/fp-papers GitHub Wiki

[§5.3.2](脱関数化を実用する 5#section5-3-2) で与えられた正当性の判断基準を証明するために、

• P₁(r,s,k) ≜ accept (r, s, k) ~> True ⇔ s ∈ L(r)L(k)
• P₂(k,s) ≜ pop_and_accept (k, s) ~> True ⇔ s ∈ L(r)L(k)
• P₃(r,s,k) ≜ accept_star (r, s, k) ~> True ⇔ s ∈ L(r)^＊L(k)

とし、相互整礎帰納法によってそれぞれの命題に尺度を与え、どの場合の証明も真に小さい命題にのみ依存するようにする。この命題の尺度は自然数の組として与えられ、辞書順で並べられる。

• |P₁(r,s,k)| = (|s|, |r|_|s| + |k|_|s|)

• |P₂(k,s)| = (|s|, |k|_|s|)

• |P₃(r,s,k)| = (|s|, |r|_|s| ( 3|s| + 2 ) + |k|_|s|)

  • ただし |s| は s の要素数である。

• |Zero|_n = 1

• |One|_n = 1

• |Char c|_n = 1

• |Sum r1 r2|_n = |r1|_n + |r2|_n

• |Cat r1 r2|_n = |r1|_n + |r2|_n + 2

• |Star r|_n = ( 3n + 2 ) |r|_n

• |Empty|_n = 0

• |Accept r k|_n = |r|_n + |k|_n + 1

• |AcceptStar s r k|_n = |r|_{min( 3(n+1), 3|s| )} + |k|_n

それぞれの場合についての証明は以下の通りである。

accept (r, s, k) ~> True も s ∈ L(Zero)L(k) = ∅ も成り立たないので、同値は成り立つ。

accept (r, s, k) ~> True は pop_and_accept (k, s) ~> True と同値である。整礎帰納法の仮定より、pop_and_accept (k, s) ~> True は s ∈ L(k) と同値であり、L(One) = {[]} であるので、s ∈ L(One)L(k) である。

accept (r, s, k) ~> True は s = c : s' かつ pop_and_accept (k, s') ~> True であることと同値である。その場合、|s'| < |s| かつ |P₂(k,s')| < |P₁(Char c,s,k)| である。帰納法の仮定より s' ∈ L(k) であるので、s = [c] ++ s' ∈ L(Char c)L(k) である。

accept (r, s, k) ~> True は accept (r1, s, k) ~> True または accept (r2, s, k) ~> True であることと同値である。|r|_n は常に正であるので、両方とも「より小さい」から、帰納法の仮定より s ∈ L(r1)L(k) または s ∈ L(r2)L(k) であることと同値であると分かる。さらにこれは s ∈ (L(r1)L(k)) ∪ (L(r2)L(k)) = (L(r1)∪L(r2))L(k) = L(r)L(k) と同じである。

accept (r, s, k) ~> True は accept (r1, s, Accept r2 k) ~> True と同値である。

順序のより小さい P₁(r1,s,Accept r2 k) により、これが s ∈ L(r1)L(Accept r2 k) = L(r1)L(r2)L(k) = L(r)L(k) と同値であると分かる。

accept (r, s, k) ~> True は accept_star (r1, s, k) ~> True と同値であると分かる。ゆえに、代わりにただ P₃(r1,s,k) を証明すればよい。

accept_star (r1, s, k) ~> True は pop_and_accept (k, s) ~> True または accept (r1, s, AcceptStar s r1 k) ~> True であることと同値である。

前者の場合は s ∈ L(k) ⊂ L(k)^＊L(k) と同値である。これは P₂(k,s) が「より小さい」ので、帰納法の仮定より言える。

後者の場合は s ∈ L(r1)L(AcceptStar s r1 k) = L(r1) ( (L(r1)^＊L(k)) ∖ {s} ) と同値である。これも帰納法の仮定より言える。

集合に対する基本演算を使うことで、これら2つの述語の論理和を取るのは、s が和集合に入っているということと同値である。つまり言い換えると、s ∈ (L(r1)⁰ ∪ (L(r1) ∖ {[]})L(r1)^＊)L(k) = L(r1)^＊L(k) である。

ただし、P₃(r1,s,k) は P₁(Star r1,s,k) より真に小さくはないが、ここでは P₃(r1,s,k) を仮定していないので問題ない。

s ∈ L(k) であり、これは s が空文字列であることと同値であり、まさにこのとき pop_and_accept (k, s) ~> True が成り立つ。

s ∈ L(k) = L(r)L(k') であり、これは帰納法の仮定より accept (r, s, k') ~> True と同値である。（P₁(r,s,k') は P₂(Accept r k',s) よりも 1 だけ小さい。）この場合、pop_and_accept (k, s) ≡ accept (r, s, k') ~> True である。

s ∈ L(k) は s ≠ s' かつ s ∈ L(r)^＊L(k') であることと同値である。帰納法の仮定より、s ∈ L(r)^＊L(k') は accept_star (r, s, k) ~> True と同値であり、不等式は Haskell のプログラムに反映されているので、s /= s' ~> True である。これらを合わせると、s ∈ L(k) が成立することは pop_and_accept (k, s) が成立することと同値である。

この場合は P₁(Star r.s,k) の中の部分帰納法と同様に証明される。実際、|P₃(r,s,k)| = |P₁(Star r.s,k)| である。