Quelles sont les utilisations des limites et des colimits de la théorie des catégories dans les problèmes quotidiens?

Je souhaite savoir comment utiliser les concepts de limites et de colimites pour modéliser des problèmes dans la vie de tous les jours? Quelqu'un pourrait-il peut-être fournir des exemples d'ingénierie (logicielle)? Ou décrire intuitivement en général pour quels types de problèmes de modélisation nous pouvons utiliser ces concepts? Je vous remercie.

Prenez quelques relations , R 1 ⊆ A 1 × A 2 . Soit π 1 : R 0 → A 1 , π 0 : R 1 → A 1 des projections avec des domaines restreints aux relations R 0 , R 1 . Alors le retrait de π 0 , π 1 est la jointure de R 0 et$R_0\subseteq A_0\times A_1$$R_1\subseteq A_1\times A_2$$\pi_1:R_0\to A_1$$\pi_0:R_1\to A_1$$R_0$$R_1$$\pi_0$$\pi_1$$R_0$ au sens SQL.$R_1$

Un bon exemple est celui de Tate et al., Generating Compiler Optimizations from Proofs . Il utilise les retraits et les poussées comme unions et intersections généralisées, dans les catégories où les flèches sont des substitutions (IIRC).

Ross Tate affirme (sur la page Web du papier) que les détails étaient accablants sans l'abstraction offerte par la théorie des catégories. Personnellement, je voudrais soumettre comme "preuves suggestives" (s'il peut y avoir des preuves d'une telle allégation) les diagrammes (6) et (7) dans leur article - ils ont l'air assez complexes sous forme schématique. Permettez-moi de citer leurs commentaires en ligne.

Certains nous ont demandé pourquoi nous avons fait abstraction de notre technique de généralisation de la preuve et pourquoi nous avons utilisé la théorie des catégories comme abstraction. Cependant, nous avons d'abord conçu l'algorithme abstrait, en utilisant la théorie des catégories, puis nous l'avons utilisé pour comprendre comment résoudre notre problème concret. Nous sommes restés coincés avec le problème concret, submergés par les détails et les variables, et toute solution à laquelle nous pouvions penser semblait arbitraire. Afin de réfléchir et de simplifier, nous avons décidé de formuler notre question de manière catégorique. Cela a conduit à un diagramme des sources et des puits, nous avons donc simplement utilisé des poussées et des retraits pour coller des choses ensemble. Le plus grand défi consistait à réaliser des poussées, plutôt que d'utiliser un concept standard existant. La formulation catégorique était facile à spécifier et à raisonner. Ensuite, nous avons instancié les processus abstraits,

Nous avons en fait trouvé ce processus d'abstraction à la théorie des catégories chaque fois que nous sommes coincés être assez fructueux. Non seulement cela finit par résoudre notre problème concret, mais nous nous retrouvons avec une meilleure compréhension de notre propre problème ainsi qu'une solution abstraite qui peut être facilement adaptée à d'autres applications. Ainsi, notre expérience suggère que la théorie des catégories peut être utile dans la construction d'algorithmes réels, en plus d'être utile comme cadre de formalisation. Nous serions intéressés de connaître d'autres expériences similaires, positives ou négatives.

Dans le livre de Spivak à la page 192, il donne un exemple d'utilisation de colimits pour créer des cartes de transit . En outre, son application 5.2.1.2 traite de l'application de correctifs de type Liquibase à un schéma de base de données au fil du temps, puis de l'utilisation des colimits pour raisonner entre les anciennes et les nouvelles données de manière universelle.

Un large champ d'applications concerne les transformations de graphes (appliquées en ingénierie dirigée par les modèles). Deux articles pertinents sont (fournis avec des liens vers Google Scholar):

• Introduction au didacticiel sur la transformation de graphes: une perspective de génie logiciel
• Approches algébriques de la transformation graphique - Partie I: Concepts de base et approche à double poussée.

EDIT: encore une fois, (une partie de) l'idée de base est que les poussées agissent comme une union avec de la colle. Cela permet de définir des "règles de réécriture" pour les graphiques - vous faites correspondre le côté gauche au graphique, puis vous collez le côté droit au (reste du) graphique d'une manière correspondante. J'ai peur de ne pas pouvoir ajouter de détails car je n'ai jamais obtenu plus que l'intuition.