O28

Size: px

Start display at page:

Download "O28"

きよあつふじがわ
4 years ago
Views:

1 ループ書いたら負けかなと思っている uskz

2 自己紹介梶本裕介 25 歳

3 ループ嫌い抽象度が低すぎる accumulate? transform? 範囲とかいちいち気にしないといけないのが嫌形式的な扱いが面倒くさい int f(int a, int b, int c) { return 3 * a + 3 * b + 3 * c; } int f(int a, int b, int c) { return 3 * (a + b + c); } bool p(bool a, bool b, bool c) { return (!a && b a &&!b)!= c; } bool p(bool a, bool b, bool c) { return a == b == c; }

4 Hoare Triple {P}S {Q} ホーア論理 P は事前条件で,Q は事後条件.{P}S{Q} が正しいことは P が成り立つ全ての状態で S を実行すると Q が成り立つ状態で終了することを主張している. 代入の公理図式 {P[ x/ E ]}x :=E {P} 逐次規則 {P}S {Q},{Q}T {R} {P}S ;T {R} 条件規則 {B P}S {Q},{ B P}T {Q} {P}if B then S else T fi {Q} 結果規則 P ' P,{P}S {Q},Q Q' {P '}S {Q ' }

5 n 0 の時 int r = 1; for (int i = 1; i <= n; ++i) r *= i; ループの推論はめんどいが実行された際に,r=n! となることを示す ( 値の定義域は無視する ). {Q}initialization ; while B do S done{r} Pはループ不変条件.{P B}S {P} ループ実行前に P が成り立つ. ループの実行が停止する. ループの停止直後に R が成り立つ. P B R ループの実行が停止することを示すには次の 2 点を満たす整数式 T を見つければ十分. T は各繰り返しで減少する. すなわち新しい変数 v に対し, {P B}v :=T ; S {T v} 実行すべき繰り返しがある間は T>0 が成り立つ. P B T 0

6 まず, ループ不変条件 P は, r= i 1! 1 i n 1 であり, これを示すには, {P i n}r :=ir ;i :=i 1{P} を証明すれば良い. ループの推論はめんどい代入列 r :=ir ;i :=i 1 を真に定める最弱事前条件は P [i/i 1][r/ir] なので, P i n P [i/i 1][r/ir] を示す. P[i /i 1][ r/ir] r= i 1! 1 i n 1 [i/i 1][r/ir] r=i! 1 i 1 n 1 [r/ir] ir=i! 1 i 1 n 1 ir=i! 0 i n r= i 1! 0 i n r= i 1! 1 i n 1 i n P i n

7 ループの推論はめんどい次に, ループが停止することを示す為の整数式 T を探す. これは, n 1 i である. なぜなら, 新しい変数 v に対し, n 1 i [i /i 1][r /ri][ v/n 1 i] n i n 1 i True だから, {P i n}v :=n 1 i r:=ir ;i :=i 1{n 1 i v} であり, n 1 i は繰り返しのたびに減少し, また, P i n r= i 1! 1 i n 1 i n i n 1 0 n 1 i より, P i n 0 n 1 i n 1 i だから, は繰り返しが残っている間は 0 より大きい. 以上より, 次のことが言えた. {P}whilei ndo r :=ir ;i :=i 1done{P n i}

8 ループの推論はめんどい次に, n 0 なら, ループ開始前に P が成り立つこと, すなわち次を示す. {n 0}r:=1 ;i :=1{P} を示す. P [i /1][ r/1] r= i 1! 1 i n 1 [i /1][r/1] 1=0! 1 1 n 1 n 0 最後に, r=n! が P n i P n i r=n! を示す. P n i r= i 1! 1 i n 1 n i r= i 1! i=n 1 r=n! 以上で階乗が計算できることが示された. より弱いこと, すなわち,

9 STL の algorithm transform(v.begin(), v.end(), back_inserter(u), _1 * _1) int n = accumulate(v.begin(), v.end(), 1, _1 * _2); int m = inner_product(v.begin(), v.end(), u.begin(), 0); いちいち iterator の pair を扱うのが面倒くさい. container に連続して適用したい.

