Prime? is in NP.

Prattのアレ. 証拠を判定するアルゴリズム on xyzzy lisp.
(Prime? w11)->t
(x1 x2 x3)というリストがあって (xi \in \{t,nil\}), (and x1 x2 x3)を計算したかったのに外した. (apply #'and list)は駄目だった. マクロをちゃんと理解しないと駄目だなぁ.

追記: 2000年にインドの3人組が素数判定がPに入ることを示した. 論文のタイトルはその名もPRIME is in P. 名前からして素晴らしい.
で, 歴史的に見ると, 1970年代にNPという概念が考え出されたと. 合成数判定がNPに入るので (素因数を持ってこれば, それが証拠), 素数判定はNPcoNPに入ることは簡単に分かっていた.
ただ, NPに入るかどうかは自明では無い. で, 1975年にPrattさんが発表した論文があって, それは素数判定はNPに入るという話をしていた. そこに挙げられている方針は面白いので, 読むと良いと思う. 下のプログラムは3章に挙げられている, Proof Treeを解析するもの. 各ノードは(素数p, 原始根)という組. (p,a)というノードの子が(p1,a1),...,(pk,ak)のとき, a^{(p-1)/p_i} \not\equiv 1 \pmod{p}かつ p-1=p_1 p_2 ... p_k.

(setq w2 '((2 1)))
(setq w3 '((3 2) ((2 1))))
(setq w5 '((5 2) ((2 1)) ((2 1))))
(setq w11 '((11 2) ((5 2) ((2 1)) ((2 1))) ((2 1))))

(defun Prime? (list1)
  (cond ((check4? list1) t)
        ((and (check2? list1) (check5? list1) (check3? list1))
         (equal (length (cdr list1)) (count 't (mapcar #'Prime? (cdr list1)))))
        (t nil)))

;((p a) w1 w2 ... wk)を入力としてa^{p-1} (mod p)=1なら真
(defun check2? (list1)
  (equal 1 (expmodt (cadar list1) (- (caar list1) 1) (caar list1))))

;list1が((2 1))と等しいなら真
(defun check4? (list1) ;
  (equal list1 '((2 1))))

;((p a) w1=((p1 a1)...) w2=((p2 a2)...)...)を入力として,
;p-1=p1p2...pkなら真
(defun check5? (list1)
  (equal (- (caar list1) 1) (apply #'* (mapcar #'caar (cdr list1)))))

;((p a) w1=((p1 a1)...) w2=((p2 a2)...)...)を入力として,
;各iについて, a^{(p-1)/pi} (mod p) \= 1ならば真
;(exp-list '(p a) '(p1 p2 p3 ... pk))
;-> (a^{p-1/p1}mod p, a^{p-1/p2}mod p, ..., a^{p-1/pk}mod p)を返す.
;(exp-list0? '(p a) '(p1 p2 ... pk))
;-> \prod ((a^{p-1/pi} mod p)-1)が0で無いなら真.
(defun check3? (list1)
  (exp-list0? (car list1) (mapcar #'caar (cdr list1)))
  (defun exp-list (list1 list2)
    (mapcar #'(lambda (x) (expmodt (cadr list1) (/ (1- (car list1)) x) (car list1))) list2))
  (defun exp-list0? (list1 list2)
    (apply #'* (mapcar #'1- (exp-list list1 list2)))))

;繰り返し2乗法. a^b mod cを返す.
(defun expmodt (a b c) 
  (cond ((equal b 0) 1)
        ((equal b 1) (mod a c))
        ((oddp b) (mod (* a (expmodt a (- b 1) c)) c))
        ((evenp b) (expmodt (* a a) (/ b 2) c))))