圏論勉強会 @ ワークスアプリケーションズ#8 http://nineties.github.io/category-seminar/8.html#/55 練習問題 回答

banana.sml

(**
 * 圏論勉強会 @ ワークスアプリケーションズ#8
 *   http://nineties.github.io/category-seminar/8.html#/55
 * 練習問題 回答
 *
 * 実行方法(for SML/NJ)
 *   $ cat banana.cm
 *     group
 *     is
 *       $/basis.cm
 *     	$/smlunitlib.cm
 *     	banana.sml
 *   $ sml
 *   CM.make "banana.cm";
 *   -
 *)

structure CategoryTheory =
struct
local
  open SMLUnit
  open Assert
  val ($,&,%) = (Test.TestLabel,Test.TestList,Test.TestCase)
in

fun id x = x

(**
 * banana-split law
 * http://nineties.github.io/category-seminar/8.html#/27
 *)
fun sum xs = foldr (fn (a,x)=> a+x) 0 xs
fun length xs = foldr (fn (_,x)=> x+1) 0 xs

fun average  ls = real (sum ls) / real (length ls)
fun average' ls = let
  val (s,a) = foldr (fn (a,(x,y))=> (a+x, y+1)) (0,0) ls
in real s / real a
end

(**
 * Fokkingaの相互再帰定理
 *
 * 練習問題
 * http://nineties.github.io/category-seminar/8.html#/35
 *
 *)

(* steepのナイーブな実装 *)
fun steep [] = true
  | steep (x::xs) = x > sum xs andalso steep xs

(* 相互再帰定理を適用したsteepの効率的な実装 *)
local
  val c = (true, 0)
  fun f (a, (b,s)) = (a > s andalso b, a + s)
in
  val steep' = #1 o foldr f c
end

(**
 * 二分木が平衡状態であるという事を,各節点で
 * 3(m+1)≧n+1 かつ 3(n+1)≧m+1
 * が成り立つ事とします。(n,mは左右の部分木の節点数)
 * 二分木が平衡状態か否かを判定する関数を相互再帰定理に基いて導出して下さい。
 * 
 * [追記]この条件式は以下の論文の共著者である山本さんの提案を受けて,講義当日に提示した1/3≦n/(n+m+1)≦2/3から変更しました。 
 *)

datatype 'a tree = Leaf | Node of 'a tree * 'a tree

fun count Leaf = 1
  | count (Node(l,r)) = count l + count r

val _ =
  let
    val test =
      $ ("count tree"
        , &[ % (fn()=> assertEqualInt 1 (count Leaf))
           , % (fn()=> assertEqualInt 2 (count (Node(Leaf,Leaf))))
           , % (fn()=> assertEqualInt 3 (count (Node(Leaf,Node(Leaf,Leaf)))))
           ])
  in
    TextUITestRunner.runTest {output=TextIO.stdOut} test
  end


(* 平衡状態を判定するナイーブな関数 *)
fun is_balanced Leaf = true
  | is_balanced (Node(l,r)) =
    let val (m,n) = (count l, count r)
    in
      3 * (m + 1) >= n + 1 andalso 3 * (n + 1) >= m + 1
      andalso is_balanced l
      andalso is_balanced r
    end

(* treeのfold *)
fun foldTree f e Leaf = e
  | foldTree f e (Node(l,r)) = f (foldTree f e l) (foldTree f e r)