10 Range N を 1 から初めてその 2 乗を足していき, 和が 2000 を初めて超えたとき和はいくつになるか using namespace pstade::oven; using namespace boost::lambda; int v = counting(1, max_count) transformed(regular(_1 * _1)) scanned(regular(_1 + _2)) dropped_while(regular(_1 <= 2000)) front;

11 リスト Range の推論にリスト ( 列 ) の理論が使える. 気がする. Listr A=ε A : r Listr A Listl A=ε Listl A : l A [1, 2,3]=1: 2: 3: ε =1: 2: 3: ε

12 [1, 2]++[3, 4,5]=[1, 2,3, 4,5] ++ :Listr A Listr A Listr A ε ++ ys= ys x : xs ++ ts=x : xs ++ ys 結合律単位元リストの連結 xs ++ ys ++ zs=xs ++ ys ++ zs xs ++ε=ε ++ xs=xs concat[[1, 2],[ ],[3, 4,5]]=[1,2, 3, 4,5] concat:listr Listr A Listr A concat ε=ε concat xs : xss =xs ++concat xss ++ 上の concat の分配律 concat xs ++ ys =concat xs++concat ys

13 reverse[1, 2,3, 4,5]=[5, 4,3, 2,1] reverse:listr A Listr A reverse ε=ε reverse x : xs =reverse xs [ x] reverse reverse xs =xs length[1, 2,3, 4,5]=5 length :Listr A N length ε=0 length x : xs =1 length xs ++ 上の # の分配律リストの反転リストの長さ length xs ++ ys =length xs length ys

14 take 3[1, 2,3, 4,5]=[1,2, 3] drop 3[1, 2,3, 4,5]=[4,5] take, drop take:n Listr A Listr A take0 xs=ε take n 1 ε=ε take n 1 x : xs =x : take n xs drop:n Listr A Listr A drop0 xs=xs drop n 1 ε=ε drop n 1 x : xs =drop n xs take n xs ++dropn xs=xs take m take n=take m n drop m drop n=drop m n take m drop n=drop n take m n splitat n xs= take n xs,drop n xs

15 Listr: A B Listr A Listr B Listr f ε=ε Listr f x : xs = f x : Listr f xs Listr Listr λ x. x 2 [1, 2,3, 4,5]=[1,4, 9,16,25] Listr id=id Listr f g=listr f Listr g f head=head Listr f Listr f tail=tail Listr f Listr f reverse=reverse Listr f Listr f concat=concat Listr Listr f 特に, concat[ xs, ys]=xs ++ ys なので, Listr f xs ++ ys =Listr f xs ++Listr f ys

16 filter odd[1, 2,3, 4,5]=[1,3,5] filter filter : A Bool Listr A Listr A filter p=concat Listr p wrap,const ε p f, g a p a = f x otherwise=g x wrap x=x : ε const x a=x filter p filter q=filter p,q f, g x= f x, g x filter p concat=concat Listr filter f

17 zip, unzip zip [1, 2,3],[a,b,c] =[ 1, a, 2, b, 3, c ] zip:listr A Listr A Listr A B zip ε, ε =ε zip x : xs, y : ys = x, y :zip xs, ys unzip:listr A B Listr A Listr A unzip= Listr π 0,Listr π 1 zip unzip=id zip Listr f Listr g =Listr f g zip Listr f Listr g unzip=unzip Listr f g f g= f π 0, g π 1

18 fold foldr c, x 1 : x 2 : x 3 : x 4 : ε =x 1 x 2 x 3 x 4 c foldr: A B A A Listr B A foldr c, h ε=c foldr c, h x : xs =h x, foldr c, h xs concat=foldr ε, ++ sum=foldr 0, + product=foldr 1, and=foldr True, Listr f =foldr ε, h where h x, xs = f x : xs length=sum Listr const1 filter p=foldr ε, p π 0 :,π 1

19 Listl 上の fold foldl: A B A A Listl B A foldl c, h ε=c foldl c, h xs : x =h foldl c, h xs, x 実際には Listr 上で定義されていることが多い. foldl: A B A A Listr B A foldl c, h ε=c foldl c, h x : xs =foldl h c, x, h xs reverse=foldl ε, cons wherecons xs x=x : xs

20 が結合的で単位元 eを持つなら, foldr e, xs=foldl e, xs 任意の x,y,z に対し, とと e について, x y z = x y z x e=e x ならば, foldr e, xs=foldl e, xs 第一双対性定理第ニ双対性定理第三双対性定理 foldr e, f xs=foldl e, flip f reverse xs

21 foldrの融合律 f a=b x, y [ f g x, y =h x, f y ] ならば, f foldr a, g =foldr b, h foldlの融合律 f a=b x, y [ f g x, y =h f x, y ] ならば, f foldl a, g =foldl b,h foldr a, f Listr g=foldr a, f g fold と Listr の融合律

22 Listr + A=wrap A A : r Listr + A Listl + A=wrap A Listl + A : l A 非空リスト foldr + f, g wrap x = f x foldr + f, g x : xs =g x,foldr + f, g xs head=foldr + id, π 0 foldr1 f =foldr + id, f maximum=foldr1

23 圏圏 C は対象 (object) の集まりと射 (morphism) の集まりからなる. C の任意の射 f には始域と呼ばれる対象と終域と呼ばれる対象が備わっている. dom f =A cod f =B f : A B A f B C の任意の射 f, gに対して,dom g = cod fのとき射の合成 g f が存在する. g f A B f g C 射の合成に対して結合律が成り立つ. f : A B, g : B C,h:C D [h g f = h g f ] C の任意の対象 Aに対して次を満たす恒等射 id A : A A が存在する. f : A B [id B f = f = f id A ]

24 集合と全域関数の圏圏 Set の対象は集合射は型付の全域写像 f, A, B where Dom f =A, Ran f B 恒等射 id A : A A はA 上の恒等写像射 f, A, B と射 g,c, D の合成射はB=Cのとき, またそのときにのみ定義され, g,c, D f, A, B = g f, A, D

25 積圏圏 A B の対象は A の対象 A と B の対象 B の対 A, B 射は A の射 f と B の射 g の対 f, g 恒等射 id A B は id A, id B f, g h, k = f h, g k

26 モノ射 f, g : C A [ f =g m f =m g ] が成り立つ時,m: A B をモノ射と言う. Set では単射. エピ射 f, g : B C [ f =g f e=g e] が成り立つ時,e : A B をエピ射と言う. Set では全射.

27 同型射 i : A B に対して j : B A が存在し, j i=id A i j=id B が成り立つ時,i : A B を同型射と言う. このような j は存在するなら多くとも1つなので, これをi 1 と書く. Set では全単射. 同型射はモノ射かつエピ射であるが, その逆は必ずしも成り立たない. i : A B が同型射のとき A と B は同型と言う.

28 関手 A,Bを圏とする. このとき関手 F : A B は対象から対象への写像と射から射への写像からなる. f : A B F f : F A F B F id A =id F A F g f =F g F f A F B A f F f F A g f B F B F g f C g F g F C 射の合成同様関手の合成が定義される. G F f =G F f 関手は ( 小さな ) 圏の圏の射となる.

29 Id :C C Id A= A Id f = f K B : A B K B A=B K B f =id B 恒等関手定関手二項関手始域が積圏の関手. F id A, id B =id F A, B F f g,h k =F f, h F g, k Listr: Set Set Listr f g =Listr f Listr g Listr id=id リスト関手

30 始対象と終対象 C の任意の対象 A に対し,0 A なる射が唯一存在するとき,0 を始対象と言う. C の任意の対象 A に対し, A 1 なる射が唯一存在するとき,1 を終対象と言う. Set では空集合が始対象で,singleton set が終対象.

31 A B 積対象と対象の積とは, 任意の対象 π 0 : A B A C と射の組 f :C A と g :C B f, g :C A B π 1 : A B B A B に対し, 次の図式を可換にするような射が唯一存在する, 2 つの射とを伴った対象のこと. A π 0 π 1 A B B f C f, g g π 0 f, g = f π 1 f, g =g id= π 0, π 1 f, g m= f m, g m h= f, g π 0 h= f π 1 h=g 圏の任意の対象の対が積を持つ時, その圏は積を持つと言う.

