351

関数型プログラミングや PLT サークルで「coalgebras」という用語を何度か耳にしたことがあります。特に、オブジェクト、コモナド、レンズなどに関する議論の場合はそうです。この用語をグーグルで検索すると、これらの構造の数学的な説明を提供するページが表示されますが、これは私にはほとんど理解できません。プログラミングのコンテキストでコールゲブラが何を意味するのか、その重要性は何か、オブジェクトやコモナドとどのように関係するのか、誰か説明してもらえますか?

4

4 に答える 4

487
于 2013-04-15T18:17:28.103 に答える
86

F-algebras and F-coalgebras are mathematical structures which are instrumental in reasoning about inductive types (or recursive types).

F-algebras

We'll start first with F-algebras. I will try to be as simple as possible.

I guess you know what is a recursive type. For example, this is a type for a list of integers:

data IntList = Nil | Cons (Int, IntList)

It is obvious that it is recursive - indeed, its definition refers to itself. Its definition consists of two data constructors, which have the following types:

Nil  :: () -> IntList
Cons :: (Int, IntList) -> IntList

Note that I have written type of Nil as () -> IntList, not simply IntList. These are in fact equivalent types from the theoretical point of view, because () type has only one inhabitant.

If we write signatures of these functions in a more set-theoretical way, we will get

Nil  :: 1 -> IntList
Cons :: Int × IntList -> IntList

where 1 is a unit set (set with one element) and A × B operation is a cross product of two sets A and B (that is, set of pairs (a, b) where a goes through all elements of A and b goes through all elements of B).

Disjoint union of two sets A and B is a set A | B which is a union of sets {(a, 1) : a in A} and {(b, 2) : b in B}. Essentially it is a set of all elements from both A and B, but with each of this elements 'marked' as belonging to either A or B, so when we pick any element from A | B we will immediately know whether this element came from A or from B.

We can 'join' Nil and Cons functions, so they will form a single function working on a set 1 | (Int × IntList):

Nil|Cons :: 1 | (Int × IntList) -> IntList