(* 効率的な平衡状態判定 *)
local
  val cd = (true, 1)
  fun f (lb,m) (rb,n)  = (3 * (m + 1) >= n + 1 andalso
                          3 * (n + 1) >= m + 1 andalso
                          lb andalso rb
                         , m + n (* g' *)
                         )
in
  val is_balanced' = #1 o foldTree f cd
end

(* is_balanced のテスト *)
val _ =
  let
    val assert = assertEqualBool
    val test =
      $ ("is_balanced tree"
        , &[ % (fn()=> assert (is_balanced Leaf) (is_balanced' Leaf))
           , % (fn()=> assert (is_balanced (Node(Leaf,Leaf))) (is_balanced' (Node(Leaf,Leaf))))
           , % (fn()=> assert (is_balanced  (Node(Node(Leaf,Leaf),Leaf)))
                              (is_balanced' (Node(Node(Leaf,Leaf),Leaf))))
           , % (fn()=> assert (is_balanced  (Node(Node(Node(Leaf,Leaf),Leaf),Leaf)))
                              (is_balanced' (Node(Node(Node(Leaf,Leaf),Leaf),Leaf))))
           , % (fn()=> assert (is_balanced  (Node(Node(Node(Node(Node(Node(Leaf
                                                                          ,Leaf)
                                                                     ,Leaf)
                                                                ,Leaf)
                                                           ,Leaf)
                                                      ,Leaf)
                                                 ,Leaf)))
                              (is_balanced' (Node(Node(Node(Node(Node(Node(Leaf
                                                                          ,Leaf)
                                                                     ,Leaf)
                                                                ,Leaf)
                                                           ,Leaf)
                                                      ,Leaf)
                                                 ,Leaf))))
           ])
  in
    TextUITestRunner.runTest {output=TextIO.stdOut} test
  end


(**
 * sectionはcatamorphism
 *
 * http://nineties.github.io/category-seminar/8.html#/37
 *)

(* cons 0 を fold で実装する例 *)
fun cons x xs = x :: xs

val cons0 = cons 0

local
  val c = [0]
  fun f (a,x) = 0::a::tl x
in
  val cons0' = foldr f c
end

(**
 * 練習問題
 * http://nineties.github.io/category-seminar/8.html#/38
 * 
 * 階乗関数
 *     fact(n)=n!
 * を自然数型についてのcatamorphismを用いて
 *     fact=π1∘(|f|)
 * の形に書いて下さい。
 *)

fun fact 0 = 1
  | fact n = n * fact (n-1)

fun foldN f e 0 = e
  | foldN f e n = f (foldN f e (n-1))

local
  val c = (1,0)
  fun f (x,n) = (fact (1+n), id (1+n))
in
  val fact' = #1 o foldN f c
end

(* fact' のテスト *)
val _ =
  let
    val assert = assertEqualInt
    val test =
      $ ("fact"
        , &[ % (fn()=> assert (fact  0) (fact'  0))
           , % (fn()=> assert (fact  1) (fact'  1))
           , % (fn()=> assert (fact  2) (fact'  2))
           , % (fn()=> assert (fact  3) (fact'  3))
           , % (fn()=> assert (fact  4) (fact'  4))
           , % (fn()=> assert (fact  5) (fact'  5))
           , % (fn()=> assert (fact  6) (fact'  6))
           , % (fn()=> assert (fact  7) (fact'  7))
           , % (fn()=> assert (fact  8) (fact'  8))
           , % (fn()=> assert (fact  9) (fact'  9))
           , % (fn()=> assert (fact 10) (fact' 10))
           , % (fn()=> assert (fact 11) (fact' 11))
           , % (fn()=> assert (fact 12) (fact' 12))
           (* overflow *)
           (* , % (fn()=> assert (fact 13) (fact' 13)) *)
           ])
  in
    TextUITestRunner.runTest {output=TextIO.stdOut} test
  end


(**
 * 練習問題
 * http://nineties.github.io/category-seminar/8.html#/54
 * 
 *  自然数型,リスト型,二分木などのhylomorphismを導出して下さい。
 *  一旦リスト[n,n−1,n−2,⋯,1]を生成して,要素の積を掛ける事でfact(n)を計算出来ます。 この方法でfactをcatamorphismとanamorphismの合成,hylomorphismの2通りの方法で実装してみて下さい。
 *)
fun unfoldr p e =
  case p e
    of SOME (x,xs) => x::unfoldr p xs
     | NONE => nil

fun hyloL (pl,pr) f e =
  case f e
    of NONE => pl
     | SOME (x,x') => pr (x, hyloL (pl,pr) f x')

(* catamorphism と anamorphism の合成で構成する fact *)
fun fact_cata_ana n =
  let
    val ana  = unfoldr (fn 0=> NONE
                         | n=> SOME(n,n-1))
    val cata = foldr op* 1
  in
    (cata o ana) n
  end

(* hylomorphism で実装する fact *)
fun fact_hylo n =
  hyloL (1,op* ) (fn 0=> NONE
                   | s=> SOME(s,s-1)) n


(* hylomorphism で定義した fact のテスト *)
val _ =
  let
    val assert = assertEqualInt
    val test =
      $ ("fact"
        , &[ % (fn()=> assert (fact_cata_ana  0) (fact_hylo  0))
           , % (fn()=> assert (fact_cata_ana  1) (fact_hylo  1))
           , % (fn()=> assert (fact_cata_ana  2) (fact_hylo  2))
           , % (fn()=> assert (fact_cata_ana  3) (fact_hylo  3))
           , % (fn()=> assert (fact_cata_ana  4) (fact_hylo  4))
           , % (fn()=> assert (fact_cata_ana  5) (fact_hylo  5))
           , % (fn()=> assert (fact_cata_ana  6) (fact_hylo  6))
           , % (fn()=> assert (fact_cata_ana  7) (fact_hylo  7))
           , % (fn()=> assert (fact_cata_ana  8) (fact_hylo  8))
           , % (fn()=> assert (fact_cata_ana  9) (fact_hylo  9))
           , % (fn()=> assert (fact_cata_ana 10) (fact_hylo 10))
           , % (fn()=> assert (fact_cata_ana 11) (fact_hylo 11))
           , % (fn()=> assert (fact_cata_ana 12) (fact_hylo 12))
           (* overflow *)
           (* , % (fn()=> assert (fact 13) (fact' 13)) *)
           ])
  in
    TextUITestRunner.runTest {output=TextIO.stdOut} test
  end

end (* local *)
end (* structure CategoryTheory *)
structure Cat = CategoryTheory