sLisp
今度書く記事のためにelispでLISPインタープリタ「sLisp」を書きました。
http://github.com/sodeyama/slisp/blob/master/slisp.el
lisp言語で書いてはいますが、読み込んだ文字列をそのままread関数でS式をパースするような事はせず、
その他の言語で行うのと同じ処理を行っています。
具体的に言うと
- トークン切り出し
- パース
- 評価
をしています。
あと、以下の特徴のようにelispっぽいです。
sLispの特徴
- 変則動的スコープ
- 末尾最適化無し
- 遅延評価無し
sLisp対応primitive
- 四則演算
- 論理演算(or, and, not)
- 不等号(=, <, >)
- 条件(if, cond)
- setq
- let
- progn
- defun
- lambda
- print (数値、文字列、真偽値の表示)
sLispサンプルコード
(defun fib (n) (if (= n 0) 0 (if (= n 1) 1 (+ (fib (- n 1)) (fib (- n 2)))))) (print (fib 5)) (setq result ((lambda (x y) (fib (+ x y))) 5 3)) (defun hoge (x) (let ((a 10)) (progn (print "aa") (+ (* a result) x)))) (print (hoge 3))
結果
5 aa 213
■
仕事でorg-modeで書いたテキストをhtmlに変換する必要があったんだけど、
結構な量があったんで自動化したいなーと思って調べてたらやっぱあった
lisp/textmodes/org.el (emacs-22.2の場合)
(defun org-export-as-html-batch () "Call `org-export-as-html', may be used in batch processing as emacs --batch --load=$HOME/lib/emacs/org.el --eval \"(setq org-export-headline-levels 2)\" --visit=MyFile --funcall org-export-as-html-batch" (org-export-as-html org-export-headline-levels 'hidden))
使い方 (※1行で)
% emacs --batch --load=/usr/share/emacs/22.2/lisp/textmodes/org.elc --eval \"(setq org-export-headline-levels 2)\" --visit=hoge.org --funcall org-export-as-html-batch
スクリプトに上記を仕込めば色々自動化出来ます。
■
rubikitchさんとこのブログを読んでwindowの切り替えをデフォルトのC-x oからC-tに変更
すごい楽。
http://d.hatena.ne.jp/rubikitch/20100210/emacs
(defun other-window-or-split () (interactive) (when (one-window-p) (split-window-horizontally)) (other-window 1)) (global-set-key (kbd "C-t") 'other-window-or-split)
あと、gtagsのgtags-pop-stackとかぶるからgtagsの方をC-zに変更
(setq gtags-mode-hook '(lambda () (local-set-key "\M-t" 'gtags-find-tag) (local-set-key "\M-r" 'gtags-find-rtag) (local-set-key "\M-s" 'gtags-find-symbol) (local-set-key "\C-z" 'gtags-pop-stack) )) (setq gtags-select-mode-hook '(lambda () (local-set-key "\C-z" 'gtags-pop-stack) ))
■
ちょっとインタフェースを変えてベータ変換数を入力しなくてもいいようにした。
ついでにgithubにリポジトリ作って突っ込んでおく。
あと、elispでemacsの簡単なメジャーモードを作成
lambda.lmとか適当なファイルでラムダ式書いておいてbeta-modeにしてからC-cbとかC-cnでラムダ計算出来ます
http://github.com/sodeyama/lambda-calculation
しかし、githubでのリポジトリ作成簡単&親切誘導すぎわろた。
sourceforgeの30倍くらい楽。
;; beta-mode (defvar betabin "/home/sode/git/beta-calculation/beta") (defun beta-mode () (interactive) (setq major-mode 'beta-mode mode-name "beta mode") (setq beta-local-map (make-keymap)) (define-key beta-local-map "\C-cb" 'beta-reduction) (define-key beta-local-map "\C-cn" 'beta-reduction-show-native-tree) (use-local-map beta-local-map)) (defun beta-reduction () (interactive) (beta-reduction-inner "false")) (defun beta-reduction-show-native-tree () (interactive) (beta-reduction-inner "true")) (defun beta-reduction-inner (is_tree) (save-excursion (let ((in_str (buffer-string))) (start-process "beta-process" "*beta-buffer*" betabin in_str is_tree) (let ((buffer (get-buffer "*beta-buffer*"))) (switch-to-buffer-other-window buffer) (goto-char (point-max))))))
■
ラムダ計算論の本読んでたので勢い余って関数型言語ocamlでラムダ計算機を書きました。
これでチャーチ数定義して計算すれば、ノイマン型の命令型計算機で計算している人を見かけた時に
「ぷっダサwww」と言えます。
一応このラムダ計算機の使い方
- ラムダ式の記法は (\x y. x y) のようにλを\と書く
- ベータ変換は最左変換戦略
(ちょっと最左最内変換戦略で書いてたら正規化されなくて悩んでたけど、ラムダ式がβ-nfを持つのときに最左変換ではβ-nfに変換される事が定理で保証されているけど、最左最内では保証されていなかったので当たり前だった)
それ以上β変換されなくなったらそれが正規形です。
非正規型の場合、引数の数値を上げても永遠に計算が終わりません
本計算機での計算例
例.1 succ
(\n f x. f (n f x)) (\f x. f (f (f x)))) -> (\f x. f (f (f (f x))))
例.2 plus
(\m n f x. m f (n f x)) (\f x. f(f x)) (\f x. f x) -> (\f x. f (f (f x)))
例.3 pred
(\n f x. n (\g h. h(g f))(\u. x)(\u. u)) (\f x. f( f (f x)))) -> (\f x. (f (f x)))
※余計な括弧があるけどλ式としては無い場合と等価
例.4 mult
(\m n f. m (n f)) (\f x. f (f x)) (\f x. f (f (f x))) -> (\f . (\x . f (f (f (f (f (f x )))))))
※(\x y. M N)は (\x. (\y. (M N))の略記なので上記は (\f x. f (f (f (f (f (f x))))))と等価
ソース
type char_type = LPAREN | RPAREN | LAMBDA | DOT | OTHER type lambda_v = string list type tree = App of lambda_v | Lambda of lambda_v * tree list let channel = open_in "lambada.lm" let token_buf = Buffer.create 64 (* utilities *) let get_l (a, b) = a let get_r (a, b) = b let rec each f e = fun x -> match x with [] -> e | x::rest -> ( f x; each f e rest ) let rec contain list n = match list with x::rest -> if x = n then true else contain rest n | [] -> false let empty lambda = match lambda with App([]) -> true | Lambda([], []) -> true | _ -> false let default_indent = " " let rec show_list_native list = match list with [] -> () | x::rest -> print_string (x ^ " "); show_list_native (rest) let rec show_lm_native lm indent = match lm with App(l) -> print_string (indent ^ "App:"); show_list_native l; print_string "\n" | Lambda(l, list) -> print_string (indent ^ "Lambda \n"); print_string (indent ^ " Variables:"); show_list_native l; print_string "\n"; each (fun x -> show_lm_native x (indent ^ default_indent)) () list let rec show_list list = match list with [] -> () | "paren"::rest -> show_list rest | x::rest -> print_string (x ^ " "); show_list (rest) let rec show_lm lm indent = match lm with App(l) -> show_list l; | Lambda(l, list) -> match l with [] -> each (fun x -> show_lm x (indent ^ default_indent)) () list | ["paren"] -> ( print_string "("; each (fun x -> show_lm x (indent ^ default_indent)) () list; print_string ")" ) | _ -> ( print_string "(\\"; show_list l; print_string ". "; each (fun x -> show_lm x (indent ^ default_indent)) () list; print_string ")" ) let get_v_lm lm = match lm with Lambda(v, l) -> v | App(v) -> [""] let get_children_lm lm = match lm with Lambda(v, l) -> l | App(v) -> [] let add_lm_list_pre lm new_lm = if not(empty new_lm) then match lm with Lambda([], []) -> new_lm | Lambda(l, r) -> Lambda(l, [new_lm]@r) | _ -> lm else lm let add_variable_list_pre x value = match x with Lambda(l, r) -> Lambda(value::l, r) | _ -> x let add_lm_list lm new_lm = if not(empty new_lm) then match lm with Lambda([], []) -> new_lm | Lambda(l, r) -> Lambda(l, r@[new_lm]) | _ -> lm else lm let add_variable_list x value = match x with Lambda(l, r) -> Lambda(l@[value], r) | _ -> x let rec reduce_paren lm = let rec reduce_paren_list lmlist = match lmlist with [] -> lmlist | lm1::lmlist1 -> (reduce_paren lm1)::(reduce_paren_list lmlist1) in match lm with App(v) -> lm | Lambda(["paren"], lmlist') -> ( match lmlist' with [Lambda(["paren"], lmlist'')] -> Lambda(["paren"], (reduce_paren_list lmlist'')) | [Lambda(vlist, lmlist''')] -> Lambda(vlist, (reduce_paren_list lmlist''')) | _ -> Lambda(["paren"], (reduce_paren_list lmlist')) ) | Lambda(vlist, lmlist') -> Lambda(vlist, (reduce_paren_list lmlist')) (* get token from lambda string *) let check_type str = match str with "(" -> LPAREN | ")" -> RPAREN | "\\" -> LAMBDA | "." -> DOT | _ -> OTHER let get_tokens ch = let add_token token_buf token tokens = if Buffer.length token_buf != 0 then ( Buffer.clear token_buf; token::tokens ) else ( tokens ) in let rec get_char in_token tokens = try let c = input_char ch in match check_type (String.make 1 c) with LPAREN|RPAREN|LAMBDA|DOT -> let token = Buffer.contents token_buf in get_char false ((String.make 1 c)::(add_token token_buf token tokens)) | OTHER -> match c with '\r' | '\n' | '\t' | ' ' -> let token = Buffer.contents token_buf in get_char false (add_token token_buf token tokens) | _ -> if in_token then ( Buffer.add_char token_buf c; get_char false ((Buffer.contents token_buf)::tokens) ) else ( Buffer.add_char token_buf c; get_char true tokens ) with End_of_file -> tokens in get_char false [] (* parse. create Lambda tree *) let rec parse tokens lm cur_lm is_lambda = match tokens with [] -> ( match cur_lm with Lambda([], []) -> (lm, []) | App(a) -> ((add_lm_list lm cur_lm), []) | _ -> (lm, []) ) | token::rest -> match check_type token with LPAREN -> let (lm', next) = parse rest (Lambda([], [])) (Lambda(["paren"], [])) false in parse next (add_lm_list (add_lm_list lm cur_lm) lm') (Lambda([], [])) false | LAMBDA -> parse rest lm cur_lm true | DOT -> parse rest lm cur_lm false | RPAREN -> ((add_lm_list lm cur_lm), rest) | OTHER -> if is_lambda then parse rest lm (add_variable_list cur_lm token) is_lambda else parse rest lm (add_lm_list cur_lm (App([token]))) is_lambda (* Alpha Conversion *) let rec get_replaced_v v depth = if depth = 0 then v else get_replaced_v (v ^ "0") (depth - 1) let rec convert_vlist list x replace = match list with [] -> [] | y::rest -> if x == y then replace::rest else y::(convert_vlist rest x replace) let rec alpha_convert x lmlist depth do_replace = let replace_lm src replace lm depth = match lm with App(vlist) -> if contain vlist src then (App(convert_vlist vlist src replace), true) else (lm, false) | Lambda(vlist, lmlist') -> let (lmlist'', do_replace'') = (alpha_convert x lmlist' (depth + 1) do_replace) in if do_replace'' then (Lambda((convert_vlist vlist x (get_replaced_v src depth)), lmlist''), true) else (Lambda(vlist, lmlist''), false) in match lmlist with [] -> ([], do_replace) | lm::lmlist_rest -> let replace = get_replaced_v x depth in let (lm', do_replace') = replace_lm x replace lm depth in if do_replace then (lm'::(get_l(alpha_convert x lmlist_rest depth do_replace)), true) else let (lmlist', do_replace'') = (alpha_convert x lmlist_rest depth do_replace) in (lm::lmlist', do_replace'') let rec alpha = fun lm -> match lm with App(v) -> lm | Lambda(vlist, lmlist) -> match vlist with ["paren"]|[] -> print_endline "alpha1"; each (fun x -> alpha x) (Lambda([],[])) lmlist | x::vlist_rest -> print_endline "alpha2"; let (lmlist', do_replace) = alpha_convert x lmlist 0 false in if do_replace then ( print_endline "alpha2 suc"; Lambda(vlist, lmlist') ) else ( add_variable_list_pre (alpha (Lambda(vlist_rest, lmlist))) x ) (* Beta Reduction *) let rec beta_reduction = fun lm -> let rec trans_lms lmlist x lm do_trans = (* lmlist u App:f do_trans *) match lmlist with [] -> ([], do_trans) | lm'::rest -> match lm' with App(vlist) -> if (contain vlist x) then ( let (lmlist1, do_trans1) = (trans_lms rest x lm true) in ((lm::lmlist1), true) ) else ( let (lmlist1, do_trans1) = (trans_lms rest x lm do_trans) in (lm'::lmlist1, true) ) | Lambda(l, r) -> if (contain l x) then (* for alpha conversion *) ( (lmlist, do_trans) ) else let (lmlist1, do_trans1) = (trans_lms r x lm do_trans) in let (lmlist2, do_trans2) = (trans_lms rest x lm do_trans) in (Lambda(l, lmlist1)::lmlist2, (do_trans1 || do_trans2)) in let rec trans_lm lm1 lm2 do_trans = let rec trans_lmlist lmlist lm2 do_trans = match lmlist with [] -> (lmlist, false) | lm::rest -> let (lm', do_trans') = trans_lm lm lm2 do_trans in let (lmlist', do_trans'') = trans_lmlist rest lm2 do_trans in (lm'::lmlist', (do_trans'||do_trans'')) in match lm1 with App(vlist) -> (lm1, false) | Lambda(vlist, lmlist) -> match vlist with [] -> (lm1, false) | ["paren"] -> let (lm'', do_trans'') = beta_reduction lm1 in (*trans_lmlist lmlist lm2 do_trans in*) if do_trans'' then (Lambda(["paren"], lm''::lm2::[]), true) else let (lmlist', do_trans''') = trans_lmlist lmlist lm2 do_trans in if do_trans''' then (Lambda(["paren"], lmlist'), true) else (lm1, false) | [v1] -> let (lmlist', do_trans') = trans_lms lmlist v1 lm2 false in if do_trans' then (Lambda(["paren"], lmlist'), true) else (lm1, false) | "paren"::v2::rest -> let (lmlist', do_trans') = trans_lms lmlist v2 lm2 false in if do_trans' then (Lambda("paren"::rest, lmlist'), true) else (lm1, false) | v1::rest -> let (lmlist', do_trans') = trans_lms lmlist v1 lm2 false in if do_trans' then (Lambda(rest, lmlist'), true) else (lm1, false) in match lm with App(vlist) -> (lm, false) | Lambda([], []) -> (lm, false) | Lambda(vlist, lmlist) -> match lmlist with [] -> (lm, false) | [lm'] -> let (lm', do_trans') = beta_reduction lm' in if do_trans' then (Lambda(vlist, [lm']), true) else (lm, false) | lm1::lm2::rest -> let (lm'', do_trans) = trans_lm lm1 lm2 false in let lmlist' = if (get_v_lm lm'') = ["paren"] then ( (* debug_print lm lm1 lm'' lm2 vlist do_trans *) get_children_lm lm'' ) else [lm''] in if do_trans then (Lambda(vlist, lmlist'@rest), true) else let (lm1', do_trans') = beta_reduction lm1 in if do_trans' then (Lambda(vlist, lm1'::lm2::rest), true) else let (lm''', do_trans'') = beta_reduction (Lambda(vlist, lm2::rest)) in if do_trans'' then (Lambda(vlist, lm1::(get_children_lm lm''')), true) else (lm, false) let rec beta_n n lm do_trans = match n with 0 -> (lm, do_trans) | _ -> let (lm', do_trans') = (beta_reduction lm) in if do_trans' then ( beta_n (n - 1) (reduce_paren lm') do_trans' ) else (lm', false) let _ = let count = int_of_string Sys.argv.(1) in let tokens = get_tokens channel in let (lm, _) = parse (List.fold_left (fun x y -> y::x) [] tokens) (Lambda(["paren"],[])) (Lambda([], [])) false in (* show_lm_native (alpha lm) default_indent; *) let (lm', do_trans) = beta_n count lm false in show_lm (reduce_paren lm') default_indent; print_endline ""
ocaml初なのでmap使えよwとか突っ込みどころ満載です。
そういえばこないだ会社行く途中の電車で「計算論」読んでたら乗り換え駅で降り忘れて2駅ほど先に進んでしまった。
その駅が会社から近かったんで、走れば間に合うだろうと思って全力疾走してたら逆走している事に気づいて結局タクった。
マジ計算論危険 有給無くなって遅刻できないやつにはお勧め出来ない。
■
計算論のP.66のβ変換における等号表現である
を定義する時に現れる表現
の定義なんだけど、直感的に
と思ってたけど
なんだね
不動点演算子Yの定義で、Mの不動点演算子Yに対して
YM -> M'(M' ≡ M''M'', M'' ≡ λx. M(xx) ) からいきなり YM = M'を導いてたから悩んだ
要するに
M -> P1 -> P2 -> ... -> P_s <- .... <- N を満たすλ式 P1,P2,...が存在するならば M = Nと。
※ ->をβ変換、=をβ等号の意味で書いた。また以下では ->>をβ変換列の意味として書く
[問2.1.5] Y' ≡ XX, X ≡ λxy. y(xxy)の時 Y'M ->> M(Y'M)となることを証明せよ [証明] 定義より Y'M ≡ XXM -> (λxy. y(xxy))XM -> (λy. y(XXy))M -> M(XXM) ≡ M(Y'M) よって Y'M ->> M(Y'M) □