- 追加された行はこの色です。
- 削除された行はこの色です。
#contents
*Proofs and Types [#z5683f1d]
Jean-Yves Girard, Yves Lafont and Paul Taylor
- http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html
定理証明器ネタのページがそろそろ必要か。
*reddit.comから [#d5676edd]
こんなのがありました。
http://as305.dyndns.org/wiki/index.php?Coq%2Ftactics
* (OCaml) char list から stringへの変換（よしひろ） [#da6c448a]
さっきまで寝てたら夢の中で急に思いついた関数。コンパイルしてみたらほんとに通った。
let string_of_charlist chars =
let rec aux n = function
| [] -> String.create n
| c :: tl ->
let s = aux (n+1) tl in
s.[n] <- c;
s
in aux 0 chars;;
バグってたら教えてください。
* 定理証明器 Coq でHello, world! (よしひろ)[#pc6c3278]
Coqで "Hello, world!" を標準出力させるのはちょっと難しい。~
なぜなら純粋だから。~
今回は29行ほどのOCamlの力を借りて実装した。~
具体的には次の三つのファイルを作った。~
-coqstring.v
-helloworld.v
-main.ml (29行のOCamlコード)
ちなみにCoqでは、文字は8bitのascii型、文字列はasciiのリストみたいな感じで定義されている。
(*Coqのスタンダードライブラリより*)
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
Inductive string : Set :=
| EmptyString : string
| String : ascii -> string -> string.
まずcoqstring.v~
Coqの文字列に関する便利のものたちを定義した。
(* Coqのコード *)
Require Import Ascii.
Require Import Strings.
Definition aH := Ascii false false false true false false true false.
Definition ae := Ascii true false true false false true true false.
Definition al := Ascii false false true true false true true false.
Definition ao := Ascii true true true true false true true false.
Definition aCMM := Ascii false false true true false true false false.
Definition aSPC := Ascii false false false false false true false false.
Definition aw := Ascii true true true false true true true false.
Definition ar := Ascii false true false false true true true false.
Definition ad := Ascii false false true false false true true false.
Definition aEXCLAM := Ascii true false false false false true false false.
Definition aLF := Ascii false true false true false false false false.
次にhelloworld.v~
このソースがこのプログラムの本質部分。
(* Coqのコード *)
Require Import Ascii.
Require Import Strings.
Require Import coqstring.
Definition msg :=
String aH
(String ae
(String al
(String al
(String ao
(String aCMM
(String aSPC
(String aw
(String ao
(String ar
(String al
(String ad
(String aEXCLAM
(String aLF EmptyString))))))))))))).
Extraction "coqhelloworld.ml" nat_of_ascii msg.
以上のコードをコンパイルした結果、自動生成されるOCamlのコードがこれである。
(* これは上にあるCoqのコードから自動的に生成されたOCamlのコードである。 *)
type bool =
| True
| False
type nat =
| O
| S of nat
(** val plus : nat -> nat -> nat **)
let rec plus n m =
match n with
| O -> m
| S p -> S (plus p m)
(** val mult : nat -> nat -> nat **)
let rec mult n m =
match n with
| O -> O
| S p -> plus m (mult p m)
type ascii =
| Ascii of bool * bool * bool * bool * bool * bool * bool * bool
(** val nat_of_ascii : ascii -> nat **)
let nat_of_ascii = function
| Ascii (a1, a2, a3, a4, a5, a6, a7, a8) ->
plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(match a8 with
| True -> S O
| False -> O))
(match a7 with
| True -> S O
| False -> O)))
(match a6 with
| True -> S O
| False -> O)))
(match a5 with
| True -> S O
| False -> O)))
(match a4 with
| True -> S O
| False -> O)))
(match a3 with
| True -> S O
| False -> O)))
(match a2 with
| True -> S O
| False -> O))) (match a1 with
| True -> S O
| False -> O)
type string =
| EmptyString
| String of ascii * string
(** val aH : ascii **)
let aH =
Ascii (False, False, False, True, False, False, True, False)
(** val ae : ascii **)
let ae =
Ascii (True, False, True, False, False, True, True, False)
(** val al : ascii **)
let al =
Ascii (False, False, True, True, False, True, True, False)
(** val ao : ascii **)
let ao =
Ascii (True, True, True, True, False, True, True, False)
(** val aCMM : ascii **)
let aCMM =
Ascii (False, False, True, True, False, True, False, False)
(** val aSPC : ascii **)
let aSPC =
Ascii (False, False, False, False, False, True, False, False)
(** val aw : ascii **)
let aw =
Ascii (True, True, True, False, True, True, True, False)
(** val ar : ascii **)
let ar =
Ascii (False, True, False, False, True, True, True, False)
(** val ad : ascii **)
let ad =
Ascii (False, False, True, False, False, True, True, False)
(** val aEXCLAM : ascii **)
let aEXCLAM =
Ascii (True, False, False, False, False, True, False, False)
(** val aLF : ascii **)
let aLF =
Ascii (False, True, False, True, False, False, False, False)
(** val msg : string **)
let msg =
String (aH, (String (ae, (String (al, (String (al, (String (ao, (String
(aCMM, (String (aSPC, (String (aw, (String (ao, (String (ar, (String (al,
(String (ad, (String (aEXCLAM, (String (aLF,
EmptyString)))))))))))))))))))))))))))
最後に以上をまとめて結果を出すOCamlのコードmain.ml。~
この部分だけは証明することができない。
(* OCamlのコード *)
module Coq = Coqhelloworld
let rec int_of_nat = function
| Coq.O -> 0
| Coq.S p -> 1 + (int_of_nat p)
let length coqstr =
let rec length_aux n = function
| Coq.EmptyString -> n
| Coq.String (_, tl) -> length_aux (1+n) tl
in
length_aux 0 coqstr
let char_of_ascii a =
char_of_int (int_of_nat (Coq.nat_of_ascii a))
let string_of_coqstring coqstr =
let n = length coqstr in
let s = String.create n in
let rec aux i = function
| Coq.EmptyString -> ()
| Coq.String (hd, tl) ->
s.[i] <- char_of_ascii hd;
aux (i+1) tl
in
aux 0 coqstr;
s;;
print_string (string_of_coqstring Coq.msg);;
実行結果
Hello, world!
やった！できた！
* StateT [#x763ddb2]
これは、permutationを返す関数：
permutation' :: [[Int]] -> Int -> [Int] -> [[Int]]
permutation' result 0 _ = result
permutation' result n cand =
do a <- cand
permutation' (map (a:) result) (n-1) [x|x<-cand,x/=a]
使い方
permutation' [[]] [1,2,3] 2
のように使う。
これをStateTを使ってわざと分かりにくくしてみる：
permutation :: [[Int]] -> Int -> StateT [Int] [] [[Int]]
permutation result 0 = return result
permutation result n =
do cand <- get
a <- lift cand
put [x|x<-cand,x/=a]
permutation (map (a:) result) (n-1)
これは
runStateT (permutation [[]] 2) [1,2,3]
のように使う。
- Thx. 勉強になります。 -- [[げんま]] &new{2007-04-24 (火) 12:45:05};
* Kamen Lisp [#a8f00089]
http://www.cs.stevens.edu/~dlong/software/kamen/index.php
matzにっきより。ブラウザ側で動くってのは他にもあったよね。でもこれはクライアントサイドのプログラムそのもの(Ajaxとか)をLispで書くって話っぽいぞ
- firefoxを拡張して、lispscriptとでもいったものを実行できるようにするんじゃない? firefoxの拡張でそんなことを実現できるのに驚いた。lispscriptで書かれた魅力的なコンテンツがたくさん生まれてみんながこの拡張をデフォルトでインストールするようになる、なんてことは無理だと思う。それなら lisp->javascript コンパイラのほうがいいわけで。しかし、firefoxってすげーな、と思った。 -- [[げんま]] &new{2007-04-21 (土) 04:07:16};
- なるほど。さんくすこ。 -- [[けいご]] &new{2007-04-23 (月) 21:18:05};
- WVkgGwOUlJtpS -- [[axsnsuvfzxo]] &new{2007-07-06 (金) 10:38:22};
- Nice site <a href="http://xrobak.12gbfree.com/fioricet.html">fioricet prescription</a><a href="http://xrobak.12gbfree.com/index.html">wisconsin</a><a href="http://xrobak.12gbfree.com/fioricet.html">buy brand name fioricet</a><a href="http://xrobak.12gbfree.com/fioricet.html">fioricet generic online</a><a href="http://xrobak.12gbfree.com/index.html">lead</a><a href="http://xrobak.12gbfree.com/fire.html">spyware</a> [URL=http://xrobak.12gbfree.com/financial-aid.html]financial aid for woman[/URL][URL=http://xrobak.12gbfree.com/fioricet.html]generic fioricet and sale[/URL] -- [[Nick]] &new{2007-08-16 (木) 10:34:06};
- <a href= http://crazyfrog.vdforum.ru >crazy frog ringtone</a> , [url= http://crazyfrog.vdforum.ru ] crazy frog ringtone [/url] , crazy frog ringtone http://crazyfrog.vdforum.ru . <a href= http://2pac.forum5.com >2pac ringtone</a> , [url= http://2pac.forum5.com ] 2pac ringtone [/url] , 2pac ringtone http://2pac.forum5.com . <a href= http://24ctu.forum5.com >24 ctu ringtone</a> , [url= http://24ctu.forum5.com ] 24 ctu ringtone [/url] , 24 ctu ringtone http://24ctu.forum5.com . <a href= http://maxis.forum5.com >maxis caller ringtone</a> , [url= http://maxis.forum5.com ] maxis caller ringtone [/url] , maxis caller ringtone http://maxis.forum5.com . <a href= http://ctu.forum5.com >ctu ringtone</a> , [url= http://ctu.forum5.com ] ctu ringtone [/url] , ctu ringtone http://ctu.forum5.com . <a href= http://hotlink.forum5.com >hotlink maxis caller ringtone</a> , [url= http://hotlink.forum5.com ] hotlink maxis caller ringtone [/url] , hotlink maxis caller ringtone http://hotlink.forum5.com . <a href= http://complimentary.forum5.com >complimentary right ringtone</a> , [url=http://complimentary.forum5.com]complimentary right ringtone[/url] , complimentary right ringtone http://complimentary.forum5.com . <a href= http://jamster.forum5.com >free jamster ringtone</a> , [url= http://jamster.forum5.com ] free jamster ringtone [/url] , free jamster ringtone http://jamster.forum5.com . <a href= http://gospel.forum5.com >free gospel ringtone</a> , [url= http://gospel.forum5.com ] free gospel ringtone [/url] , free gospel ringtone http://gospel.forum5.com . <a href= http://3gforfree.forum5.com >free ringtone 3gforfree</a> , [url= http://3gforfree.forum5.com ] free ringtone 3gforfree [/url] , free ringtone 3gforfree http://3gforfree.forum5.com . -- [[Ralf]] &new{2007-08-18 (土) 00:16:28};
#comment
* The OCaml Summer Project [#bdda327b]
The OCaml Summer Project - from gmailの広告:)
http://osp2007.janestcapital.com/
*HaskellでWIKI [#x4eef27a]
書いてみました。いまのところ日本語は使えません。
http://icecs.ice.nuie.nagoya-u.ac.jp/~h043078b/wiki.cgi
*OCamlマスコット [#b01a2279]
OCamlはフランス生まれ。フランスでは日本のアニメが受け入れられていると、のだめにも書かれている。そこで、こんなマスコットはどうだろう。
- http://www.ctb.ne.jp/~silver-s/view/V_camel03.jpg
http://www.ctb.ne.jp/~silver-s/view/V_camel02.jpg
http://www.ctb.ne.jp/~silver-s/view/V_camel01.jpg
http://www.ctb.ne.jp/~silver-s/camel.htm
//#comment
* プログラミング言語Factor [#of2c212d]
http://factorcode.org/
逆ポーランド記法な言語。"1 2 +"など、日本語だと思えばスラスラ読めます。
* 数独 [#n52a102c]
** yet another [#x8235231]
- 解説 http://d.hatena.ne.jp/Gemma/20070128
- 2次元配列仕様、16x16に対応。solve は複数解をリストで返します。ここではそのheadをとっているので、解がひとつ見つかりしだい終了します。 - げんま 06/11/25
import System
import List
import Array
import Char
import Monad
dim = 16
sqrtdim = 4
isSingle [x] = True
isSingle _ = False
slice n [] = []
slice n l = a:(slice n b) where (a,b) = splitAt n l
allCells = range ((0,0),(dim-1,dim-1))
rowCells idx =
let (row,col) = idx
in range ((row,0),(row,dim-1))
colCells idx =
let (row,col) = idx
in range ((0,col),(dim-1,col))
boxCells idx =
let (row,col) = idx
a = (row `div` sqrtdim) * sqrtdim
b = (col `div` sqrtdim) * sqrtdim
in range ((a,b),(a+(sqrtdim-1),b+(sqrtdim-1)))
unfixedCells ar = filter (?idx -> not (isSingle (ar!idx))) allCells
arrayList ar = [ar!idx | idx <- allCells]
logicalSolve ar =
let ar' = foldl f ar $ unfixedCells ar
where f ar idx = ar//[(idx, getCandidate ar idx)]
ar'' = foldl f ar' $ unfixedCells ar'
where f ar idx =
case find isSingle $ map (?func -> ar!idx ?? concat [ar!n | n <- func idx, n /= idx]) [rowCells, colCells, boxCells] of
Nothing -> ar
Just x -> ar//[(idx, x)]
in
if any (?idx -> ar!idx /= ar''!idx) $ allCells
then logicalSolve ar''
else ar''
candarList ar = [ar//[(idx,[x])] | x <- ar!idx] where idx = head $ unfixedCells ar
solve ar | all (?idx -> isSingle (ar!idx)) $ allCells = return ar
| any (?idx -> (ar!idx) == []) $ allCells = fail "fail"
| otherwise = do candar <- candarList ar
solve (logicalSolve candar)
getCandidate ar idx =
let used = concat [ar!x | x <- rowCells idx ++ colCells idx ++ boxCells idx, isSingle (ar!x)]
in
[1..dim] ?? used
main :: IO ()
main = do
[file] <- getArgs
contents <- readFile file
let start = listArray ((0,0),(dim-1,dim-1))
$ map (?x -> if x == [0] then [1..dim] else x)
$ map (?x -> [(mdigitToInt x)]) (concat (lines contents))
printArray (head (solve (logicalSolve start)))
where printArray ar = mapM_ putStrLn $ (slice dim l)
where l = map mintToDigit (concat (arrayList ar))
mdigitToInt x | isDigit x = digitToInt x
| x == 'a' = 10
| x == 'b' = 11
| x == 'c' = 12
| x == 'd' = 13
| x == 'e' = 14
| x == 'f' = 15
| x == 'g' = 16
| otherwise = -1
mintToDigit x | x < 10 = intToDigit x
| x == 10 = 'a'
| x == 11 = 'b'
| x == 12 = 'c'
| x == 13 = 'd'
| x == 14 = 'e'
| x == 15 = 'f'
| x == 16 = 'g'
| otherwise = '0'
入力
050g02c00f70b080
0008500f300dc000
c0e0100b80090d03
0f00030000e00010
3000006974000001
00b5380000fc6700
208700500a00df04
0c0e00400d009030
006080f00c030b00
490fcab005g83027
00c0000340000500
80030007b000a00c
0e006f3008c100b0
03d0000cf0000g60
004b00000000fc00
f0004b0e50670008
出力
d53ge2c61f74b98a
b128549f3gadce76
c7e41gab86592df3
af96d378cbe2541g
3afd2c6974beg851
94b538dg21fc67ae
2687be519a3gdfc4
1cgef74a6d85923b
7g6285f4ac13eb9d
491fcabde5g83627
ebca912347d685gf
8d53g6e7b29fa14c
ge796f32d8c14ab5
53d1a98cfe4b7g62
684b7d15g32afce9
f2ac4bge596713d8
timeは、0m2.065s @ Pen4 2.6GHz
**Prolog で数独(sue) [#q7446ee0]
-プログラム
?- use_module(library(bounds)).
resolve([Row1,Row2,Row3,Row4,Row5,Row6,Row7,Row8,Row9]) :-
rowCheck([Row1,Row2,Row3,Row4,Row5,Row6,Row7,Row8,Row9]),
columnCheck(Row1,Row2,Row3,Row4,Row5,Row6,Row7,Row8,Row9),
blockCheck([Row1,Row2,Row3]),
blockCheck([Row4,Row5,Row6]),
blockCheck([Row7,Row8,Row9]),
label(Row1),
label(Row2),
label(Row3),
label(Row4),
label(Row5),
label(Row6),
label(Row7),
label(Row8),
label(Row9).
rowCheck([]).
rowCheck([Row|Rows]) :-
Row in 1..9,
all_different(Row),
rowCheck(Rows).
columnCheck([],[],[],[],[],[],[],[],[]).
columnCheck([N1|Row1],[N2|Row2],[N3|Row3],[N4|Row4],[N5|Row5],[N6|Row6],[N7|Row7],[N8|Row8],[N9|Row9]) :-
all_different([N1, N2, N3, N4, N5, N6, N7, N8, N9]),
columnCheck(Row1, Row2, Row3, Row4, Row5, Row6, Row7, Row8, Row9).
blockCheck([Row1,Row2,Row3]) :-
nth1(1, Row1, N11),
nth1(2, Row1, N12),
nth1(3, Row1, N13),
nth1(1, Row2, N21),
nth1(2, Row2, N22),
nth1(3, Row2, N23),
nth1(1, Row3, N31),
nth1(2, Row3, N32),
nth1(3, Row3, N33),
all_different([N11, N12, N13, N21, N22, N23, N31, N32, N33]),
nth1(4, Row1, N14),
nth1(5, Row1, N15),
nth1(6, Row1, N16),
nth1(4, Row2, N24),
nth1(5, Row2, N25),
nth1(6, Row2, N26),
nth1(4, Row3, N34),
nth1(5, Row3, N35),
nth1(6, Row3, N36),
all_different([N14, N15, N16, N24, N25, N26, N34, N35, N36]),
nth1(7, Row1, N17),
nth1(8, Row1, N18),
nth1(9, Row1, N19),
nth1(7, Row2, N27),
nth1(8, Row2, N28),
nth1(9, Row2, N29),
nth1(7, Row3, N37),
nth1(8, Row3, N38),
nth1(9, Row3, N39),
all_different([N17, N18, N19, N27, N28, N29, N37, N38, N39]).
-実行結果
?- time(resolve(
[[N11, N12, 6, N14, N15, N16, N17, N18, 1],
[N21, 7, N23, N24, 6, N26, N27, 5, N29],
[8, N32, N33, 1, N35, 3, 2, N38, N39],
[N41, N42, 5, N44, 4, N46, 8, N48, N49],
[N51, 4, N53, 7, N55, 2, N57, 9, N59],
[N61, N62, 8, N64, 1, N66, 7, N68, N69],
[N71, N72, 1, 2, N75, 5, N77, N78, 3],
[N81, 6, N83, N84, 7, N86, N87, 8, N89],
[2, N92, N93, N94, N95, N96, 4, N98, N99]]
)).
% 218,588 inferences, 0.05 CPU in 0.05 seconds (94% CPU, 4371760 Lips)
N11 = 5,
N12 = 3,
N14 = 8,
N15 = 2,
・
・
・
長いので略．
一応合ってるっぽい．
拡張性無い & もっとスマートに書けるはず．
でもやっぱり速い．なぜ?
** original [#g4b15298]
11月13日のネタ。とりあえず9x9限定です。
とりあえずソースはこんな感じでした。みなさんにいろいろとつっこまれましたが、とりあえず修正はしてません。それにしてもgoはいただけないね、我ながら。
(追記)Haskell Hackerにデバッグしていただきました！
-- Leftが不確定要素(リスト)でRightが確定要素
import System
import Array
-- 最初のLeftを見つけて候補のリストを作る。
go ar = case first 0 of
Nothing -> [Right ar]
Just n -> map (?c -> Left $ ar//[(n,Right c)]) (getCandidate n)
where
first n = if n>80 then
Nothing
else
case ar!n of
Right _ -> first (n+1)
Left _ -> Just n
-- 候補のリストを作る関数
getCandidate n =
let used = getRow n ar ++ getCol n ar ++ getBox n ar in
[x|x<-"123456789", notElem x used]
-- 9x9 の数独を想定。使われている関数を見つけ出す関数
getRow n ar = let row = n `div` 9 in
concatMap (?n -> case ar!(row*9+n) of
Right x -> [x]
Left _ -> []) [0..8]
getCol n ar = let col = n - (n `div` 9 * 9) in
concatMap (?n -> case ar!n of
Right x -> [x]
Left _ -> []) [col,col+9..col+72]
getBox n ar = let line = n `div` 9 -- 行
col = n - (n `div` 9 * 9) -- 列
-- i = line `div` 3 -- 左上のy
i = line `div` 3 * 3 -- 左上のy <- ここを修正!
j = col `div` 3 * 3 -- 左上のx
in
concatMap (?n -> case ar!n of
Right x -> [x]
Left _ -> []) [x*9+y|x<-[i..i+2], y<-[j..j+2]]
-- ファイルからデータを読み込んで最初の配列を作る
main :: IO ()
main = do args <- getArgs
case args of
[] -> return ()
_ -> do contents <- readFile (args!!0)
let start = array (0,80) $ zip [0..]
[if cs=='0' then Left "0" else Right cs|cs<-contents, cs/='?n']
answer = next [Left start]
putStr9 $ map (?n -> fromRight $ answer!n) [0..80]
where
next ars = case get ars of -- ここを回る
[a] -> a -- found!
[] -> next (next' ars >>= go) -- not yet found
next' [] = [] -- Leftをはがす関数
next' (x:xs) = case x of
Left ars -> ars : next' xs
Right _ -> error "you never see this message."
get [] = [] -- 終了したもの(Right)があるかどうか
get (x:xs) = case x of
Right a -> [a]
Left _ -> get xs
putStr9 [] = return ()
putStr9 str = do let (a,b) = splitAt 9 str
putStrLn a
putStr9 b
fromRight x = case x of
Right y -> y
_ -> error "This is left"
入力例。
006000001
070060050
800103200
005040800
040702090
008010700
001205003
060070080
200000400
出力。
536827941
172964358
894153267
715349826
643782195
928516734
481295673
369471582
257638419
ちなみに、PowerPC 1GHzのiBookで
0.16s user 0.02s system 76% cpu 0.236 total
でした。
* SEND + MORE = MONEY を解いてみよう! [#e74b7ff8]
S E N D
+ M O R E
----------
M O N E Y
(S,M != 0)
- 10/18の OCaml講義第3回 by ガリグ先生で、授業の課題として出ました。
- 授業では、search関数はガリグ先生のお手本があって、生徒はcheck関数を書くだけでしたが。
- 計算量が苦しいなら、M=1はOKにしましょう。 - げんま
** 授業の課題 [#w55b6646]
let toint (li : int list) =
List.fold_left (fun a b -> (a * 10 + b)) 0 li;;
let check (d : (char * int) list) =
let f l = (toint (List.map (fun a -> List.assoc a d) l)) in
((List.assoc 'S' d != 0) &&
(List.assoc 'M' d != 0) &&
((f ['S'; 'E'; 'N'; 'D']) + (f ['M'; 'O'; 'R'; 'E']) = (f ['M'; 'O'; 'N'; 'E'; 'Y'])));;
let rec search dict letters numbers =
match letters with
[] -> if check dict then [dict] else []
| a :: letters ->
let rec choose tried numbers =
match numbers with
[] -> []
| n :: numbers ->
let sols = search ((a, n) :: dict) letters (tried @ numbers) in
sols @ choose (n::tried) numbers
in
choose [] numbers ;;
let rec interval m n =
if m > n then [] else m :: interval (m+1) n;;
let solve () =
search [] ['S';'E';'N';'D';'M';'O';'R';'Y'] (interval 0 9);;
solve();;
** Gauche [#if874cf2]
ライブラリに、順列組み合わせのpermutationなどがあったので、かなり楽ができました。見つかったらreturnラベルで大域脱出。2.6Ghzで13秒。 - げんま
(use srfi-1)
(use util.combinations)
(use util.match)
(define return #f)
(define (eval-poly li x)
(fold (lambda (a b) (+ a (* b x))) 0 li))
(define (check li)
(match li
((S E N D M O R Y)
(if
(and
(not (= S 0))
(not (= M 0))
(= (+ (eval-poly (list S E N D) 10)
(eval-poly (list M O R E) 10))
(eval-poly (list M O N E Y) 10)))
(return (list S E N D '+ M O R E '= M O N E Y))))))
(define (solve)
(combinations-for-each
(lambda (a) (permutations-for-each check a))
(iota 10) 8))
(print
(call/cc
(lambda (cc)
(set! return cc)
(solve))))
**Haskellで解いてみる [#n5f2521d]
(''追記''：[[nobsunさんのコード:http://haskell.g.hatena.ne.jp/nobsun/20061019/alphametic]]のほうがスマート。)
([[らくがきえんじん:http://d.hatena.ne.jp/syd_syd/20061018]]にも書いた。)
何も考えてない。15分くらいででけた。こういう問題にはリストモナドがめっぽう強い。（けいご）
Showのインスタンスが必要なのはご愛嬌。
import Control.Monad.State
ten = [0..9]
-- StateT [Int] [] Intが何であるかを考えるより、単に [Int]->[(Int,[Int])] だと思えばよい
-- (「リストlを貰って、その中のどれかの要素eと、lからeを取った残りl'の対(e,l')を返す」という非決定的な関数)
getNum :: StateT [Int] [] Int
getNum = StateT $ ?ns -> do{n <- ns; return (n, filter (n/=) ns)}
sendmory = do
s <- getNum
if s==0 then lift [] else return ()
m <- getNum
if m==0 then lift [] else return ()
e <- getNum
n <- getNum
d <- getNum
o <- getNum
r <- getNum
y <- getNum
if s*1000+e*100+n*10+d+m*1000+o*100+r*10+e==m*10000+o*1000+n*100+e*10+y then return (s,e,n,d,m,o,r,y) else lift []
instance (Show s, Show e, Show n, Show d, Show m, Show o, Show r, Show y)=>
Show (s,e,n,d,m,o,r,y) where
show (s,e,n,d,m,o,r,y) = "("++show s++","++show e++","++show n++","++show d++","++show m++","++show o++","++show r++","++show y++")"
main = print (evalStateT sendmory ten)
sydney$ ghc -package mtl Desktop/hoge.hs -o a.out
sydney$ time ./a.out
[(?,?,?,?,?,?,?,?)]
real 0m4.544s
user 0m4.341s
sys 0m0.076s
体感5秒位 (PPC, 2.3GHz dual) ただし今インタプリタ(ghci)で試したら25秒くらいかかった。
**そっちがMonadなら、こっちはamb<<改訂版>> [#rad040bb]
- 48秒@2.6GHz- げんま
(use srfi-1)
;; stack of cc.
(define fail '())
;; nondeterminsm operator
(define (amb li)
(if (null? li)
((pop! fail))
(call/cc
(lambda (cc)
(push! fail (lambda ()
(cc (amb (cdr li)))))
(car li)))))
(define (toint li)
(fold (lambda (a b) (+ a (* b 10))) 0 li))
(define (solve)
(let ((digs (iota 10 0))
(digs1 (iota 9 1)))
(let* ((S (amb digs1))
(E (amb (lset-difference = digs (list S))))
(N (amb (lset-difference = digs (list S E))))
(D (amb (lset-difference = digs (list S E N))))
(M (amb (lset-difference = digs1 (list S E N D))))
(O (amb (lset-difference = digs (list S E N D M))))
(R (amb (lset-difference = digs (list S E N D M O))))
(Y (amb (lset-difference = digs (list S E N D M O R)))))
(if
(= (+ (toint (list S E N D))
(toint (list M O R E)))
(toint (list M O N E Y)))
(list S E N D '+ M O R E '= M O N E Y)
(amb '())))))
(print
(call/cc
(lambda (cc)
;; initial value for fail
(push! fail
(lambda ()
(cc 'no-choise)))
(solve))))
**憶えたての Prolog でやってみる(sue) [#nddbaf73]
-Program
?- use_module(library(bounds)).
smm(S, E, N, D, M, R, O, Y) :-
Digits = [S, E, N, D, M, R, O, Y],
Digits in 0..9,
all_different(Digits),
S #> 0,
M #> 0,
Send = S * 1000 + E * 100 + N * 10 + D,
More = M * 1000 + O * 100 + R * 10 + E,
Money = M * 10000 + O * 1000 + N * 100 + E * 10 + Y,
Send + More #= Money,
label(Digits).
-実行結果
?- [sendmoremoney].
% sendmoremoney compiled 0.00 sec, 16 bytes
Yes
?- time(smm(S, E, N, D, M, R, O, Y)).
% 40,088 inferences, 0.02 CPU in 0.02 seconds (111% CPU, 2004400 Lips)
S = 9,
E = 5,
N = 6,
D = 7,
M = 1,
R = 8,
O = 0,
Y = 2
直感的．
- 0.02秒? all_different(Digits)は、10C8 * 8! 個の組み合わせを試すんだよね? -- [[げんま]] &new{2007-04-13 (金) 15:56:43};
- 書いておきながらよく分かってないんだけど，おそらく全探索のはず．なぜこんなに速いんだろう... -- [[sue]] &new{2007-04-13 (金) 20:52:33};
- よく考えたら，これは一つ目の解を出すまでの時間だから，たまたま早かった，というのもありうる... -- [[sue]] &new{2007-04-13 (金) 20:54:21};
- 「正解なんて用意されてないのさ、全探索ごくろうさま!」のタイムを見てみたいです。 -- [[げんま]] &new{2007-04-13 (金) 22:36:49};
#comment
*javascriptでゲームなら、<canvas>タグが面白い![#k543fb5f]
-[[3DWalker:http://www.abrahamjoffe.com.au/ben/canvascape/index.htm]]
http://www.geocities.jp/teruakigemma/scheme2js/doom.png
*継続とは?[#y87e71e0]
**参考文献 [#c9a07956]
-[[なんでも継続:http://www.shiro.dreamhost.com/scheme/docs/cont-j.html]]
-[[Scheme:なぜSchemeにはreturnが無いのか:http://www.shiro.dreamhost.com/scheme/wiliki/wiliki.cgi?Scheme%3a%e3%81%aa%e3%81%9cScheme%e3%81%ab%e3%81%afreturn%e3%81%8c%e7%84%a1%e3%81%84%e3%81%ae%e3%81%8b]]
-[[Schemeを作ろう 第3回:http://www.jah.ne.jp/~naoyuki/Writings/VScheme3.html]]
-[[Scheme入門 継続:http://www.shido.info/lisp/scheme_cc.html]]
- 継続には副作用がある。
[[Scheme:call/ccと副作用:http://www.shiro.dreamhost.com/scheme/wiliki/wiliki.cgi?Scheme%3acall%2fcc%e3%81%a8%e5%89%af%e4%bd%9c%e7%94%a8]]
**何ができるの? [#c933f2be]
- 大域脱出
- 例外処理
- [[非決定性:http://www.shido.info/lisp/scheme_amb.html]] [[gemmaの実装:http://www.shiro.dreamhost.com/scheme/wiliki/wiliki.cgi?amb]]
例えば、
(let ((i (amb 4 6 7))
(j (amb 5 8 11)))
(if (prime? (+ i j))
(list i j)
(amb)))
;Value 23: (6 5)
のようにすると '(4 6 7) と '(5 8 11) のうちから二つの数の和が素数になる組の１つを返します。
これを理解するのに、自分は3ヶ月かかりました。
ambは、バックトラック演算子です。動きを大雑把に言うと、
(let (i (amb 4 6 7))で、
i に 4 が入ると同時に、
この時点のツヅキ、
"6 7))
(j (amb 5 8 11)))
(if (prime? (+ i j))
(list i j)
(amb)))"
を取り出して、スタックにpush。
次の行、
(j (amb 5 8 11))で、
j に 5が入ると同時に、
この時点のツヅキ、
"8 11)))
(if (prime? (+ i j))
(list i j)
(amb)))"
を取り出して、スタックにpush。
(prime? (+ 4 5))は偽。(amb)が動く。amb関数は、引数なしで呼ばれると、スタックをpopして、中身の、ツヅキを実行。
"8 11)))
(if (prime? (+ i j))
(list i j)
(amb)))"
が実行されて、jに8が入ると同時に、
この時点のツヅキ、
"11)))
(if (prime? (+ i j))
(list i j)
(amb)))"
を取り出して、スタックにpush...という感じです。
**もっと教えて! [#vf61a3fe]
-[[名大の謎の天才h003149b氏:http://www.ice.nuie.nagoya-u.ac.jp/~h003149b/lang/index.html]]
-[[SICP.Nondeterministic Computing:http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-4.html#%_toc_%_sec_4.3]]
**継続サーバはどうなった? [#qc90b476]
-[[境界を越える: 継続とWeb開発、そしてJavaプログラミング:https://www-06.ibm.com/jp/developerworks/java/060412/j_j-cb03216.shtml]]
-[[継続サーバの実装の最先端、Seaside:http://www.seaside.st/]]
-[[Seasideの開発者が継続のゆくえについて語る:http://smallthought.com/avi/?p=14]]
-[[HaskellのWASH:http://www.informatik.uni-freiburg.de/~thiemann/haskell/WASH/]]
-[[もとネタになった??Queinnec氏の論文PDF:http://www-spi.lip6.fr/~queinnec/PDF/webcont.pdf]]
-[[WebBasedアプリケーションと継続について、わかりやすい説明:http://www.shiro.dreamhost.com/scheme/wiliki/wiliki.cgi?Scheme%3aCPS]]
* 型クラスがあるC言語!? [#h5b86e1f]
- [[Jekyll:http://jekyllc.sourceforge.net/index.html]]
>Jekyll is a high-level language that can be losslessly translated to and from readable editable C. This allows it to be used in C projects, with C programmers, C libraries, and C tools.
* Compiling Scheme to JavaScript [#p1b71405]
- http://hop.inria.fr/usr/local/share/hop/weblets/home/articles/scheme2js/article.html
- 夏休み中に、Hopを試してみるつもりです。 -- [[げんま]] &new{2006-08-10 (木) 09:39:32};
- [[Compiling to JavaScript:http://calculist.blogspot.com/2006/08/compiling-to-javascript.html]]いろんな言語で、Javascriptへのコンパイルが模索されているらしい。 -- [[げんま]] &new{2006-08-26 (土) 10:22:24};
- Scheme2jsを使って、テトリスを書いてみました。http://www.geocities.jp/teruakigemma/scheme2js/demo.html -- [[げんま]] &new{2006-09-02 (土) 21:10:45};
- sugeeeeee! -- [[Keigo]] &new{2006-09-04 (月) 16:55:31};
- あれ、IEだとキー入力ができないです。Firefoxでならできてたんです。 -- [[げんま]] &new{2006-09-04 (月) 21:23:40};
- Safari(MacOSX)ではOK。ところで勉強会には来れません？ -- [[けいご]] &new{2006-09-04 (月) 21:56:00};
- １１日の勉強会に行きます。浜松に帰省してましたが、ようやく。PPLサマースクールでバイト申し込んだので、そこでもみんなに会えます♪ -- [[げんま]] &new{2006-09-05 (火) 10:13:39};
- prototype.jsのおかげで、ＩＥでキー入力できるようになりました。 -- [[げんま]] &new{2006-09-05 (火) 22:55:07};
- script.aculo.usのデモを書いてみました。Firefoxでは動いてるんですが、他だとどうでしょう。http://www.geocities.jp/teruakigemma/scheme2js/aculo.html -- [[げんま]] &new{2006-09-07 (木) 02:09:49};
* Proof are Programs [#fca44cec]
- http://www.radiumsoftware.com/0605.html#060523
- Philip Wadler. [[Proofs are Programs: 19th Century Logic and 21st Century Computing:http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf]]
- 数理論理学とコンピュータ・プログラムの間には深い関連性がある。この論文では，近代論理学の開祖であるフレーゲの概念記法を出発点として，ゲンツェンの自然演繹 と，チャーチの型付きラムダ計算の二つの流れを追い，最終的にそれらのモデルがカリー・ハワード対応によって同型として対応付けられるところまでを辿る。
* History of Haskell [#z4d010cb]
- http://haskell.org/haskellwiki/History_of_Haskell
- HOPL'07に提出する予定の論文の、ドラフトだそうです。
* Functional Reactive Programming [#i4d505da]
- http://www.haskell.org/frp/
- LL3での、"Functional Reactive Programming in Scheme"の発表者、 Gregory Cooper氏のホームページ http://www.cs.brown.edu/~greg/
* roguelike in ocaml [#o7afaf8c]
(今井) http://cristal.inria.fr/%7Eddr/mlrogue/
- おぉーー! -- [[源馬]] &new{2006-07-13 (木) 03:12:06};
* 尋ね人 [#sdf98c23]
- 場違いな質問で恐縮ですが、ご存じありませんか? 名大の方みたいなんですが。
- http://www.ice.nuie.nagoya-u.ac.jp/~h003149b/lang/index.html -- [[源馬]] &new{2006-07-11 (火) 04:30:06};
- その人、気になりますよね。私と同い年です。元坂部研という噂。ただ、私は情報工学の人間ではなかったので、知りません。末ちゃんなら知ってると思う。 -- 今井
- たくさん興味深いことを書かれているので、続きを読みたい! -- [[源馬]] &new{2006-07-13 (木) 03:18:14};
- 確かに同級生のようです．ただ名前が無いので誰だか分からない。。。 -- [[末次]] &new{2006-08-10 (木) 21:59:55};
- 名字は"水野"だそうです。そこまでなんとか掴みました。 -- [[末次]] &new{2006-08-10 (木) 22:10:37};
- "水野"で坂部研なら水野 清貴君かな? かなり当てずっぽうです．信憑性はありません． -- [[末次]] &new{2006-08-10 (木) 22:13:33};
- 違うよ。そうじゃなくて…僕らがB4の時の坂部研だったはず -- [[けいご]] &new{2006-08-11 (金) 12:07:11};
- M1になってはじめに聞いたのが彼の行方だったのだけど(明らかに先を越されていたから)、確か末ちゃんその時は教えてくれたような… -- [[けいご]] &new{2006-08-11 (金) 12:09:11};
- [[はてなブックマークでもそれなりに人気が:http://b.hatena.ne.jp/entrylist?url=http%3A%2F%2Fwww.ice.nuie.nagoya-u.ac.jp%2F]] -- [[けいご]] &new{2006-08-11 (金) 12:28:46};
*[[AA折れ線グラフ:http://oss.timedia.co.jp/index.fcgi/kahua-web/show/column/%ba%a3%c6%fc%a4%ce%b0%ec%b9%d4/%a3%b2%a3%b0%a3%b0%a3%b6%c7%af%a3%b3%b7%ee#H-1bpntk8]] [#j83662b2]
>AAで折れ線グラフを書くというお題．
>入力は'R','F','C'の3種類も文字からなる長さ1以上の文字列
>'R'は上昇を表し，折れ線グラフの要素としては '/' (スラッシュ)1文字に対応
>'F'は下降を表し，折れ線グラフの要素としては '?' (バックスラッシュ)1文字に対応
>'C'は変化なしを表し，折れ線グラフの要素としては'_'(アンダスコア)1文字に対応
>たとえば，
$ ./plot RCRFCRFFCCRFFRRCRRCCFRFRFF
>とすると
__
/ ?/?/?
_/?_/? _/ ?
/ ?__/? /
?/
>が出力されるようなスクリプトを書け．
> --nobsun
源馬のSchemeでの回答はこちら。~
http://www.shiro.dreamhost.com/scheme/wiliki/wiliki.cgi?gemma -- [[源馬]] &new{2006-07-01 (土) 12:00:06};
**解答 in Haskell [#nd70223e]
下村です。
無駄に長い上に汚いですけど…。
output str =
let result = graph str
output' :: [String] -> IO ()
output' mat =
if any null mat then return ()
else do if any (' '/=) h then putStrLn h
else return ()
output' t
where
h = map head mat
t = map tail mat
in
output' result
graph :: String -> [String]
graph str =
let
height = (length str) * 2
graph' [] _ = []
graph' (x:xs) pos =
case x of
'R' -> oneline (pos) '/' height : graph' xs (pos-1)
'F' -> oneline (pos+1) '??' height : graph' xs (pos+1)
'C' -> oneline pos '_' height : graph' xs pos
in
graph' str (length str)
-- n番目の文字がcであるような、長さlの文字列を生成する
oneline :: Int -> Char -> Int -> String
oneline _ _ 0 = ""
oneline n c l = (if n==0 then c else ' ') : oneline (n-1) c (l-1)
で、結果は…
Main> output "RCRFCRFFCCRFFRRCRRCCFRFRFF"
__
/ ?/?/?
_/?_/? _/ ?
/ ?__/? /
?/
Main>
**解答 in OCaml [#yc2d1595]
また下村です。OCamlで書き換えたので書いときます。Haskell版より関数とかをちょっと整理しました。あと、文字列はコマンドライン引数で指定するようにしてあります。explodeとimplodeは拡張ライブラリ関数なので、コンパイルするためにはExtLibをインストールする必要があります。
(* <<COMPILE>> "ocamlopt -I +extlib extlib.cmxa lineGraph.ml" *)
open ExtString.String;;
open List;;
exception NotRFC;;
let any = List.fold_left (or) false;;
let graph charlist =
let height = (length charlist) * 2 in
let rec transpose mat = if any (map (fun x -> x=[]) mat)
then []
else map hd mat :: transpose (map tl mat) in
let rec oneline n c l = if l=0
then []
else (if n=0 then c else ' ') :: oneline (n-1) c (l-1) in
let rec graph' charlist pos =
match charlist with
[] -> []
| c::cs -> match c with
'R' -> oneline (pos) '/' height :: graph' cs (pos-1)
| 'F' -> oneline (pos+1) '??' height :: graph' cs (pos+1)
| 'C' -> oneline pos '_' height :: graph' cs pos
| otherwise -> raise NotRFC
in
transpose (graph' charlist (length charlist));;
let output =
try
let result =
map (fun l -> if any (map (fun x -> x<>' ') l)
then implode l ^ "?n" else "")
(graph (explode Sys.argv.(1))) in
let rec output' list = match list with
[] -> ()
| (""::ls) -> output' ls
| (l::ls) -> print_string l;
output' ls in
output' result
with
NotRFC ->
print_string ("Usage : " ^ Sys.argv.(0) ^ " [RFC]*?n")
| Invalid_argument _ ->
print_string ("Usage : " ^ Sys.argv.(0) ^ " [RFC]*?n");;
実行結果は…
mac{sho}% ./a.out RCRFCRFFCCRFFRRCRRCCFRFRFF [~/src/ocaml]
__
/ ?/?/?
_/?_/? _/ ?
/ ?__/? /
?/
mac{sho}% [~/src/ocaml]
- Ocamlがわかってないので、おぼろげにしかわからないです。なんかすごい。今度、教えてください。 -- [[源馬]] &new{2006-07-04 (火) 03:35:28};
* HaskellでOS。 [#s0a682d7]
http://www.cse.ogi.edu/~hallgren/House/ -- [[源馬]] &new{2006-07-04 (火) 16:16:05};
*The Evolution of a Haskell Programmer [#ga1c48ba]
[[The Evolution of a Haskell Programmer:http://www.willamette.edu/~fruehr/haskell/evolution.html]] かなりハイレベルにバカやってる感じ
- バカだ〜！fold関数使うまではわかるけど、その後が！まだまだまだまだ続くし。 -- [[げんま]] &new{2006-08-12 (土) 10:35:43};
- インタプリタを作って階乗計算させたり，型クラスを使ったテクニックなんかもあるので分かると結構良いかも。 -- [[けいご]] &new{2006-08-12 (土) 15:27:52};
![[PukiWiki]](image/caml3.jpg "[PukiWiki]")
