遺伝学・遺伝統計学関連の姉妹ブログ『ryamadaの遺伝学・遺伝統計学メモ』
京都大学大学院医学研究科ゲノム医学センター統計遺伝学分野のWiki
講義・スライド
医学生物学と数学とプログラミングの三重学習を狙う学習ツール
駆け足で読む○○シリーズ
ぱらぱらめくるシリーズ
カシオの計算機
オンライン整数列大辞典

2 Talking about Mathematical Objects 数学オブジェクトを語る ぱらぱらめくる『The Haskell Road to Logic, Maths and Programming』

Haskell ぱらぱらめくるシリーズ
  • この章はどちらかというと、論理演算の概論。Haskellで実装できない・しないでよい部分も多いので読むのを基本に。
  • Connectives 論理演算子の話
    • and(conjunction),or(disjunction),not(negation),if-then(implication),if-and-only-if=iff(equivalence)
GS> :i Bool
data Bool = False | True        -- Defined in ‘GHC.Types’
instance Bounded Bool -- Defined in ‘GHC.Enum’
instance Enum Bool -- Defined in ‘GHC.Enum’
instance Eq Bool -- Defined in ‘GHC.Classes’
instance Ord Bool -- Defined in ‘GHC.Classes’
instance Read Bool -- Defined in ‘GHC.Read’
instance Show Bool -- Defined in ‘GHC.Show’
  • Exercise 2.2 exclusive or (xor)の演算表(実は<+>がその中置演算子)
    • T xor T = F, T xor F = T, F xor T = T, F xor F =T
    • その他の表
TAMO> [ not x | x <- [True,False] ]
[False,True]
TAMO> [ x && y | x <- [True,False], y <- [True,False] ]
[True,False,False,False]
TAMO> [ x || y | x <- [True,False], y <- [True,False] ]
[True,True,True,False]
TAMO> [ x <=> y | x <- [True,False], y <- [True,False] ]
[True,False,False,True]
TAMO> [ x ==> y | x <- [True,False], y <- [True,False] ]
[True,False,True,True]
TAMO> [ x <+> y | x <- [True,False], y <- [True,False] ]
[False,True,True,False]
  • 中置関数の定義
    • 第１行 "infix 1 ==>"を書かなくても、==>という記号が中置関数として働き、それを(==>)のようにかっこでくくれば、前置関数として使える
    • では、"infix 1 ==>"は何か、と言えば、「複数の中置関数１行のコマンドに並んでしまったときに、どれを先にやるか」というのを決めないと、困ってしまう。その順序を定めるのが"1"の数字。precedenceと呼ばれる情報で、詳しくはこちらだが、数字は0,1,...,9で9が一番強い
    • なお、中置関数には、infix,infixr,infixlの３種類があり、これは無結合・右結合・左結合の３タイプを表す
infix 1 ==>
(==>) :: Bool -> Bool -> Bool
x ==> y = (not x) || y
  • Logical validity と logical equivalence
    • Logical validity
      • ある論理式がlogically validとは、引数であるBool型変数にT/Fを入れるすべてのパターンについて、結果がTになること
-- 1変数論理式の場合
myValid1 :: (Bool -> Bool) -> Bool
myValid1 bf = and [ bf p | p <- [True,False] ]

myExcluded_middle :: Bool -> Bool
myExcluded_middle p = p || not p

v1 = myValid1 myExcluded_middle

-- 2,3変数論理式の場合
myValid2 :: (Bool -> Bool -> Bool) -> Bool
myValid2 bf = and [ bf p q | p <- [True,False],
                             q <- [True,False] ]

myValid3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
myValid3 bf = and [ bf p q r | p <- [True,False],
                               q <- [True,False],
                               r <- [True,False] ]
    • Logical equivalence
      • ある二つの論理式が同数のBool型引数を取るとき、そのBool型引数のT/Fのパターンのすべての場合において、二つの論理式の値が等しいとき、その二つの論理式はequivalentと言う
      • not (P && Q) と (not P ) || (not Q) とは equivalent(ド・モルガン)
