代数的データ型はF-始代数的データ型
-
deprecatad
- 3201
- 5
- 0
- 0
-
- いいね！0
あいや🐕
@public_ai000ya
ん？ 今ほんの少しだけF代数について見てみたんだけど、F代数って 自己関手F:C->Cがあって A,B∈ob(C)に対して 射α:F(A)->Aとの組(A,α)こそがF-代数であり 射f:A->Bがあり、射β:F(B)->BとのF代数(B,β) ならば
2017-05-30 22:50:35
あいや🐕
@public_ai000ya
F-代数とF代数という表記が（僕のツイートで）混同してるのは、F-代数というのが一文字多くて、ツイート文字数がアレするからです
2017-05-30 22:56:57
あいや🐕
@public_ai000ya
F代数の圏は、F代数が対象、F代数準同型（写像）が射の圏なんだけど （任意の？）代数的データ型はF代数の圏の始対象（これを始代数と呼ぶぽい）であるらしい
2017-05-30 23:05:24
あいや🐕
@public_ai000ya
BoolのIdentity-代数は(Bool, [False, not:Bool->Bool])やろ（ほんまか？？？？） そんならBoolはIdentity-代数か？？？ いやわからん？？？
2017-05-30 23:22:22
あいや🐕
@public_ai000ya
（任意の？）X∈ob(Sets) F = 1+N×(-) と置いて 自己関手（の対象関数？）F : X -> 1+N×X 元x∈X 写像f : N×X -> X とすれば F-代数は(X, [x,f]) らしい
2017-05-30 23:37:59
あいや🐕
@public_ai000ya
言ったじゃん！！！ F-代数は対象Aとその写りを取ったα:F(A)->Aの組って言ったじゃん！！ [x,f]って！！！ xって！！！？
2017-05-30 23:41:41
もーひずむ
@yuwki0131
@public_ai000ya 具体的には、代数的データ型でリストを表した時に、 data List a = Cons a (List a) | Nil とした時、NilはF始代数における始対象で、|は直和、 Cons a (List a)は直和、=は、(Lambekの補題における)準同型F(a) =~ aを
2017-05-30 23:55:52
もーひずむ
@yuwki0131
@public_ai000ya すみません。Cons a (List a)は直和は、Cons a (List a)は直積の間違いです。。。
2017-05-31 00:01:32
あいや🐕
@public_ai000ya
@yuwki0131 うお～わからぬですー……けど、値が対象になるんですね！？ Cons a (List a)が直和…直積でなくてですか？
2017-05-31 00:02:01