「数学ガール ゲーデルの不完全性定理」を少しずつ読んでいる。
数学ガール/ゲーデルの不完全性定理 (数学ガールシリーズ 3)
- 作者: 結城浩
- 出版社/メーカー: SBクリエイティブ
- 発売日: 2009/10/24
- メディア: 単行本
- 購入: 37人 クリック: 930回
- この商品を含むブログ (149件) を見る
前2作は、大半がなじみのある話で十津川警部シリーズ並みのスピードと気楽さで読めたが、今回は違って、しばしば立ち止まりながら進んでいる。論理は苦手。考えれば分かるんだけれど、身になっていないというか。
大昔にブルーバックスで不完全性定理について読んでいちおう納得したつもりになっていた。しかし内容を忘れてしまったのでもう一度読みたかったが、どこかに行ってしまった。この本で復習しようということだ。
その中の最初のほうにこんな問題があった（改変しているが趣旨は同じ）。
3×3のマスに0〜2の数字が入っている。縦でも横でもどの列も0〜2が一度ずつ使われている。その中の一部のマスの数字が分かっていて次のようになっている（'_'は見えていないマス）。
_1_
_0_
1__このとき、見えていないマスの数字も求めよ。
この問題自体は簡単だが、ここで疑問が湧いた。見えているマスは常に3つなのだろうか。また、4×4の場合はどうなのか。
見えているマスは最小限でなければならない。すなわち、ここから見えているマスを減らして一意に解が得られてはならない。
数学的にどうしていいかわからないのでプログラミングで解く。
見えているマスを1個から次第に増やしていく。そのときに解が一意になったらその枝はそこでストップ。しかし、見えているマスを減らせる場合は妥当な問題とみなさない。ここで、見えているマスを減らして解が一意になる場合、マスを減らせると呼ぶことにする。
見えているマスの個数が同じの場合、一つだけ出力する。
3×3の場合、
0__
_1_
___01_
1__
___
実は見えているマスは2つでもよかったのだ。気づいていなかった。
4×4の場合、
__0_
_3__
____
0_1_01__
_3_0
__3_
________
3_1_
__21
_2_02_1_
0__1
____
1_20
妥当な問題は4〜7つ見えているマスがある。これで正しいだろうか。
下のコードは今一つなので後で書き直すかも。
from itertools import permutations, product, ifilterfalse, imapdef all(f, a):
for e in ifilterfalse(f, a):
return False
return Truedef is_valid_col(s, k):
return sum(map(lambda a: 1 << a[k], s)) == Mdef is_valid(s):
return all(lambda k: is_valid_col(s, k), range(N))def mul(s, d):
return reduce(lambda x, k: x * (N + 1) + (s[k] + 1) * ((d >> k) & 1),
range(L), 0)def add_dic(dic, key, value):
if key in dic:
dic[key].append(value)
else:
dic[key] = [ value ]def gen_sols(d, solutions):
dic = { }
for sol, prob in imap(lambda s: (s, mul(s, d)), solutions):
add_dic(dic, prob, sol)
for sols in dic.itervalues():
yield solsdef gen_digits(n, base = 10):
for k in range(L):
yield n % base
n /= basedef to_display(n):
return reduce(lambda x, y: (x << 1) + y,
map(lambda d: d > 0, gen_digits(n, N + 1)), 0)def make_sym_pos():
def sym_position(k):
x = k % N
y = k / N
if x >= (N + 1) / 2:
x = N - 1 - x
if y >= (N + 1) / 2:
y = N - 1 - y
return max(x, y) + min(x, y) * N
return map(sym_position, range(L))def head_display(d):
for k in range(L):
if d == 0:
return -1
if d & 1:
return k
d >>= 1def gen_valid_pos(k0, hd0):
if k0 == 0:
for k in filter(lambda k: sym_pos[k] == k, range(k0, L)):
yield k
else:
for k in filter(lambda k: sym_pos[k] >= hd0, range(k0, L)):
yield kdef gen_problem(d0, sols0, k0 = 0, l = 0, max_used_digit = -1):
hd = head_display(d0)
for k in gen_valid_pos(k0, hd):
d = d0 | 1 << k
for sols in gen_sols(d, sols0):
sol = sols[0]
if sol[k] > max_used_digit + 1:
continue
if len(sols) == 1:
yield mul(sol, d)
elif len(sols) > 1:
md = max(sol[k], max_used_digit)
for n in gen_problem(d, sols, k + 1, l + 1, md):
yield ndef make_problems():
problems = [ [] for n in range(L) ]
for problem in gen_problem(0, solutions):
problems[display_num(problem)].append(problem)
return problemsdef to_s(n, k = 0):
r = n % (N + 1)
s = str(r - 1) if r else "_"
if k == N * N - 1:
return s
elif k % N == N - 1:
return to_s(n / (N + 1), k + 1) + "\n" + s
else:
return to_s(n / (N + 1), k + 1) + sdef display_num(p):
return sum(map(lambda d: d > 0, gen_digits(p, N + 1)))def remove(problem, k):
a = list(gen_digits(problem, N + 1))
a.reverse()
a[k] = 0
return reduce(lambda x, y: x * (N + 1) + y, a, 0)def has_unique_solution(problem):
disp = to_display(problem)
counter = 0
for p in imap(lambda s: mul(s, disp), solutions):
if p == problem:
counter += 1
if counter == 2:
return False
return Truedef is_able_to_reduce(problem):
disp = to_display(problem)
for k in filter(lambda k: (disp >> k) & 1, range(L)):
p = remove(problem, k)
if has_unique_solution(remove(problem, k)):
return True
return Falsedef head_valid_problem(k):
print k, len(problems[k])
for p in ifilterfalse(is_able_to_reduce, problems[k]):
print to_s(p)
breakN = 4
M = 2 ** N - 1
L = N * N
solutions = map(lambda s: reduce(lambda x, y: x + y, s),
filter(is_valid, product(permutations(range(N)), repeat = N)))sym_pos = make_sym_pos()
problems = make_problems()
for k in range(L):
head_valid_problem(k)
