2013年8月30日金曜日

selbriの結合はマグマである。

マグマとは:(wikipediaより)
マグマは集合 M と、M のどの二元 ab に対しても a • b で表される別の元を対応させる二項演算 "•" を対として考える。ここで記号 • は適当に定義された何らかの演算というのを一般に表すためのプレースホルダである。集合と演算の組 (M, •) がマグマと呼ばれるためには、マグマの公理として知られる条件
  • 演算について閉じていること: M の任意の元 ab に対して、その演算結果 a • b が再び M に属する。
を満足しなければならない。演算が明らかで紛れの虞の無いときは、演算を落として台集合の記号のみによってマグマ M などという。(しばしば中置記法に従う)二項演算 • は、マグマ M における乗法とも呼ばれ、このときの演算結果 a • b は a と b とのという[* 2]。また、誤解の虞が無いならば積 a • b は演算記号を省略してしばしば ab と書かれる。

selbriの集合をMとし、修飾演算子(>>)を考える。
たとえば、nixli skami は、 nixli >> skami と書く。左が修飾語で、右が被修飾語。
実際、broda >> brode もまたひとつのselbriであるから、selbriの集合と>>の組はマグマである。
selbriの修飾は、結合則が成り立たないことに注意。
ロジバンでは barda xunre plise は、(barda  >> xunre) >> plise と解される。
ここで、 barda >> (xunre >> plise) は、大きな[赤いりんご] である一方で
(barda >> xunre) >> plise は、[大きい系の赤をした]りんご と解される。
これより、結合則が満たされないことが分かる。
もちろん、単位元も逆元も存在しない。さらには可換則もなりたたない。







2013年8月16日金曜日

Haskellの練習:ヒットアンドブローキラー

import Data.Char
import Data.List
import Control.Applicative
import System.Random

main = do
gen <- getStdGen
let (x, newgen) = randomR (0, length list -1) gen
let firstStr = list !! x
putStrLn $ "HEY. FISRTLY, JUST SAY "++ firstStr ++ "."
solver list [] firstStr newgen

addZero :: String -> String
addZero str = replicate (4 - length str) '0' ++ str

list = filter (\ x -> length x > 3) $ map (nub) $ nub $ map (addZero.nub.addZero.show) [1..9999]

hitCount :: String -> String -> Int
hitCount ans datni = length $ filter (&&True) $ zipWith (\ a b -> if(a==b) then True else False) ans datni

blowCount :: String -> String -> Int
blowCount ans datni = length (filter (&&True) $ (==) <$> ans <*> datni ) - (hitCount ans datni)

behead :: [String] -> [[String]] -> [String]
behead str datni = filter (\ cand -> foldl (\ truth [a,b,c] -> truth && (hitCount a cand) == read b && (blowCount a cand) == read c ) True datni) str

solver :: (RandomGen g) => [String] -> [[String]] -> String -> g -> IO ()
solver cand datni str gen = do
putStrLn $ "GIVE ME INFORMATION: HIT, BLOW..."
element <- fmap (words) getLine
let newdatni = (str : element) : datni
let newcand = behead cand newdatni
let (nextNumber , newgen) = randomR (0, length newcand -1) gen
let nextStr = newcand !! nextNumber
putStrLn $ "NOW, THE NUMBER OF CANDIDATES ARE "++ (show (length newcand )) ++ "."
putStrLn $ "HEY, YOU JUST SAY " ++ nextStr ++ "."
if (length newcand == 1)
then return ()
else solver newcand newdatni nextStr newgen


Haskellの練習がてら、以前にjavaでつくったヒットアンドブローを解くプログラムコードをHaskellでも書いてみた。javaのソースコードが209行、Haskellのソースコードが39行。テキストサイズだと、javaが4918byte, Haskellが1555byteですね。こんな短く書けるなんて…(いや俺がjavaが下手なだけかもしれない)。
テキストはすごいH本を使っています。まあ他にも色んなサイトを転々とはしましたが。
javaでもリスト処理をもう少しまともに勉強すれば短くなったのかもしれない。
Haskellのリスト処理は簡単で素晴らしいですね。

短くできそうなところは…
・list、[1...9999]からヒットアンドブローに使う重複しない4桁の数字を抽出するところ。
・behead (候補を落としていく関数) のラムダ式の入れ子
かなあと思います。とりあえず今の知識だけで頑張りました。