32 A B 余積対象と対象の余積とは, 任意の対象 ι 0 : A A B C と射の組 f :C A と g :C B [ f, g]: A B C ι 1 : A B B A B に対し, 次の図式を可換にするような射が唯一存在する, 2 つの射とを伴った対象のこと. A ι 0 ι 1 A B B f C [ f, g] g h=[ f, g ] h ι 0 = f h ι 1 =g [ f, g] ι 0 = f [ f, g ] ι 1 =g id=[ι 0, ι 1 ] m [ f, g ]=[m f, m g]

33 積関手 C が積を持つ時, 射に対し f g= f π 0, g π 1 : C C C が考えられる. と定義することで 2 項関手 id id= id π 0, id π 1 =id f g h, k = f h, g k f g h k = f h g k

34 f g=[ι 0 f,ι 1 g] 余積関手と定義することで 2 項関手 +:C C C が考えられる. id id=[ι 0 id,ι 1 id]=id [ f, g] h k =[ f h, g k ] f g h k = f h g k [ f, g ],[h, k ] =[ f, h, g, k ] 交換律

35 多項式関手恒等関手と定関手は多項式関手 FとGが多項式関手のとき,FG, F+G, F Gは多項式関手 F G h=f h G h F G h=f h G h 例えば F X =A K A とF f =id A f id A によって定まる関手 Fは, F =K A Id K A なので多項式関手

36 自然変換関手 F,G : A B に対して, 自然変換 τ : F G とは,AA の各対象 A に, B の射 τ A : F A G A を割り当てる写像で,A の任意の射 f : A A' について次の図式を可換にするもの. F f F A F A' τ A τ A ' G f τ A =τ A' F f G A G A' G f

37 自然変換の例 f head=head Listr + f Listr f tail=tail Listr + f Listr f reverse=reverse Listr f Listr Listr f inits=inits Listr f Listr f concat=concat Listr Listr f zip Listr f Listr g =Listr f g zip Listr f Listr g unzip=unzip Listr f g

38 任意の関手 F 恒等変換に対して, 恒等変換 id F : F F は, id F A =id FA 自然変換の合成 φ: G H と ψ : F G に対し, φ ψ A =φ A ψ A F A ψ A G A φ A H A F f G f H f F A' ψ A ' G A' τ A ' H A' 自然変換はその対象が関手である圏の射となる各 component が全単射の時, 自然変換は自然同系射と呼ばれる

39 代数関手 F :C C に対して,F- 代数とは, 型 A F Aを持つ射のこと. f : A F A からする射 h: A A' g : A' F A' への F- 準同型射とは, 次の図式を可換に F A F h f A h F A' g h f =g F h A' 恒等射は準同型射であり, 準同型射の合成は準同型射なので F- 代数は射が準同型射な圏 Alg F の対象となる.

40 始代数 Set の多項式関手を初め, 多くの関手に対してこれを α : F T T で表す. Alg F は始対象を持ち, F- 始代数が存在すると言うことは, 任意のF- 代数 f : A F A α から [ f ] :T A で表す. F T α T F [ f ] [ f ] に対し, f への準同型射が唯一存在すると言うこと. この準同型射を F A f A h= [ f ] h α= f F h [ f ] の形の射を catamorphism と言う.

41 [ f ] α= f F [ f ] [α] =id 評価規則反射律 id= [ f ] id α= f F id f =α h [ f ] = [ g] h f =g F h 融合律 h [ f ] = [ g ] h [ f ] α=g F h [ f ] h [ f ] α=g F h F [ f ] h f F [ f ] =g F h F [ f ] h f =g F h

42 型関手 Listr A=ε A : r Listr A は [ε, : r ]: F A Listr A Listr A F A B=1 A B かつ F A f =id 1 id A f で定義される関手 F A をの始代数として宣言する. F A は二項関手 F の第一引数を A で固定したものと見なす. F を始代数のコレクション α A : F A,T A T A を伴う二項関手とすると, T f = [α F f,id ] と定義することによって T を関手にすることが出来る. 例えばリスト関手は, Listr f = [[ε, : r ] id f id ] により定義される. 変形すると, Listr f = [ε, : r f id ]

