最近買った本
- 作者:中川 裕
- 発売日: 2013/11/27
- メディア: 単行本(ソフトカバー)
[普及版]ジェネラティブ・アート―Processingによる実践ガイド
- 作者:マット・ピアソン,Matt Pearson
- 発売日: 2014/11/21
- メディア: 単行本(ソフトカバー)
甲賀流忍者ぽんぽこ&オシャレになりたい!ピーナッツくん オフィシャルファンブック ぽこピーの本
- 作者:甲賀流忍者ぽんぽこ・オシャレになりたい! ピーナッツくん
- 発売日: 2021/01/29
- メディア: Kindle版
レーブの定理
「スマリヤンの決定不能の論理パズル(白揚社 2008年)」という本にレーブの定理がわかりやすく紹介されていたので、それを紹介したいと思います。
レーブの定理
任意の命題について、もし4型の推論者がとを信じるならば、を信じる。
ここで、というのは、「命題を信じている」という意味で、4型の推論者とは以下の推論規則に従う人です。
証明する前に補題を2つほど示します。
補題1
証明 ∵(A2)と同値
∵(1),(A1b)より
∵(2)のをに置き換え
∵ のを,を,
をに置き換え
∵(1),(4),(A1b)より
∵(5),(A1b)より
∵(3),(6)より
∵(A3)より
∴ ∵(7),(8)より
∵(4)より
∵ のを,を,
をに置き換え
∵(2),(3),(A1b)より
∴ ∵(1),(4),(A1b)より
ではレーブの定理を証明します。
レーブの定理
証明 ∵補題2より
∵ のを,を,
をに置き換え
∵(1),(2),(A1b)より
∵(A1b)より
∵(A3)より
∵(A1b)より
∴ ∵(3),(4),(5),(6)より
これで、レーブの定理が示せました。
実は、本はまだ半分までしか読んでないので、これがレーブの定理の全てなのかは分かりません。(まだ読んでないとこにも出てきていたので)
実際にはもっと詳しく書いてあるので、興味があったらぜひ読んでみてください。
コラッツ予想 Part3
の母関数
を考えます。
以下の議論は、私の無知により多少不正確です。(つまり、母関数を扱ったことはありません)
と分けると、
また、
になります。Q1を無視すれば、
単純に、とあ思いましたが、
になり、私には力不足のようです。
オセロ必勝法 Part4
(defun Othello () (setq table nil) (setq sq 8) (setq r nil) (defun initable () (defun initableat () (cond ((not table) (setq table '((0 0)))) ((= (caar table) (1- sq)) (setq table (push `(0 ,(1+ (cadr (car table)))) table))) (t (setq table (push `(,(1+ (caar table)) ,(cadr (car table))) table))))) (defun nest (f n) (if (zerop n) nil (progn (funcall f) (nest f (1- n))))) (nest 'initableat (* sq sq)) (setq table (reverse table)) (setq table (mapcar (lambda (x) (list x 0)) table))) (defun setdisk (x y disk) (setq table (mapcar (lambda (z) (cond ((and (eq (caar z) x) (eq (cadr (car z)) y)) (list (list x y) disk)) (t z))) table))) (defun subsetdisk (x y disk) (setq subtable (mapcar (lambda (z) (cond ((and (eq (caar z) x) (eq (cadr (car z)) y)) (list (list x y) disk)) (t z))) subtable))) (defun begintable () (setq table nil) (initable) (setdisk 1 1 t) (setdisk 2 1 nil) (setdisk 1 2 nil) (setdisk 2 2 t) (display)) (defun neighbor (x) (cond ((= x 0) '(-1 -1)) ((= x 1) '(0 -1)) ((= x 2) '(1 -1)) ((= x 3) '(-1 0)) ((= x 4) '(1 0)) ((= x 5) '(-1 1)) ((= x 6) '(0 1)) ((= x 7) '(1 1)))) (defun getdisk (x y) (cadr (elt table (+ (* sq y) x)))) (defun turnover (x y color) (let ((dir nil) (flag nil) (i 0) (subtable table) (nei 8)) ;(if (not (checkturnover x y color)) '(cant put here) (progn (setdisk x y color) (setq subtable table) (defun turnoverat (x y color dir flag) (let ((neix (+ x (car (neighbor dir)))) (neiy (+ y (cadr (neighbor dir))))) (if (or (> 0 (+ (* sq neiy) neix)) (<= (* sq sq) (+ (* sq neiy) neix)) (eq (getdisk neix neiy) 0)) (setq subtable table) (if (not flag) (if (eq (getdisk neix neiy) (not color)) (progn (subsetdisk neix neiy color) (turnoverat neix neiy color dir t))) (cond ((eq (getdisk neix neiy) 0) (setq subtable table)) ((eq (getdisk neix neiy) (not color)) (progn (subsetdisk neix neiy color) (turnoverat neix neiy color dir t))) ((eq (getdisk neix neiy) color) (setq table subtable))))))) (while (< i nei) (turnoverat x y color i flag) (setq i (1+ i)))) ;) ) ;(display) table) (defun checkturnover (x y color) (let ((dir nil) (flag nil) (i 0) (subtable table) (nei 8) (checkflag nil)) (if (eq (getdisk x y) 0) (progn (defun checkturnoverat (x y color dir flag) (let ((neix (+ x (car (neighbor dir)))) (neiy (+ y (cadr (neighbor dir))))) (if (or (> 0 (+ (* sq neiy) neix)) (<= (* sq sq) (+ (* sq neiy) neix)) (eq (getdisk neix neiy) 0)) nil (if (not flag) (if (eq (getdisk neix neiy) (not color)) (checkturnoverat neix neiy color dir t)) (cond ((eq (getdisk neix neiy) 0)) ((eq (getdisk neix neiy) (not color)) (checkturnoverat neix neiy color dir t)) ((eq (getdisk neix neiy) color) (setq checkflag t))))))) (while (< i nei) (checkturnoverat x y color i flag) (setq i (1+ i))))) checkflag)) (defun displaycolor () (mapcar (lambda (x) (cond ((eq (cadr x) 0) 0) ((eq (cadr x) nil) '●) ((eq (cadr x) t) '○) (t '.))) table)) (defun cutoff (table) (let ((i nil) (j nil)) (defun cutoffat (table i j) (cond ((eq i nil) (progn (setq i 0) (setq j 0) (setq p nil) (setq q nil) (cutoffat table i j))) ((< i sq) (progn (push (car table) p) (cutoffat (cdr table) (1+ i) j))) ((< j sq) (progn (push (reverse p) q) (setq i 0) (setq p nil) (cutoffat table i (1+ j)))) (t (reverse q)))) (cutoffat table i j))) (defun displaynewline (table) (if (eq table nil) nil (progn (setq r (concat r (format "%s" (car table)) (string ?\n))) (displaynewline (cdr table)))) r) (defun display () (setq r (string ?\n)) (displaynewline (cutoff (displaycolor)))) (defun count () (let ((sumb 0) (sumw 0)) (defun countat (table) (cond ((eq table nil) nil) ((eq (cadr (car table)) nil) (progn (setq sumb (1+ sumb)) (countat (cdr table)))) ((eq (cadr (car table)) t) (progn (setq sumw (1+ sumw)) (countat (cdr table)))) (t (countat (cdr table))))) (countat table) (cond ((= sumb sumw) 'draw) ((> sumb sumw) nil) ((< sumb sumw) t)))) (defun end (table) (catch 'loop (let ((j 0)) (while (< j sq) (let ((i 0)) (while (< i sq) (if (or (checkturnover i j nil) (checkturnover i j t)) (throw 'loop nil)) (setq i (1+ i)))) (setq j (1+ j)))) t)) (defun strategy (table turn) (if (end table) (count) (catch 'loop (let ((j 0) (i 0) (win (not turn)) (flag nil)) (while (< j sq) (while (< i sq) (if (checkturnover i j turn) (let ((x (strategy (turnover i j turn) (not turn)))) (cond ((eq turn x) (throw 'loop turn)) ((eq 'draw x) (setq win 'draw))) (setq flag t))) (setq i (1+ i))) (setq i 0) (setq j (1+ j))) (if (not flag) (strategy table (not turn)) win))))))
というわけで、プログラムは出来たのですが、計算量が多すぎます。
多く見積もっても、10^80分かかります。
どうしたものか・・・