-- equiv

myLogEquiv1 :: (Bool -> Bool) -> (Bool -> Bool) -> Bool
myLogEquiv1 bf1 bf2 = and [ (bf1 p) <=> (bf2 p) | p <- [True, False]]

myLogEquiv2 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> Bool
myLogEquiv2 bf1 bf2 = and [ (bf1 p q) <=> (bf2 p q) | p <- [True, False],
                                                      q <- [True, False] ]
  • Exercise 2.9
    • lambda関数を使ってformulaを書いています
let formula3 p q = p
let formula4 p q = (p <+> q) <+> q
myLogEquiv2 formula3 formula4
  • Exercise 2.11　上からいくつか
*TAMO> myValid1 (\ p -> p ==> not (not p))
True
*TAMO> myValid1 (\ p -> (p && p) ==> p)
True
*TAMO> myValid2 (\ p q -> (p ==> q) ==> ((not p) ||q))
True
  • logical equivalenceも色々と
test1 = myLogEquiv1 id (\ p -> not (not p))
test2a = myLogEquiv1 id (\ p -> p && p)
test2b = myLogEquiv1 id (\ p -> p || p)
test3a = myLogEquiv2 (\ p q -> p ==> q) (\ p q -> not p || q)
test3b = myLogEquiv2 (\ p q -> not (p ==> q)) (\ p q -> p && not q)
test4a = myLogEquiv2 (\ p q -> not p ==> not q) (\ p q -> q ==> p)
test4b = myLogEquiv2 (\ p q -> p ==> not q) (\ p q -> q ==> not p)
test4c = myLogEquiv2 (\ p q -> not p ==> q) (\ p q -> not q ==> p)
test5a = myLogEquiv2 (\ p q -> p <=> q)
                   (\ p q -> (p ==> q) && (q ==> p))
test5b = myLogEquiv2 (\ p q -> p <=> q)
                   (\ p q -> (p && q) || (not p && not q))
test6a = myLogEquiv2 (\ p q -> p && q) (\ p q -> q && p)
test6b = myLogEquiv2 (\ p q -> p || q) (\ p q -> q || p)
test7a = myLogEquiv2 (\ p q -> not (p && q))
                   (\ p q -> not p || not q)
test7b = myLogEquiv2 (\ p q -> not (p || q))
                   (\ p q -> not p && not q)
test8a = myLogEquiv3 (\ p q r -> p && (q && r))
                   (\ p q r -> (p && q) && r)
test8b = myLogEquiv3 (\ p q r -> p || (q || r))
                   (\ p q r -> (p || q) || r)
test9a = myLogEquiv3 (\ p q r -> p && (q || r))
                   (\ p q r -> (p && q) || (p && r))
test9b = myLogEquiv3 (\ p q r -> p || (q && r))
                   (\ p q r -> (p || q) && (p || r))
  • Exercise 2.15 Propositional contradiction (論理矛盾)はすべての論理型引数の組み合わせにもFalseを返すような論理式。それかどうかのテスト関数は…(たぶん)
-- Propositional contradiction

-- 1変数論理式の場合
myContra1 :: (Bool -> Bool) -> Bool
myContra1 bf =and [ not (bf p) | p <- [True,False] ]

-- myValid1 myExcluded_middle

-- 2,3変数論理式の場合
myContra2 :: (Bool -> Bool -> Bool) -> Bool
myContra2 bf = and [ not (bf p q) | p <- [True,False],
                             q <- [True,False] ]

myContra3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
myContra3 bf = and [ not (bf p q r) | p <- [True,False],
                               q <- [True,False],
                               r <- [True,False] ]
  • Exercise 2.20はこんな風にやればよい？
