Last active
December 19, 2015 14:39
-
-
Save eldesh/5970931 to your computer and use it in GitHub Desktop.
圏論勉強会 @ ワークスアプリケーションズ#8 http://nineties.github.io/category-seminar/8.html#/55
練習問題 回答
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** | |
* 圏論勉強会 @ ワークスアプリケーションズ#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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment