日々の流転

λ. H↔Provable([H]) な H の真偽

不動点定理によって、任意の一変数論理式P(X)に対して、ある論理式Qが存在して ⊢ Q↔P([Q]) が成り立つ。ゲーデル文Gはそうして作った ⊢ G↔¬Provable([G]) を満たす論理式だった。ゲーデル文は直観的には「この文は証明できない」と解釈でき、この意味から(標準モデルで)真であることがわかる。

では、同様に不動点定理を使って作った ⊢ H↔Provable([H]) を満たす論理式 H の真偽はどうなっているだろうか?　直観的には「この文は証明出来る」という解釈できるのだが、別にそこから真偽が決まるわけでもなく……

最近知って、ちょっと面白かった話(答えは知ってます→20070916#p01)。

λ. length (filter p xs) ≦ length xs の証明

syd_sydさんの「Coqでクイックソート (未完)」を見て、length (filter p xs) ≦ length xs をAgdaで証明してみた(Filter.agda)。 ここから以下の2つを示すことが出来、クイックソートでの再帰呼び出しで引数が小さくなっていることを示すことが出来る。

• length (filter (\y -> y < x) xs) ≦ length xs < length (x:xs)
• length (filter (\y -> x <= y) xs) ≦ length xs < length (x:xs)