Indeed, if Nil|Cons function is applied to () value (which, obviously, belongs to 1 | (Int × IntList) set), then it behaves as if it was Nil; if Nil|Cons is applied to any value of type (Int, IntList) (such values are also in the set 1 | (Int × IntList), it behaves as Cons.

Now consider another datatype:

data IntTree = Leaf Int | Branch (IntTree, IntTree)

It has the following constructors:

Leaf   :: Int -> IntTree
Branch :: (IntTree, IntTree) -> IntTree

which also can be joined into one function:

Leaf|Branch :: Int | (IntTree × IntTree) -> IntTree

It can be seen that both of this joined functions have similar type: they both look like

f :: F T -> T

where F is a kind of transformation which takes our type and gives more complex type, which consists of x and | operations, usages of T and possibly other types. For example, for IntList and IntTree F looks as follows:

F1 T = 1 | (Int × T)
F2 T = Int | (T × T)

We can immediately notice that any algebraic type can be written in this way. Indeed, that is why they are called 'algebraic': they consist of a number of 'sums' (unions) and 'products' (cross products) of other types.

Now we can define F-algebra. F-algebra is just a pair (T, f), where T is some type and f is a function of type f :: F T -> T. In our examples F-algebras are (IntList, Nil|Cons) and (IntTree, Leaf|Branch). Note, however, that despite that type of f function is the same for each F, T and f themselves can be arbitrary. For example, (String, g :: 1 | (Int x String) -> String) or (Double, h :: Int | (Double, Double) -> Double) for some g and h are also F-algebras for corresponding F.

Afterwards we can introduce F-algebra homomorphisms and then initial F-algebras, which have very useful properties. In fact, (IntList, Nil|Cons) is an initial F1-algebra, and (IntTree, Leaf|Branch) is an initial F2-algebra. I will not present exact definitions of these terms and properties since they are more complex and abstract than needed.

Nonetheless, the fact that, say, (IntList, Nil|Cons) is F-algebra allows us to define fold-like function on this type. As you know, fold is a kind of operation which transforms some recursive datatype in one finite value. For example, we can fold a list of integer into a single value which is a sum of all elements in the list:

foldr (+) 0 [1, 2, 3, 4] -> 1 + 2 + 3 + 4 = 10

It is possible to generalize such operation on any recursive datatype.

The following is a signature of foldr function:

foldr :: ((a -> b -> b), b) -> [a] -> b

Note that I have used braces to separate first two arguments from the last one. This is not real foldr function, but it is isomorphic to it (that is, you can easily get one from the other and vice versa). Partially applied foldr will have the following signature:

foldr ((+), 0) :: [Int] -> Int

We can see that this is a function which takes a list of integers and returns a single integer. Let's define such function in terms of our IntList type.

sumFold :: IntList -> Int
sumFold Nil         = 0
sumFold (Cons x xs) = x + sumFold xs

We see that this function consists of two parts: first part defines this function's behavior on Nil part of IntList, and second part defines function's behavior on Cons part.

Now suppose that we are programming not in Haskell but in some language which allows usage of algebraic types directly in type signatures (well, technically Haskell allows usage of algebraic types via tuples and Either a b datatype, but this will lead to unnecessary verbosity). Consider a function:

reductor :: () | (Int × Int) -> Int
reductor ()     = 0
reductor (x, s) = x + s

It can be seen that reductor is a function of type F1 Int -> Int, just as in definition of F-algebra! Indeed, the pair (Int, reductor) is an F1-algebra.

Because IntList is an initial F1-algebra, for each type T and for each function r :: F1 T -> T there exist a function, called catamorphism for r, which converts IntList to T, and such function is unique. Indeed, in our example a catamorphism for reductor is sumFold. Note how reductor and sumFold are similar: they have almost the same structure! In reductor definition s parameter usage (type of which corresponds to T) corresponds to usage of the result of computation of sumFold xs in sumFold definition.

Just to make it more clear and help you see the pattern, here is another example, and we again begin from the resulting folding function. Consider append function which appends its first argument to second one:

(append [4, 5, 6]) [1, 2, 3] = (foldr (:) [4, 5, 6]) [1, 2, 3] -> [1, 2, 3, 4, 5, 6]

This how it looks on our IntList:

appendFold :: IntList -> IntList -> IntList
appendFold ys ()          = ys
appendFold ys (Cons x xs) = x : appendFold ys xs

Again, let's try to write out the reductor:

appendReductor :: IntList -> () | (Int × IntList) -> IntList
appendReductor ys ()      = ys
appendReductor ys (x, rs) = x : rs

appendFold is a catamorphism for appendReductor which transforms IntList into IntList.

So, essentially, F-algebras allow us to define 'folds' on recursive datastructures, that is, operations which reduce our structures to some value.

F-coalgebras

F-coalgebras are so-called 'dual' term for F-algebras. They allow us to define unfolds for recursive datatypes, that is, a way to construct recursive structures from some value.

Suppose you have the following type:

data IntStream = Cons (Int, IntStream)

This is an infinite stream of integers. Its only constructor has the following type:

Cons :: (Int, IntStream) -> IntStream

Or, in terms of sets

Cons :: Int × IntStream -> IntStream

Haskell allows you to pattern match on data constructors, so you can define the following functions working on IntStreams:

head :: IntStream -> Int
head (Cons (x, xs)) = x

tail :: IntStream -> IntStream
tail (Cons (x, xs)) = xs

You can naturally 'join' these functions into single function of type IntStream -> Int × IntStream:

head&tail :: IntStream -> Int × IntStream
head&tail (Cons (x, xs)) = (x, xs)

Notice how the result of the function coincides with algebraic representation of our IntStream type. Similar thing can also be done for other recursive data types. Maybe you already have noticed the pattern. I'm referring to a family of functions of type

g :: T -> F T

where T is some type. From now on we will define

F1 T = Int × T

Now, F-coalgebra is a pair (T, g), where T is a type and g is a function of type g :: T -> F T. For example, (IntStream, head&tail) is an F1-coalgebra. Again, just as in F-algebras, g and T can be arbitrary, for example,(String, h :: String -> Int x String) is also an F1-coalgebra for some h.

Among all F-coalgebras there are so-called terminal F-coalgebras, which are dual to initial F-algebras. For example, IntStream is a terminal F-coalgebra. This means that for every type T and for every function p :: T -> F1 T there exist a function, called anamorphism, which converts T to IntStream, and such function is unique.

Consider the following function, which generates a stream of successive integers starting from the given one:

nats :: Int -> IntStream
nats n = Cons (n, nats (n+1))

Now let's inspect a function natsBuilder :: Int -> F1 Int, that is, natsBuilder :: Int -> Int × Int:

natsBuilder :: Int -> Int × Int
natsBuilder n = (n, n+1)

Again, we can see some similarity between nats and natsBuilder. It is very similar to the connection we have observed with reductors and folds earlier. nats is an anamorphism for natsBuilder.

Another example, a function which takes a value and a function and returns a stream of successive applications of the function to the value:

iterate :: (Int -> Int) -> Int -> IntStream
iterate f n = Cons (n, iterate f (f n))

Its builder function is the following one:

iterateBuilder :: (Int -> Int) -> Int -> Int × Int
iterateBuilder f n = (n, f n)

Then iterate is an anamorphism for iterateBuilder.

Conclusion

So, in short, F-algebras allow to define folds, that is, operations which reduce recursive structure down into a single value, and F-coalgebras allow to do the opposite: construct a [potentially] infinite structure from a single value.

In fact in Haskell F-algebras and F-coalgebras coincide. This is a very nice property which is a consequence of presence of 'bottom' value in each type. So in Haskell both folds and unfolds can be created for every recursive type. However, theoretical model behind this is more complex than the one I have presented above, so I deliberately have avoided it.

Hope this helps.

于 2013-04-15T18:18:50.453 に答える
37

チュートリアル ペーパーを読む (余) 代数と (余) 帰納法のチュートリアルでは、コンピューター サイエンスにおける余代数についての洞察を得ることができます。

以下は、あなたを納得させるための引用です。

一般的に、プログラミング言語のプログラムはデータを操作します。過去数十年にわたるコンピュータ サイエンスの発展の中で、たとえばプログラムが動作するデータの特定の表現に依存しないことを保証するために、これらのデータの抽象的な記述が望ましいことが明らかになりました。また、そのような抽象性は正当性の証明を容易にします。
この欲求は、代数仕様または抽象データ型理論と呼ばれる分野で、コンピューター サイエンスにおける代数的手法の使用につながりました。学習の目的は、代数でよく知られている手法の概念を使用して、それ自体がデータ型です。コンピューター科学者が使用するデータ型は、(コンストラクター) 操作の特定のコレクションから生成されることが多く、代数の「初期性」が非常に重要な役割を果たすのはこのためです。
標準的な代数的手法は、コンピューター サイエンスで使用されるデータ構造のさまざまな重要な側面を捉えるのに役立つことが証明されています。しかし、コンピューティングで発生する本質的に動的な構造のいくつかを代数的に記述するのは難しいことが判明しました。このような構造には通常、さまざまな方法で変換できる状態の概念が含まれます。このような状態ベースの動的システムへの正式なアプローチでは、一般に、古典的な初期の参考資料として、オートマトンまたは遷移システムが使用されます。
過去 10 年間で、そのような状態ベースのシステムは代数としてではなく、いわゆる余代数として記述されるべきであるという洞察が徐々に深まりました。これらは代数の正式な双対であり、このチュートリアルで正確に説明します。代数の「初期性」の二重の性質、つまり最終性は、そのような余代数にとって重要であることが判明しました。そして、そのような最終余代数に必要な論理的推論原理は、帰納法ではなく共帰納法です。

前奏曲、圏論について。 圏論はファンクターの理論に改名すべきです。カテゴリーは、ファンクターを定義するために定義しなければならないものです。(さらに、ファンクタは、自然な変換を定義するために定義しなければならないものです。)

ファンクターとは？ それは、構造を維持しながら、あるセットから別のセットへの変換です。（詳細については、ネット上に多くの優れた説明があります）。

F代数とは？ ファンクターの代数です。それはファンクターの普遍的な妥当性の研究にすぎません。

どのようにコンピュータサイエンスにリンクできますか? プログラムは、構造化された一連の情報として表示できます。プログラムの実行は、この構造化された情報の変更に対応します。実行がプログラム構造を維持するのは良さそうです。次に、実行は、この一連の情報に対するファンクターの適用と見なすことができます。(プログラムを定義するもの)。

なぜF余代数なのか? プログラムは、情報によって記述され、それに基づいて行動するため、本質的に二重です。そして、主にプログラムを構成したり変更したりする情報を2通りに見ることができます。

  • プログラムによって処理される情報として定義できるデータ。
  • プログラムによって共有されている情報として定義できる状態。

では、この段階で言いたいのは、

  • F 代数は、データの宇宙 (ここで定義) に作用する関手変換の研究です。
  • F-共代数は、状態の宇宙 (ここで定義されている) に作用する関手変換の研究です。

プログラムの存続期間中、データと状態は共存し、相互に補完します。それらは二重です。

于 2013-04-15T12:53:28.063 に答える
5

明らかにプログラミングに関連するものから始めて、数学的なものを追加して、できる限り具体的で現実的なものにします。

人工誘導について何人かのコンピューター科学者の言葉を引用しましょう…</h2>

http://www.cs.umd.edu/~micinski/posts/2012-09-04-on-understanding-coinduction.html

誘導は有限のデータに関するものであり、共誘導は無限のデータに関するものです。

無限データの典型的な例は、遅延リスト (ストリーム) のタイプです。たとえば、メモリ内に次のオブジェクトがあるとします。

 let (pi : int list) = (* some function which computes the digits of
 π. *)

限られた量のメモリしかないため、コンピュータは π のすべてを保持することはできません! しかし、それができることは、あなたが望む π の任意の長さの拡張を生成する有限プログラムを保持することです。リストの有限部分のみを使用する限り、その無限リストを必要なだけ計算できます。

ただし、次のプログラムを検討してください。

let print_third_element (k : int list) =   match k with
     | _ :: _ :: thd :: tl -> print thd


 print_third_element pi

このプログラムは、円周率の 3 桁目を出力するはずです。しかし、一部の言語では、関数への引数は、関数に渡される前に評価されます (遅延ではなく厳密な評価)。この削減順序を使用すると、上記のプログラムは、プリンター関数に渡す前に pi の数字を計算するために永久に実行されます (決して起こりません)。マシンには無限のメモリがないため、プログラムは最終的にメモリ不足になり、クラッシュします。これは最適な評価順序ではない可能性があります。

http://adam.chlipala.net/cpdt/html/Coinductive.html

Haskell のような遅延関数型プログラミング言語では、無限のデータ構造がいたるところにあります。無限リストとより風変わりなデータ型は、プログラムの部分間の通信に便利な抽象化を提供します。無限の遅延構造を使用せずに同様の利便性を実現するには、多くの場合、制御フローのアクロバティックな反転が必要になります。

http://www.alexandrasilva.org/#/talks.html Alexandra Silvaによるcoalgebraの例

周囲の数学的コンテキストを通常のプログラミング タスクに関連付ける

「代数」とは？

代数構造は一般に次のようになります。

  1. もの
  2. 何ができるか

これは、1. プロパティと 2. メソッドを持つオブジェクトのように聞こえるはずです。またはさらに良いことに、型シグネチャのように聞こえるはずです。

標準的な数学的例には、モノイド ⊃ 群 ⊃ ベクトル空間 ⊃ 「代数」が含まれます。モノイドはオートマトンのようなものです: 動詞のシーケンス (例: f.g.h.h.nothing.f.g.f)。git履歴を常に追加し、決して削除しないログはモノイドですが、グループではありません。逆数 (負の数、分数、根、蓄積された履歴の削除、壊れた鏡の破片の解除など) を追加すると、グループが得られます。

グループには、一緒に加算または減算できるものが含まれています。たとえば、Durations を一緒に追加できます。(しかし、Dates はできません。) 期間は、外部の数値によってもスケーリングできるため、(単なるグループではなく) ベクトル空間に存在します。( の型シグネチャscaling :: (Number,Duration) → Duration。)

代数 ⊂ ベクトル空間では、さらに別のことができますm :: (T,T) → T。これを「乗算」と呼ぶか、呼ばないでください。一度離れると、「乗算」(または「累乗」 ) がIntegers何であるかがあまり明白でなくなるためです。

（これが、人々が（圏論的）普遍的性質に目を向ける理由です：掛け算がどうあるべきか、またはどのようにすべきかを彼らに伝えるために：

製品の普遍性 )

