tnomuraのブログ

手続き型言語風の Haskell プログラム

手続き型言語のプログラム風に見える Haskell プログラムを書いてみた。簡単な統計量を計算するプログラムだ。（行頭のアンダースコアはスペースに置き換える。）順次実行するようなアルゴリズムは、IOモナドでない純粋関数のプログラムでも let ~ in 文を利用するとそれらしく書くことができる。

手続き型プログラム言語風のプログラムを書くということは、プログラムの文が順次実行されることが期待されることを示しており、見た目だけでなくアルゴリズム的にも意味がある。

なんということはないプログラムだが、これを知らないと Haskell を道具として使えないという小ネタがいっぱい詰まっている。

module Statistics where

data Stat = Stat {n :: Int, mean :: Double, var :: Double, sd :: Double}
__ deriving Show

statistics xs =
__ let
____ n = length xs
____ mean = (sum xs) / fromIntegral n
____ var = (sum $ map (\x -> (x - mean) * (x - mean)) xs) / fromIntegral n
____ sd = sqrt var
__ in
____ Stat n mean var sd

main = do
__ putStr "input file name: "
__ fname <- getLine
__ contents <- readFile fname
__ let rawdata = map (read :: String -> Double) $ lines contents
__ let result = statistics rawdata
__ putStrLn $ show (n result)
__ putStrLn $ show (mean result)
__ putStrLn $ show (var result)
__ putStrLn $ show (sd result)

実行例

$ runhaskell statistics.hs
input file name: data
3
2.0
0.6666666666666666
0.816496580927726

アキュームレータと畳込み

手続き型のプログラムではループの中に途中経過を保持する変数（アキュームレータ）を使うことが多い。例えば数列の総和を求めるプログラムは次のようになる。

irb(main):001:0> begin
irb(main):002:1> total = 0
irb(main):003:1> for i in 1..10
irb(main):004:2> total += i
irb(main):005:2> end
irb(main):006:1> puts total
irb(main):007:1> end
55

上のプログラムの for ループのなかで、総和の途中経過を保持する変数 total がアキュームレータだ。しかし、Haskell ではこのような再代入の方法はないので、別の方法を考えないといけない。一般的には次のようにリストの総和を求める関数を再帰的に定義する。

Prelude> {total [] = 0; total (x:xs) = x + total xs}
Prelude> total [1..10]
55

また、foldr や foldl のような畳込み関数を利用すると、擬似的なアキュームレータを記述することができる。それを示す前にまず foldr などの畳込みがどのように実行されるかを見てみる。

Prelude> foldr (\x y -> "(" ++ show x ++ "+" ++ y ++ ")") "0" [1..10]
"(1+(2+(3+(4+(5+(6+(7+(8+(9+(10+0))))))))))"
Prelude> foldl (\x y -> "(" ++ x ++ "+" ++ show y ++ ")") "0" [1..10]
"((((((((((0+1)+2)+3)+4)+5)+6)+7)+8)+9)+10)"

アキュームレータはなく、リストのデータがスタックに保存されていって展開の最後に計算されることがわかる。これをよく見ると foldl の x が手続き型のプログラムのアキュームレータ total の役割に近いことがわかる。そこでやってみた。

Prelude> foldl (\total x -> total + x) 0 [1..10]
55

ラムダ記法の本体の total + x のところが for ループの total = total + i に対応しているのがわかる。手続き型のプログラムのループの部分はこのように foldl で置き換えることができるかどうかを考えてみるのもいいかもしれない。たとえば、リストの要素の２乗和をとる計算は次のようになる。

Prelude> foldl (\total x -> total + x*x) 0 [1..10]
385

しかし、これは次のようなプログラムのほうが可読性が高い。

Prelude> sum [x*x| x <- [1..10]]
385

アキュームレータにこだわらずに計算の意味を考えた翻訳のほうも考える必要があるだろう。

追記

数値リストの総和と2乗和を同時に計算するプログラムを考えてみた。アキュームレータを意識したプログラムは次のようになる。

Prelude> foldl (\total x -> (fst total + x, snd total + x*x)) (0,0) [1..10]
(55,385)

アキュームレータを使わない場合は次のようになる。

