日々の流転

λ. RHG読書会::東京 Reloaded

.

λ. 素数リスト

RHG読書会後ジョナサンで mini Haskell Marathon と称して数人でコードを書き散らかしたが、その中に僕が書いたコードで素数のリストを以下のように定義するのがあった。

prime :: [Integer]
prime = 2 : [n | n <- [3..], f n]
  where f n = all (\p -> n `mod` p /= 0)
                  (takeWhile (\p -> p <= g n) prime)
        g   = floor . sqrt . fromInteger

こいつが well-defined であることはさすがに自明ではないな。 考えてみると、3以上の任意の自然数nに対して、 floor(√n) < p < n を満たす素数pが存在すれば、 こいつが takeWhile (\p -> p <= g n) に対する番兵になって 無限ループに陥らないはずだ。

n=3 のとき

floor(√n) = 1 < 2 < 3 = n

n≧4 のとき

「ベルトランの仮説(Bertrand's postulate) 」 ∀n∈N. (n≧2 ⇒ ∃p∈N. Prime(p)∧(n < p < 2n)) から、 ある素数pが存在して floor(√n) < p < 2 floor(√n) で、 ここで 2 floor(√n) ≦ √n floor(√n) ≦ n なので、 floor(√n) < p < n 。

というわけで、問題なしと。