代数 → 代数

余剰乗算は、乗算よりも恣意的ではない方法で定義する方が簡単です。なぜならT → (T,T)、同じ要素を繰り返すことができるからです。(「対角マップ」 – スペクトル理論の対角行列/演算子のようなもの)

Counit は通常、トレース (対角線エントリの合計) ですが、ここでも重要なのは counit の動作です。trace行列の良い答えです。

一般に、二重空間を見る理由は、その空間で考える方が簡単だからです。たとえば、通常の平面よりも法線ベクトルについて考える方が簡単な場合がありますが、ベクトルを使用して平面 (超平面を含む) を制御できます (ここでは、レイ トレーサーのようなおなじみの幾何学的ベクトルについて話します)。 .

(非) 構造化データを使いこなす

数学者はTQFT のような楽しいものをモデリングしているかもしれませんが、プログラマーはそれに取り組まなければなりません

  • 日時（+ :: (Date,Duration) → Date）、
  • 場所 ( Paris≠ (+48.8567,+2.3508)! 点ではなく形です。)、
  • ある意味で一貫性があるはずの構造化されていないJSON、
  • 間違っているが近い XML、
  • 合理的な関係の負荷を満たすべき信じられないほど複雑なGISデータ、
  • あなたにとっては意味のある正規表現ですが、perl にとってはかなり意味がありません。
  • すべての幹部の電話番号と別荘の場所、彼の (現在の) 妻と子供の名前、誕生日、および以前のすべての贈り物を保持する必要がある CRM。コーディングが難しく、
  • .....

コンピューター科学者は、coalgebras について話すとき、通常、デカルト積のような集合的な操作を念頭に置いています。これは、「代数は Haskell のコールジェブラである」という言葉の意味だと思います。しかし、プログラマーがPlace、Date/Time、および のような複雑なデータ型をモデル化Customerし、それらのモデルを可能な限り現実世界 (または少なくともエンドユーザーの現実世界のビュー) に近づける必要がある限り、私は双対性を信じています。セットワールドを超えて役立つ可能性があります。

于 2015-10-02T18:49:55.587 に答える