はじめに
自作のEasy-ISLispにユニコードの機能を拡張しています。これのテストにユニコードで記述された論理式の文字列をゲーデル数化するもの、そしてその数を論理式を表す文字列に復号するコードを書きました。
ゲーデル数
数学者ゲーデルはその不完全性定理の証明にあたり論理式を自然数に変換する手法を用いました。ゲーデル数と呼ばれています。数学が自己言及するための仕組みです。素因数分解の一意性を利用しています。
論理式に用いられる記号に対応する自然数を定義しておきます。そして素数のべき乗の積を計算します。
2^3 * 3^4 * 5^2 のようにです。
復号の計算ではmathライブラリの素因数分解を利用しています。
動作例
Easy-ISLisp Ver2.40
> (load "tests/godel.lsp")
T
> dt
"∃xy〜(x)∧(y)"
> (encode dt)
395017145154031183566599905857292182568201440502240006394147044479902343750000
> (decode 395017145154031183566599905857292182568201440502240006394147044479902343750000)
"∃xy〜(x)∧(y)"
ソースコード
#|
godel number (test unicode)
|#
(import "math")
(import "cxr")
(defglobal dt "∃xy〜(x)∧(y)")
(defglobal code-list
'((1 #\〜)
(2 #\∧)
(3 #\))
(4 #\∃)
(5 #\=)
(6 #\0)
(7 #\s)
(8 #\()
(9 #\))
(10 #\")
(11 #\x)
(13 #\y)))
(defun rev-assoc (key list)
(if (equal (cadar list) key)
(caar list)
(rev-assoc key (cdr list))))
(defun char->integer (ls)
(mapcar (lambda (x) (rev-assoc x code-list)) ls))
(defun string->integer (str)
(char->integer (convert str <list>)))
(defun integer->godel (ls)
(integer->godel1 ls 1))
(defun integer->godel1 (ls n)
(if (null ls)
1
(* (expt (prime n) (car ls)) (integer->godel1 (cdr ls) (+ n 1)))))
(defun encode (str)
(integer->godel (string->integer str)))
(defun decode (n)
(decode1 (factorize n)))
(defun decode1 (ls)
(if (null ls)
""
(string-append (convert (cadr (assoc (cadar ls) code-list)) <string>)
(decode1 (cdr ls)))))
ISLisp規格との関連
ISLisp規格ではユニコードについて規定されていません。Easy-ISLisp用に独自に拡張しました。文字列とキャラクタにのみユニコードが使えます。
> dt
"∃xy〜(x)∧(y)"
> (elt dt 0)
#\∃
> (aref dt 7)
#\∧
> (convert dt <list>)
(#\∃ #\x #\y #\〜 #\( #\x #\) #\∧ #\( #\y #\))
> (length "こんにちは")
5
>
現在、ISLispの規格を満たしつつユニコードの拡張ができているか検証テストコードで確認中です。確認作業が終わりましたら正式にver2.40としてリリース予定です。