J'ai entendu le terme "coalgebras" plusieurs fois dans la programmation fonctionnelle et PLT cercles, surtout quand la discussion est sur les objets, comonads, des lentilles, et tels. Googler ce terme donne des pages qui donnent la description mathématique de ces structures qui est à peu près incompréhensible pour moi. Quelqu'un peut-il expliquer ce qu'est coalgebras dans le contexte de la programmation, quelle est leur signification, et comment ils se rapportent à des objets et comonads?
Réponse
Trop de publicités?
zurgl
Points
1563
Passer par le tutoriel papier Un tutoriel sur la (co)algèbres et (co)induction devrait vous donner un aperçu de la co-algèbre dans l'informatique.
Ci-dessous est une citation de lui pour vous en convaincre,
En termes généraux, un programme dans certains langage de programmation manipule les données. Au cours de la le développement de l'informatique au cours des dernières décennies, il est devenu clair qu'un résumé description de ces données est souhaitable, par exemple pour s'assurer que le programme ne dépend pas de la représentation particulière de données sur lesquelles il opère. Aussi, une telle abstraction facilite l'exactitude des preuves.
Cette volonté a conduit à utiliser des méthodes algébriques en informatique, dans une branche appelée spécification algébrique ou du type abstrait de données de la théorie. L'objet de l'étude sont les types de données en elles-mêmes, à l'aide des notions de techniques qui sont familiers de l'algèbre. Les types de données utilisés par les informaticiens sont souvent générés à partir d'une collection donnée (constructeur) de l'exploitation,et c'est pour cette raison que "initiality" des algèbres joue un rôle important.
Standard techniques algébriques ont prouvé leur utilité dans la capture de divers aspects essentiels de structures de données utilisé en informatique. Mais il s'est avéré difficile à décrire algébriquement certains de la nature dynamique des structures qui se produisent dans le calcul. De telles structures sont généralement liés à une notion de l'état, qui peut être transformé en différentes manières. Formelle méthodes basées sur l'état des systèmes dynamiques en général de rendre l'utilisation d'automates ou de transition, les systèmes classiques de début de références.
Au cours de la dernière décennie, la perspicacité grandit peu à peu que cet état des systèmes à base ne devraient pas être décrit comme des algèbres, mais en tant que soi-disant co-algèbres. Ce sont les formel des double-algèbres, dans un sens qui sera précisé dans ce tutoriel. La double propriété de "initiality" pour les algèbres, à savoir la finalité s'est avéré déterminant pour la suite de la co-algèbres. Et le raisonnement logique principe qui est nécessaire pour de tels finale de la co-algèbres n'est pas l'induction, mais la co-induction.
Prélude, à propos de Catégorie de la théorie. Catégorie de la théorie, doit être renommer la théorie des foncteurs. Comme les catégories sont ce que l'on doit définir dans le but de définir les foncteurs. (D'ailleurs, les foncteurs sont ce que l'on doit définir dans le but de définir les transformations naturelles.)
Qu'est ce qu'un foncteur? C'est une transformation à partir d'un ensemble à un autre, la préservation de leur structure. (Pour plus de détails il y a beaucoup de bonne description sur le net).
Ce qui est une F-algèbre? C'est l'algèbre de foncteur. C'est juste l'étude de l'universel, de la bienséance de foncteur.
Comment peut-il être le lien à l'informatique ? Le programme peut être vue comme un ensemble structuré d'informations. Déroulement du programme correspondent à la modification de cet ensemble structuré d'informations. Il sonne bien, que l'exécution doit préserver la structure du programme. L'exécution peut être vue comme l'application d'un foncteur sur cet ensemble d'informations. (Celui de la définition du programme).
Pourquoi F-co-algèbre ? Programme double, par essence, comme ils sont de décrire l'information et de la ils agissent sur elle. Puis principalement les informations qui composent le programme et les faire changé peut être vue dans les deux sens.
- Des données qui peuvent être définir comme l'information traitée par le programme.
- De l'état qui peuvent être définis comme le partage de l'information par le programme.
Puis, à ce stade, je tiens à dire que,
- F-algèbre est l'étude de functorial transformation agissant sur les Données de l'Univers (comme cela a été défini ici).
- F-co-algèbres est l'étude de functorial transformation agissant sur l'État de l'Univers (comme cela a été défini ici).
Au cours de la vie d'un programme, les données et l'état de co-existent, et ils se complètent. Elles sont à double.