43 catamorphism は fold 型 Listr A に対し, h= [c, f ] h α=[c, f ] Fh h α=[c, f ] id id h h α=[c, f id h ] h [ε, : r ]=[c, f id h ] [h ε, h : r ]=[c, f id h ] h ε=c h : r = f id h これは, h ε=c h x, xs = f x, h xs ということであり, すなわち, [c, f ] =foldr c, f ということ.

44 [h] T g= [h F g,id ] 型関手の融合律 [h] T g= [h F g,id ] [h] [α F g,id ] = [h F g, id ] [h] α F g, id =h F g,id F id, [h] h F id, [h] F g, id =h F g, id F id, [h] True 例えば sum= [0, + ] とすると, sum Listr f = [0, + f id ]

45 分配圏積と余積を持つ圏において, 対象 A B C と対象 A B A C が同型の時, その圏を分配圏と言う. 積と余積を持つ圏では, undistl: A B A C A B C は常に存在する.( 例えば undistl=[id ι 0, id ι 1 ] とすれば良い ) しかし, 逆射 distl: A B C A B A C が存在するとは限らない. 例えば Set が分配圏.

46 論理値分配圏では論理値を Bool=1 1, True=ι 0, False=ι 1 とすることにより扱える. =[False, True] quad を Bool な同型射として, =[True,False,False,False] quad 条件式 p f, g =[ f, g ] π 0 π 0 distl id, p h p f, g = p h f, h g p f, g h= p h f h, g h p f, f = f filter filter p= [ε, p π 0 : r, π 1 ]

47 Banana-split の法則 [h], [k ] = [ h F π 0, k F π 1 ] catamorphism の普遍性より, [h], [k ] α= h F π 0, k F π 1 F [h], [k ] を示せばよい. [h], [k ] α = [h α], [k α] = h F [h], k F [k ] = h F π 0 [h], [k ],k F π 1 [h], [k ] = h F π 0 F [h], [k ], k F π 1 F [h], [k ] = h F π 0, k F π 1 F [h], [k ]

48 average= / sum, length リストの横断を纏めるこの average の定義はリストを 2 度横断する. sum, length = [0, + ], [0, 1 π 1 ] = [ [0, + ] F π 0,[0, 1 π 1 ] F π 1 ] = [ [0, + ] id id π 0,[0, 1 π 1 ] id id π 1 ] = [ [0, + id π 0 ],[0, 1 π 1 id π 1 ] ] = [ 0,0, + id π 0, 1 π 1 id π 1 ] = [ 0,0, + id π 0, 1 π 1 π 1 ] λ 式を用いると, [ 0,0, λ a, b, n. a b, n 1 ]

49 やり残しとこれから currying の圏論的扱い Curry Howard Lambek 同型対応 F- 代数と catamorphism の双対概念としての F- 余代数と anamorphism モナドとコモナド集合と全域関数の圏ではなく pointed CPO と連続関数の圏関数と category ではなく関係と allegory などなど

50 参考文献 Antony J. T. Davie. An Introduction to Functional Programming Systems Using Haskell. Cambridge University Press, Benjamin C. Pierce. Basic Category Theory for Computer Scientists. MIT Press, David Gries, and Fred B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, Jeremy Gibbons and Oege De Moor (Eds). The Fun of Programming. Palgrave Macmillan, Mac Lane, S. Categories for the Working Mathematician. Springer, Richrd Bird. Introduction to Functional Programming using Haskell. Prentice Hall, Richrd Bird and Oege De Moor. Algebra of Programming. Prentice Hall, Roland Backhouse, Roy Crole and Jeremy Gibbons (Eds). Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. Springer-Verlag, Steve Awodey. Category Theory. Oxford University Press, 2006.

Functional Programming

Functional Programming PROGRAMMING IN HASKELL プログラミング Haskell Chapter 7 - Higher-Order Functions 高階関数愛知県立大学情報科学部計算機言語論 ( 山本晋一郎大久保弘崇 2013 年 ) 講義資料オリジナルは http://www.cs.nott.ac.uk/~gmh/book.html を参照のこと 0 Introduction カリー化により