myF1 p q = (not p ==> q) && ( p ==> (not q))
myF2 p q = (not p ==> q ) && ( q ==> (not p))
myF3 p q = (not p ==> q ) && ((not q) ==> p)
myF4 p q r = (p ==> (q ==> r)) && (q ==> (p ==> r))
myF5 p q r = (p ==> (q ==> r)) && ((p ==> q) ==> r)
myF6 p q r = ((p ==> q) ==> p ) && p
myF7 p q r = ((p || q) ==> r ) && ((p ==> r) && (q ==> r))

myF2list = [myF1, myF2,myF3]
myF3list = [myF4,myF5,myF6,myF7]

-- [myLogEquiv2 f1 f2 | f1 <- myF2list,f2 <- myF2list ]
-- [myLogEquiv3 f1 f2 | f1 <- myF3list,f2 <- myF3list ]
  • ここまでは論理。ここからはそれの数学への活用
  • 『ある自然数が』とか、『すべての自然数が』とかいうときに使う\forall,\existsはquantifiersと呼ぶが、それを使って数学的な内容を述べることを扱うことにする
  • 集合の扱いに二通りあって…
[x | x <- [51,53,..99]]
[x | x <- [1..1000],rem x 2 == 1, x> 50, x < 100]
[n | n <- [1..],(n < 1) && (ld(n) ==n)] -- 素数の定義
  • ラムダ関数が\forall,\existsを扱うときに、役に立つらしきことが書かれている
    • 以下のように２通りの書き方があるが、後者(ラムダ関数を使っている)の方は、mySq2に"x"を渡さずに、mySq2をラムダ関数である、として定義している。この「"x"をラムダに持たせて、『表に出さない』」ことにして、そのうえで、そんな影の"x"の『すべてが』とか『すくなくとも１つが』という考え方を\forall,\exsitsと対応付ける」という考え方らしい
mySq1 :: Integer -> Integer
mySq1 x = x^2

mySq2 :: Integer -> Integer
mySq2 = \ x -> x^2
  • Haskellで論理quantifiersを使おうと思ったら、any,all,some everyがある
  • まとめ、以下のファイルはTAMO.hs
module TAMO
where

import GS -- GSモジュールのld関数を使いたいから

infix 1 ==>
(==>) :: Bool -> Bool -> Bool
x ==> y = (not x) || y

infix 1 <=>

(<=>) :: Bool -> Bool -> Bool
x <=> y = x == y

infixr 2 <+>

(<+>) :: Bool -> Bool -> Bool
x <+> y = x /= y

-- これはBoolな値を出させる
p = True
q = False 
formula1 = (not p) && (p ==> q) <=> not (q && (not p))

-- これは、２つのブール引数を取ってブール値を返す関数の定義

formula2 p q = ((not p) && (p ==> q) <=> not (q && not p))

tabnot = [ not x | x <- [True,False] ]
taband = [ x && y | x <- [True,False], y <- [True,False] ]
tabor = [ x || y | x <- [True,False], y <- [True,False] ]
tabiff = [ x <=> y | x <- [True,False], y <- [True,False] ]
tabifthen = [ x ==> y | x <- [True,False], y <- [True,False] ]
tabxor = [ x <+> y | x <- [True,False], y <- [True,False] ]

-- validity

-- 1変数論理式の場合
myValid1 :: (Bool -> Bool) -> Bool
myValid1 bf = and [ bf p | p <- [True,False] ]

myExcluded_middle :: Bool -> Bool
myExcluded_middle p = p || not p

-- myValid1 myExcluded_middle

-- 2,3変数論理式の場合
myValid2 :: (Bool -> Bool -> Bool) -> Bool
myValid2 bf = and [ bf p q | p <- [True,False],
                             q <- [True,False] ]

myValid3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
myValid3 bf = and [ bf p q r | p <- [True,False],
                               q <- [True,False],
                               r <- [True,False] ]

-- equiv

myLogEquiv1 :: (Bool -> Bool) -> (Bool -> Bool) -> Bool
myLogEquiv1 bf1 bf2 = and [ (bf1 p) <=> (bf2 p) | p <- [True, False]]