Prelude> foldl (\x y -> (fst x + fst y, snd x + snd y)) (0,0) [(x,x*x)| x <- [1..10]]
(55,385)

アキュームレータを想定したほうが簡潔？

mapM_ で IO モナドに for 文を作る

map 関数で多重ループを作って遊んでいるうちに、mapM_ 関数を使えば擬似的な for ループを IO モナドに書けるのではないかと思いついた。そこで、まず星印を並べて印刷するプログラムを書いてみた。

Prelude> mapM_ (\x-> putStr "*") [1..5]
*****Prelude>

文字列の最後を改行するには do ブロックを使えばいい。

Prelude> do {mapM_ (\x-> putStr "*") [1..5]; putStrLn ""}
*****
Prelude>

このループの外側にもうひとつループを作ってみた。

Prelude> mapM_ (\x-> do {mapM_ (\y-> putStr "*") [1..5]; putStrLn ""}) [1..5]
*****
*****
*****
*****
*****

パラメータの y を x と連動させてみた。

Prelude> mapM_ (\x-> do {mapM_ (\y-> putStr "*") [1..x]; putStrLn ""}) [1..5]
*
**
***
****
*****

for 文らしく見えるように example.hs というファイルを作って整形してみた。(行頭のアンダースコアはスペースに読み替える。）

example =
__mapM_ (\x-> do
____mapM_ (\y-> do
______putStr "*"
______putStr (show y)
______) [1..x]
____putStrLn ""
__) [1..5]

実行例：

Prelude> :l example
[1 of 1] Compiling Main ( example.hs, interpreted )
Ok, modules loaded: Main.
*Main> example
*1
*1*2
*1*2*3
*1*2*3*4
*1*2*3*4*5

特に問題なく IO モナドで mapM_ を利用した for 文が書けるような気がする。

map による多重ループ

map 関数による多重ループを考えてみたが、単純に入れ子にしたら、リストのリストができてしまった。

Prelude> map (\x-> (map (\y -> (x,y)) ["a","b","c"])) [1,2,3]
[[(1,"a"),(1,"b"),(1,"c")],[(2,"a"),(2,"b"),(2,"c")],[(3,"a"),(3,"b"),(3,"c")]]

そこで、外側のループに map ではなく、concatMap を使ったらうまくいった。外側のループのパラメータで内部のループをコントロールすることもできた。

Prelude> concatMap (\x-> (map (\y-> (x,y)) ["a","b","c"])) [1,2,3]
[(1,"a"),(1,"b"),(1,"c"),(2,"a"),(2,"b"),(2,"c"),(3,"a"),(3,"b"),(3,"c")]

Prelude> concatMap (\x-> (map (\y-> (x,y)) [1..x])) [1,2,3]

[(1,1),(2,1),(2,2),(3,1),(3,2),(3,3)]

concatMap を繋げることで、３重ループも作れる。

Prelude> concatMap (\x-> (concatMap (\y-> (map (\z-> (x,y,z)) [1,2])) [1,2])) [1,2]
[(1,1,1),(1,1,2),(1,2,1),(1,2,2),(2,1,1),(2,1,2),(2,2,1),(2,2,2)]

星印の３角形も作れた。

Prelude> map (\x-> map (\y-> '*') [1..x]) [1..5]
["*","**","***","****","*****"]

リスト内包表記で書けるプログラムは、map の多重ループでも書けるようだ。ガード付きのプログラムは次のように書ける。

Prelude> [x*x| x <- [1..10], odd x]
[1,9,25,49,81]

Prelude> map (\x -> x*x) $ filter odd [1..10]
[1,9,25,49,81]

リスト内包表記は map あるいはリストモナドのシンタックスシュガーであることがわかるが、可読性や簡潔性が利点だ。

IOモナドの再帰

IOモナドの再帰関数を書くときの注意点は次の２つだ。

１．関数の値は必ず return で返す。

２．関数の値をとりだして加工するときは do 記法の中で <- 記法を使って IO モナドのコンテナの中の生データを取り出す。

IOモナドの関数を手続き型言語のアナロジーで書いて、訳の分からないエラーに泣いた人は多いと思うが、IOモナドの戻り地は必ず IO a 型のデータにカプセル化されていなければならないことを押さえておけばそう難しくはない。IOモナドの関数で値を返すときは必ず、次のように return 関数で値をカプセル化する必要がある。

return 10

次に、IOモナド型の関数の値を利用するときは、カプセル化された IO a 型のデータから do 構文の <- 記法を使って取り出さなければならない。例えば、IOモナドの関数が foo で IO a 型のデータを戻す場合、次のようにして IO a のカプセルから生データの a を取り出さなければならない。

do { x <- foo; ... }

つまり、IOモナドの関数を書くときは、いつも関数の戻り値が IO a 型にカプセル化されていることを意識しておく必要がある。

それでは実際の例を見てみよう。次のプログラム fact n は IOモナド型の関数だ。

Prelude> {fact 0 = return 1; fact n = do {x <- fact (n-1); return (n * x)}}
Prelude> fact 5
120

fact 0 は IO 1 をデータとして返す。fact n は fact (n-1) のデータを <- 記法で取り出し、n と掛けて retrun 関数で IO a 型の値にして返している。上の２つの原理に従っていることがわかる。

普通に fact 0 = 1; fact n = n * fact (n-1) と純粋関数で書いたほうが分かりやすいが、IOモナド版の fact の方は次のように、途中経過を print 文で表示して print デバッグをすることができる。

Prelude> {fact 0 = return 1; fact n = do {print n; x <- fact (n-1); return (n * x)}}
Prelude> fact 5
5
4
3
2
1
120

IOモナドの再帰関数についてはこのブログの 2011 年の記事に書いていた。同じところをぐるぐる巡っているが、あちこち浮気をして彷徨うからこんなことになる。

IOモナドの再帰関数の注意点

IOモナドと末尾再帰の相性がいい

入れ子の内包表記

内包表記は基本的には map 関数と同じだ。次のプログラムはリストの要素の２乗の要素からなるリストを作成する。

Prelude> [x*x| x <- [1..5]]
[1,4,9,16,25]

しかし、コンマ区切りを使うことによって、ループを入れ子にすることができる。

Prelude> [(x,y)| x <- [1,2,3], y <- ["a", "b", "c"]]
[(1,"a"),(1,"b"),(1,"c"),(2,"a"),(2,"b"),(2,"c"),(3,"a"),(3,"b"),(3,"c")]

また、外側のループのパラメータで内側のループの動作を制御することもできる。

Prelude> [(x,y)| x <- [1..3], y <- [1..x]]
[(1,1),(2,1),(2,2),(3,1),(3,2),(3,3)]

ただ、手続き型プログラムの多重ループのテストでよくやるような '*' を三角形にプリントするようなプログラムは、上の方法では難しい。しかし、これも内包表記自体をループさせることで実現できる。

Prelude> [['*'| _ <- [1..x]]| x <- [1..3]]
["*","**","***"]
Prelude> mapM_ putStrLn [['*'| _ <- [1..x]]| x <- [1..3]]
*
**
***

入れ子になったリストの内包表記はリストモナドの do 記法を使って記述することもできる。

Prelude> do {x <- [1,2,3]; y <- ["a","b","c"]; [(x,y)]}
[(1,"a"),(1,"b"),(1,"c"),(2,"a"),(2,"b"),(2,"c"),(3,"a"),(3,"b"),(3,"c")]

Prelude> do {x <- [1,2,3]; y <- [1..x]; [(x,y)]}
[(1,1),(2,1),(2,2),(3,1),(3,2),(3,3)]

Prelude> do {x <- [1,2,3]; [do {_ <- [1..x];['*']}]}
["*","**","***"]

これらのトリックを使えば、手続き型言語の多重ループを Haskell に移植するのも楽にできるかもしれない。

パラメータが２つの再帰

多分岐の再帰関数は内包記法を使うと簡単に書ける。順列を列挙するプログラムを再掲すると次のようになる。

Prelude> {perm [] = [[]]; perm xs = [x:y| x <- xs, y <- perm (filter (/=x) xs)]}
Prelude> perm [1,2,3]
[[1,2,3],[1,3,2],[2,1,3],[2,3,1],[3,1,2],[3,2,1]]

上のは全ての要素からなる順列を作ったが、順列の要素の数を制限するプログラムが必要になることがある。これは、prem 関数が取り出す順列数 n と元になる要素の集合 xs の２つのパラメータを持つようにすればよい。つまり perm n xs という形になる。

このようなパラメータが２つある再帰関数の場合は、base case が２つになる。つまり、perm 0 xs の場合と、perm n [] の２つの場合だ。面倒なようだが、上の順列プログラムに取り出す要素数 n というパラメータを追加し、perm 0 xs と perm n [] という２つの base case を定義するだけで、取り出す要素数を指定できる perm 関数に改造することができる。

Prelude> {perm 0 _ = [[]]; perm _ [] = []; perm n xs = [x:y | x <- xs, y <- perm (n-1) (filter (/=x) xs)]}
Prelude> perm 2 [1,2,3,4]
[[1,2],[1,3],[1,4],[2,1],[2,3],[2,4],[3,1],[3,2],[3,4],[4,1],[4,2],[4,3]]

このような base case が２つになる再帰のパターンを理解すれば、組み合わせを列挙する次のプログラムも簡単に書ける。

Prelude> {comb 0 _ = [[]]; comb _ [] = []; comb n (x:xs) = map (x:) (comb (n-1) xs) ++ comb n xs}
Prelude> comb 2 [1,2,3]
[[1,2],[1,3],[2,3]]

また、集合の冪集合を作るプログラムも comb 関数の類推から次のように作ることができる。

Prelude> {pow [] = [[]]; pow (x:xs) = map (x:) (pow xs) ++ pow xs}
Prelude> pow [1,2,3]
[[1,2,3],[1,2],[1,3],[1],[2,3],[2],[3],[]]

順列、組み合わせ、冪集合は Haskell で集合を扱うときに必須の関数となるから、これが空で作れるということには重要な意味がある。

分岐する再帰

Haskellではループは再帰関数で記述しないといけない。最初は戸惑うが、分岐しない再帰関数はすぐに空で書けるようになる。例えば、階乗を計算するプログラムは分岐しない再帰関数なので次のようになる。

Prelude> {fact 0 = 1; fact n = n * fact (n-1)}
Prelude> fact 5
120

引数がリストの場合も分岐しない再帰関数は簡単だ。次のプログラムはリストの要素の総和を計算する。

Prelude> {mysum [] = 0; mysum (x:xs) = x + mysum xs}
Prelude> mysum [1..10]
55

しかし、クイックソートの時は、選択した要素について、右にそれより小さい要素、左にそれより大きい要素を集めてそれについて再帰しないといけないので、再帰が左と右の2方向におきる。つまり、2分岐の再帰になる。

Prelude> {qsort [] = []; qsort (x:xs) = qsort (filter (<=x) xs) ++ [x] ++ qsort (filter (>x) xs)}
Prelude> qsort [2,9,7,5]
[2,5,7,9]

分岐がない場合に比べてやや複雑になるが、選択した要素の左側と右側に再帰を並べると考えると理解しやすい。ソートしたいリストの先頭の要素を取りだしたら、その左側にはその要素以下の要素のリストの qsort を、その右側にはその要素より大きい要素のリストの qsort の結果をつなぐだけだ。

しかし、リストの順列を全て列挙するプログラムの場合は、多分岐になるのでイメージが作りづらい。しかし、これも内包表記を利用すると呆れるほど簡単に書けることが分かる。

Prelude> {perm [] = [[]]; perm (xs) = [(x:y) | x <- xs, y <- perm (filter (/=x) xs)]}
Prelude> perm [1,2,3]
[[1,2,3],[1,3,2],[2,1,3],[2,3,1],[3,1,2],[3,2,1]]

内包表記の x <- xs はリスト xs の全ての要素を順に取り出す。また、y <- prem (filter (/=x) xs) では xs から x を取り除いたリストの順列から、その要素の一つ（リスト）を取り出し、x をそれらをのリストと連結したリストのリストを返す。コンマの後の y は x のループの入れ子になっているから、このコードは上手く動作する。

内包表記は Python にもあるので、順列のプログラムは Python でも動作するはずだ。内包表記を利用すれば他の多分岐の再帰関数も楽に書けるのではないだろうか。

述語論理と型付きλ記法

述語論理のモデルの領域を集合 D とする。また、領域 D の冪集合を D* とする。領域 D のアリティ１の述語 P(x) のうち同じ真理集合 {x ∈ D | P(x)} を持つものどうしには同値関係がある。そこで、D* の要素 A が A = {x ∈ D | P(x)}のとき、P(x) = (x ∈ A) を考えると、これは真理集合が A である述語の同値類の代表元になる。

このとき、P(x) の論理演算と D* の要素の集合演算は同型であるから、P(x) の集合と D* は同型である。つまり、述語論理の論理演算は全て、領域 D の冪集合の集合演算と対応している。また、領域 D* の集合演算は領域 D* で閉じている。したがって、領域 Dとこのような述語 P(x) からなる述語論理のモデルは述語論理を充足している。

同様に、アリティ２の述語 P(x, y) は、領域 D の直積 D × D とその冪集合 (D × D)* を考えたとき、

P(x, y) = (x, y) ∈ A　ただし、A ∈ (D × D)*

によって領域 D の全てのアリティ２の述語を記述することができる。これもまた、述語論理のモデルとして述語論理を充足している。そうして、この述語 P(x, y) は型付きラムダ記法で記述された関数 P(x,y) :: D × D -> {True, False} に対応している。

言葉足らずになってしまったが、言いたいことは、領域 D があったとき、これに関する型付きラムダ記法によるプログラムは述語論理を充足しているのではないかということだ。述語論理で証明できる数学の定理は全て型付きラムダ記法のプログラムで記述して実験できるかもしれない。

要するに、述語論理的に正しいことは、すべて、型付けられた関数型プログラム言語のプログラムとして調べることができるのではないかということだ。ある数学的な定理が正しいかどうかは、型付き関数型プログラム言語のプログラムで検証できるのではないかという気がする。

上に述べたことが本当に適切かどうかはわからないが、型付き関数言語がかなり数学的な問題についても親和性が高いのではないかという気がする。数学的な理論のモデルを型付き関数言語で記述しながら学習していくという方法もとれるかもしれない。抽象的な数学の理論を具体的なプログラム例として捉えることができたら、随分学習が楽になるのではないだろうか。

ところで、ラッセルのパラドックスの記事は、これで一旦終了したい。何年間かこの問題に素人の立場として取り組んできたのは、集合の学習の最初にラッセルのパラドックスに出会って非常に戸惑ったことがあったからだ。そこで、ラッセルのパラドックスに悩まされないで、集合や論理学を理解できないだろうかと思っていろいろと考えてみた。数学の専門家ではないので、逆に専門家が当たり前として通過するところをいろいろ考えてみたつもりだ。

結論としては述語論理の領域を「自分自身を要素としては含まない集合」にとり、内包記法で集合を定義するときに { x ∈ D | P(x) } という型付き関数 P(x) :: D -> {True, Fasle} を使用すれば、論理学や集合に矛盾はおきないことがわかった（と思う）。確証はできないが、Haskell のような関数型プログラム言語は述語論理のモデルとして使えるような気がするところまできた。

論理学の深いところまで知りたいわけではなく、論理学をどう効率的にいろいろな分野、特に数学の学習に利用できないかというのが目的だったので、これからは、Haskell という関数型プログラム言語の利用法について重点的に色々やってみたい。

公理的集合論の集合とはどんな集合？

公理的集合論の集合は、公理をもとに集合と定義できるものを演繹していく考え方だ。公理はプログラム言語の文法規則に当たる。プログラム言語ではどのような記号の配列が式であるかを文法規則で判断する。文字列をパーサーに通すことによって、機械的に再帰的に解析され、その文字列がプログラムかどうかが判別される。同様に、公理的集合論においても、ある対象が集合かどうかは再帰的に公理の規則に帰着できるかどうかで判断される。

プログラム言語の再帰的定義の場合、base case がないと、解析が終わらない。公理的集合論の場合はそれは空集合ひとつだけだ。公理的集合論の集合は再帰的に解析していくと最終的には空集合になる。これは、自分自身を要素として含む集合とは性質が異なる。自分自身を要素として含む集合は再帰的な解析が無限に続くため base case に帰着することはないからだ。

したがって、公理的集合論の集合は、自分自身を要素としては含まない集合だ。これは、素朴集合論の場合でも述語論理を充足する。

公理的集合論の集合が述語論理と矛盾しないのはそのためかもしれない。