val it: α → α = fun

もしくはハッカーは算数に弱いという話。

皆さんは、ある自然数が与えられたとき、その数が11の倍数かどうかを判定する方法を知っているだろうか。

3の倍数かどうかを判定するとき、10進数表記にして各ケタの数字を合計し、その合計が3の倍数であればもとの数も3の倍数、という判定方法は知っている人が多いと思う。似たようなやつに11の倍数というのがあるのですよ。

その方法では、各ケタを1つずつ飛ばして足す。すると1つの自然数から2つの合計値が出てきます。その合計値が一致するか、差が11の倍数のとき、もとの数も11の倍数なのです。

たとえば「121」という数がありますね。奇数個目は 1 + 1 で2、偶数個目は 2 なので一致していますが、これは11の倍数です。また 9152 は 9 + 5 = 14、 1 + 2 = 3 で差が11となりますから11の倍数です。たとえば 123455233 も11の倍数ですが、 1 + 3 + 5 + 2 + 3 = 14、 2 + 4 + 5 + 3 = 14 で一致しています。

さて本当でしょうか。本当なんですが、ちょっと不安になったので、ランダムな例からチェックしてみましょう。

import Test.QuickCheck newtype Rank = R Integer deriving Show instance Arbitrary Rank where arbitrary = fmap (R . (`mod` 10)) arbitrary f :: [Rank] -> Integer f l = foldl (+) 0 $ zipWith (\(R x) n -> x * 10 ^ (n-1)) l [1..] g :: [Rank] -> (Integer, Integer) g = odd (0, 0) where odd (x, y) (R v:vs) = even (x+v, y) vs odd t [] = t even (x, y) (R v:vs) = odd (x, y+v) vs even t [] = t c :: [Rank] -> Bool c l = (f l `mod` 11 == 0) == ((abs $ uncurry (-) $ g l) `mod` 11 == 0)

*Main> quickCheck c
OK, passed 100 tests.

チェックされました。

という話なんですがここまでに紆余曲折を経ております。何度か失敗してドキっとした。まず最初は単純に f とかを [Int] -> Int としていたのですが失敗しまして、なぜかというと各ケタに22とか-7とか来てますがこれはアウトです。しかたないのでケタに対応して 0 - 9 の範囲内の数値を生成する Rank 型を宣言するハメになりました。 Arbitrary は幸いにして fmap だったので作るのは簡単でしたが……。で、そこを直してみたらまたアウト。 f の返り値が Int になってて、ケタが大きいとオーバフローしちゃいまして負事例が発生してしまいました。なので Integer に直しました。

そういう紆余曲折のすえにテストには成功したわけですが、もちろんこれはどうも正しそうだという確認ができたというだけであり正しさが証明されたわけではありません。こんなこと書いてるヒマがあったら真面目に「なぜそうなるのか」を考えなさいってこった。

なぜそうなるかも本当はそんなに難しくありませんが……。