myLogEquiv2 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> Bool
myLogEquiv2 bf1 bf2 = and [ (bf1 p q) <=> (bf2 p q) | p <- [True, False],
                                                      q <- [True, False] ]
myLogEquiv3 :: (Bool -> Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool -> Bool) -> Bool
myLogEquiv3 bf1 bf2 = and [ (bf1 p q r) <=> (bf2 p q r) | p <- [True, False],
                                                          q <- [True, False],
                                                          r <- [True, False] ]

formula3 p q = p
formula4 p q = (p <+> q) <+> q

-- myLogEquiv2 formula3 formula4

test1 = myLogEquiv1 id (\ p -> not (not p))
test2a = myLogEquiv1 id (\ p -> p && p)
test2b = myLogEquiv1 id (\ p -> p || p)
test3a = myLogEquiv2 (\ p q -> p ==> q) (\ p q -> not p || q)
test3b = myLogEquiv2 (\ p q -> not (p ==> q)) (\ p q -> p && not q)
test4a = myLogEquiv2 (\ p q -> not p ==> not q) (\ p q -> q ==> p)
test4b = myLogEquiv2 (\ p q -> p ==> not q) (\ p q -> q ==> not p)
test4c = myLogEquiv2 (\ p q -> not p ==> q) (\ p q -> not q ==> p)
test5a = myLogEquiv2 (\ p q -> p <=> q)
                   (\ p q -> (p ==> q) && (q ==> p))
test5b = myLogEquiv2 (\ p q -> p <=> q)
                   (\ p q -> (p && q) || (not p && not q))
test6a = myLogEquiv2 (\ p q -> p && q) (\ p q -> q && p)
test6b = myLogEquiv2 (\ p q -> p || q) (\ p q -> q || p)
test7a = myLogEquiv2 (\ p q -> not (p && q))
                   (\ p q -> not p || not q)
test7b = myLogEquiv2 (\ p q -> not (p || q))
                   (\ p q -> not p && not q)
test8a = myLogEquiv3 (\ p q r -> p && (q && r))
                   (\ p q r -> (p && q) && r)
test8b = myLogEquiv3 (\ p q r -> p || (q || r))
                   (\ p q r -> (p || q) || r)
test9a = myLogEquiv3 (\ p q r -> p && (q || r))
                   (\ p q r -> (p && q) || (p && r))
test9b = myLogEquiv3 (\ p q r -> p || (q && r))
                   (\ p q r -> (p || q) && (p || r))

-- Propositional contradiction

-- 1変数論理式の場合
myContra1 :: (Bool -> Bool) -> Bool
myContra1 bf =and [ not (bf p) | p <- [True,False] ]

-- myValid1 myExcluded_middle

-- 2,3変数論理式の場合
myContra2 :: (Bool -> Bool -> Bool) -> Bool
myContra2 bf = and [ not (bf p q) | p <- [True,False],
                             q <- [True,False] ]

myContra3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
myContra3 bf = and [ not (bf p q r) | p <- [True,False],
                               q <- [True,False],
                               r <- [True,False] ]

myF1 p q = (not p ==> q) && ( p ==> (not q))
myF2 p q = (not p ==> q ) && ( q ==> (not p))
myF3 p q = (not p ==> q ) && ((not q) ==> p)
myF4 p q r = (p ==> (q ==> r)) && (q ==> (p ==> r))
myF5 p q r = (p ==> (q ==> r)) && ((p ==> q) ==> r)
myF6 p q r = ((p ==> q) ==> p ) && p
myF7 p q r = ((p || q) ==> r ) && ((p ==> r) && (q ==> r))

myF2list = [myF1, myF2,myF3]
myF3list = [myF4,myF5,myF6,myF7]

-- [myLogEquiv2 f1 f2 | f1 <- myF2list,f2 <- myF2list ]
-- [myLogEquiv3 f1 f2 | f1 <- myF3list,f2 <- myF3list ]