2013年8月7日水曜日

記号論理入門



読みました。面白かったです。
ロジバン関連で、述語論理の知識がほしいなあと思って買ったわけですが、
真理値についての記述がないのが新鮮でした。
Amazonのレビューに「ツメが甘い」的なこと書いてましたが、
論理学者でもないし、数学者でもない、アバウトな人間(僕)にとっては
比較的直感的に書かれていたのでむしろ読み進めやすかった。
たしかに、本格的に記号論理学をやるぞ!って人にはぬるすぎるかもしれない。

問題もなかなか充実しているし、解答も(奇数番だけだが)きちんとありますので、
独習でも充分なテキストだと思います。

教養として論理学を学びたい(特に推論)人は是非。
難易度的には高校生でも読めると思います。

2013年8月6日火曜日

∀と∃ メモ

(∀x) Fx や、(∃x)Fx は簡単にわかるとして、∀x ∃y Fxy など、入れ子になるとわかりにくくなる。

∀と∃は「全称」「存在」と訳されているが、思い切って、

∀ ・・・ 偽をみつけたら偽を返す量化子
∃ ・・・ 真をみつけたら真を返す量化子

と考えるのもよさそうだ。

∀x Fx というのは、議論領域のxについて走査していき、Fxが偽になれば偽を返せということ
∃x Fx というのは、議論領域のxについて走査していき、Fxが真になれば真を返せということ

若干、プログラミングちっくにかけば…

■∀x Fx
while(未調査の要素xが存在する){
 if (Fx == False) return False;
}
return Ture

■∃x Fx
while(未調査の要素xが存在する){
 if(Fx == True) return True;
}
return False;


このことからも、
「すべての人間はいずれ死ぬ」を ∀x { Hx ⇒ Dx}
「ある人間はいずれ死ぬ」を ∃x { Hx ∧ Dx}
と書き分ける理由がわかる。

∀xのxは議論領域が定まっていなければ、万物を指す。
∀x ~の命題は、偽がひとつでも出ればFalseを返して終了してしまうので、
∀x {Hx ∧ Dx}とは書けない。これは当然とも言える。
ほとんどすべての場合で、∀x {Hx ∧ Dx}はFalseを返してしまうだろう。
一方で、∀x { Hx ⇒ Dx}は適切である。
これは、非人間なxについてはHxがFalseとなることで「Hx⇒Dx」がTrueであり続けるからだ。
平たくいえば、非人間なxへのフィルターがかかるので、きちんと働く。

∃xのxも議論領域が定まっていなければ、万物を指す。
∃x~の命題は、真がひとつでも出ればTrueを返して終了してしまうので、
∃x {Hx ⇒ Dx} とは書けない。これは⇒の性質による。
すなわち、Hx ⇒ Dx は、HxがFalseであれば真となってしまうため、
そこで∃x~の命題がTrueを返してしまうからである。これは言いたいこととは異なる。
ほとんどすべての場合で、∃x {Hx ⇒ Dx}はTrueを返してしまうはずである。
一方で、∃x { Hx ∧ Dx}は適切である。
これは、非人間なxについてはHxがFalseとなることで「Hx ∧ Dx」がFalseとなり続けるため。
平たく言えば、非人間なxへのフィルターがかかるので、きちんと働く。

結局、∀と∃で違う表現をとらなければならないのは、その性質、すなわち「偽をみつける」のか「真をみつける」のかの違いに起因するともとれる。


入れ子量化子も「偽をみつける」「真をみつける」という視点でみれば、そこそこ見やすいかも。

∀x ∃y (x loves y)
これは、xを走査していき、∃y (x loves y)が偽となるものがあればFalseを返す命題。
∃y (x loves y) の真偽をみるためには、(一時的に固定された)xの元で、
yを走査していき、x loves y が真となるものがあるかどうかをみればよい。(なければ偽)

∃y ∀x (x loves y)
これは、yを走査していき、∀x (x loves y)が真となるものがあればTrueを返す命題。
∀x (x loves y)の真偽をみるためには、(一時的に固定された)yの元で、
xを走査していき、x loves y が偽となるものがあるかどうかをみればよい。(なければ真)


なお、∀が「偽をみつける」量化子であるのは、
∀x Fx と¬(∃x ¬Fx)が同値であることからも明らか。
すなわち、FxがFalseとなるxが存在すれば、∀x Fxは偽となるのである。