Représentation formelle d'une hiérarchie d'abstraction

introduction

J'écris ma thèse de doctorat sur la modélisation abstraite du delta (ADM), une description algébrique abstraite des modifications (connues sous le nom de deltas ) capables d'agir sur les produits (comme dans les «produits logiciels»). Cela peut être utilisé pour organiser un ensemble de produits connexes (une «ligne de produits») comme un produit de base simple et un ensemble de deltas appliqués conditionnellement, et ainsi permettre une plus grande réutilisation des artefacts sous-jacents.

Les détails de la modélisation delta ne sont pas vraiment importants pour ma question, mais ADM sert de bon exemple pour expliquer le problème, je vais donc présenter les concepts les plus importants.

Contexte

La structure principale d'intérêt est le deltoïde . Les produits proviennent d'un ensemble universel P . Les deltas proviennent d'un monoid ( D , ⋅ , ε ) avecopérateur de composition ⋅ : D × D → D etélément neutre ε ∈ D . L'opérateur d'évaluation sémantique$(\mathcal P, \mathcal D, \cdot, \epsilon, \mathbf{[\kern-1pt[-]\kern-1pt]})$$\mathcal P$$(\mathcal D, \cdot, \epsilon)$$\cdot : \mathcal D \times \mathcal D \to \mathcal D$$\epsilon \in \mathcal D$ transforme un delta «syntaxique» d ∈ D en une relation$\mathbf{[\kern-1pt[-]\kern-1pt]} : \mathcal D \to 2^{\mathcal P \times \mathcal P}$$d \in \mathcal D$ qui décide comment d peut modifier un produit.$\mathbf{[\kern-1pt[}\,d\,\mathbf{]\kern-1.5pt]} \subseteq \mathcal P \times \mathcal P$$d$

Question

Comme ADM est une algèbre abstraite, la plupart de mes travaux résument la nature concrète des produits et des deltas, et un certain nombre de résultats sont prouvés sans descendre à un niveau plus concret. Ces résultats devraient se poursuivre dans un domaine plus concret, mais je ne l'ai pas encore formalisé.

Il existe des exemples et des études de cas qui fonctionnent dans un domaine concret: code source orienté objet, Code X , nombres naturels, profils de téléphonie mobile, etc. Il existe également des étapes d'abstraction intermédiaires telles que des paires clé-valeur imbriquées. Pour chaque je redéfinis (ou «affine»)( P , D ,⋅,ϵ,$\small\mathrm{\LaTeX}$ .$(\mathcal P, \mathcal D, \cdot, \epsilon, \mathbf{[\kern-1pt[-]\kern-1pt]})$

Je voudrais rendre cette hiérarchie explicite: (1) pour fournir une plus grande clarté au lecteur et (2) pour justifier formellement l'utilisation des résultats de niveaux plus abstraits.

Ma question: comment organiser formellement ces niveaux d'abstraction?

J'espère pouvoir raisonner avec une simple relation de raffinement sur les deltoïdes. Et je me sens comme il pourrait être défini simplement en faisant appel à la relation de sous - ensemble de P et D . Mais je n'en suis pas encore sûr. Existe-t-il des approches pour le type de problème que je décris? Publications que je devrais lire?$\sqsubseteq$$\mathcal P$$\mathcal D$

La hiérarchie deltoïde

Pour vous donner une meilleure idée de ce que je veux dire, voici la hiérarchie d'abstraction deltoïde que j'ai en tête:

• Résumé Deltoïde : C'est le deltoïde de base dans lequel les produits et les deltas peuvent toujours être n'importe quoi. La majeure partie de la théorie est basée sur celle-ci et la plupart des résultats sont prouvés à ce niveau.
  • Deltoïde relationnel : Ici, les deltas sont des relations sur et $\mathcal P$ est la fonction d'identité. $\mathbf{[\kern-1pt[-]\kern-1pt]}$
    • Deltoïde fonctionnel : Ici, les deltas sont fonctionnels (ou «déterministes»).
  • Deltoïde en nombre naturel : Il s'agit du deltoïde en béton le plus simple, créé juste pour illustrer le raffinement du deltoïde. Ici, les produits sont des nombres naturels et les deltas D = N + sont de simples séquences de nombres représentant des opérations polynomiales.$\mathcal P = \mathbb N$$\mathcal D = \mathbb N^+$
  • Deltoïde de paires clé-valeur imbriquées : niveau d'abstraction intermédiaire pour toute hiérarchie dans laquelle les clés sont mappées à des valeurs ou à des sous-hiérarchies. Les deltas peuvent effectuer des modifications dans cet «arbre» ​​à n'importe quelle profondeur.
    • Delopoid OOP : Pour les représentations abstraites de programmes orientés objet. Ce sont essentiellement des paires clé-valeur imbriquées, car les programmes mappent les noms de module aux ensembles de classes, qui mappent les noms de classe aux ensembles de méthodes, qui mappent les noms de méthode aux implémentations de méthode.
      • ABS Deltoid : ABS est un véritable langage de programmation orienté objet.
    • Profil de téléphone Deltoïde : Ici, un produit est un mappage plat des paramètres (tels que le volume, la luminosité de l'écran, etc.) aux valeurs d'un domaine correspondant.
  • $\small\mathrm{\LaTeX}$$\small\mathrm{\LaTeX}$

$\mathbf{[\kern-1pt[-]\kern-1pt]}$$\mathcal D$$\mathcal D'$

$\mathcal P$$\mathcal D$

Je pense qu'il serait avantageux pour vous de rechercher la théorie de l'interprétation abstraite, qui fournit des réponses très approfondies à des questions similaires dans le domaine légèrement différent de l'analyse de programme sur réseau.

Il me semble que vous utilisez un framework basé sur les algèbres. J'utilise ici le mot algèbre dans le sens d'algèbre universelle, où je suppose que les contraintes sur la structure de l'algèbre sont données par des égalités entre les termes. Il existe deux sens différents dans lesquels les abstractions (ou hiérarchies) entrent dans l'image.

1. L'abstraction en tant que relation entre deux algèbres spécifiques. Vous voudrez peut-être dire qu'une algèbre a une structure plus riche qu'une autre algèbre, ou que chaque problème que vous pouvez résoudre avec une algèbre, vous pouvez le résoudre avec l'autre. Ce type de relation est ce qui serait formalisé par des homomorphismes d'achat, ou une autre cartographie entre algèbres.
2. Hiérarchies d'abstraction en tant que familles d'algèbres. Dans votre cas, il s'agit de familles de deltoïdes possédant certaines propriétés. À titre d'exemple plus général, considérons tous les ensembles partiellement ordonnés. Nous pouvons considérer les réseaux, les réseaux distributifs et les réseaux booléens comme une séquence de sous-familles qui ont des propriétés plus riches.

Les deux notions sont étroitement liées mais différentes.

Abstraction entre deux structures

L'intuition de l'interprétation abstraite est qu'il est utile de doter les structures que vous considérez d'une notion d'ordre. Considérons deux structures

$(M, f_M)$$(N, f_N)$$f_M: M \to M$$f_N:N \to N$

Un homomorphisme au sens de l'algèbre universelle ressemblerait à ceci:

$h:M \to N$$h(f_M(a)) = f_N(h(a))$

Nous pouvons voir les deux structures apparaissant ci-dessus comme des structures pré-ordonnées

$(M, =, f_M)$$(N, =, f_N)$

et l'homomorphisme que nous pouvons réécrire pour être une fonction satisfaisante

1. $a = b$$h(a) = h(b)$
2. $a$$M$$h(f_M(a)) = f_N(h(a))$

Supposons maintenant que vous ayez une autre notion d'approximation disponible qui ait du sens. Par exemple, lorsque nous traitons des ensembles d'états dans la vérification de programme, l'inclusion de sous-ensemble est logique pour certaines applications, ou lorsqu'il s'agit de formules dans la déduction automatisée, l'implication est logique. Plus généralement, on peut considérer

$(M, \preceq, f_M)$$(N,\sqsubseteq, f_N)$$\preceq$$\sqsubseteq$

Maintenant, au lieu de l'homomorphisme, nous pouvons avoir une fonction d'abstraction

$\alpha: M \to N$

1. $a \preceq b$$\alpha(a) \sqsubseteq \alpha(b)$
2. $\alpha(f_M(a)) \sqsubseteq f_N(\alpha(a))$$a$$M$

$N$$M$$N$$N$$M$$N$

$M$$N$

$\gamma: N \to M$$f_M(\gamma(b)) \preceq \gamma(f_N(b))$

$\alpha$$\gamma$

Tout ce que nous avons fait jusqu'à présent ne fait que formaliser la notion d'abstraction entre une paire de structures. Les choses que j'ai dites peuvent être résumées beaucoup plus succinctement dans le langage de la théorie des catégories. J'ai évité les catégories à cause de votre commentaire ci-dessus.

Hiérarchies d'abstraction

$\mathcal{M}$$\mathcal{N}$$\mathcal{N}$$\mathcal{M}$$\mathcal{N}_1$$\mathcal{N}_2$$\mathcal{M}$

Si je considère votre exemple, il apparaît que votre deltoïde abstrait peut être un candidat pour l'élément maximal dans une certaine hiérarchie. Je ne suis pas tout à fait sûr car le deltoïde abstrait semble être une famille de deltoïdes plutôt qu'un deltoïde spécifique.

Ce que vous pouvez maintenant faire, c'est considérer différentes hiérarchies. La hiérarchie de tous les deltoïdes. Une sous-hiérarchie basée sur diverses considérations que vous avez ci-dessus. Un exemple spécifique dans le contexte d'interprétation abstraite est une hiérarchie de réseaux complets qui sont en connexion galoisienne avec un réseau de jeux de pouvoirs donné, et des sous-hiérarchies constituées uniquement de réseaux distributifs ou booléens uniquement.

Comme le souligne Martin Berger dans les commentaires, cette notion d'abstraction entre hiérarchies est saisie par celle d'adjonctions entre catégories.

Une perspective catégorique

Il y avait un commentaire demandant plus de commentaires sur les catégories. Ce commentaire n'est plus là mais je répondrai quand même.

Revenons en arrière et examinons ce que vous faites dans la conception de deltoïdes et ce que j'ai décrit ci-dessus dans une perspective plus générale. Nous souhaitons comprendre la structure essentielle des entités que nous manipulons dans un contexte logiciel et la relation entre ces entités.

La première réalisation importante est que nous ne sommes pas seulement intéressés par un ensemble d'éléments mais par les opérations que nous pouvons effectuer sur ces éléments et les propriétés de ces opérations. Cette intuition anime la conception de classes en programmation orientée objet et la définition de structures algébriques. Vous avez déjà rendu explicite cette intuition dans la définition d'un deltoïde qui a identifié quelques opérations d'intérêt. Plus généralement, c'est le processus de pensée qui sous-tend les descriptions algébriques. Nous devons identifier nos opérations et leurs propriétés. Cette étape nous indique la structure de type avec laquelle nous travaillons.

La deuxième réalisation est que nous ne nous intéressons pas seulement à un ensemble d'éléments mais à des relations d'abstraction. La formalisation la plus simple que j'imagine de l'abstraction est de considérer un ensemble pré-ordonné. Nous pouvons considérer un ensemble pré-commandé comme une généralisation stricte d'un ensemble à quelque chose qui vient avec une notion d'approximation intégrée.

Nous souhaitons idéalement travailler dans un cadre où les deux idées ci-dessus sont des citoyens de première classe. C'est-à-dire que nous voulons un réglage typé comme celui d'une algèbre, mais aussi le réglage sensible à l'approximation d'une précommande. Un premier pas dans cette direction consiste à considérer un réseau. Un réseau est une structure conceptuellement intéressante car nous pouvons la définir de deux manières équivalentes.

1. $(L, \sqcap, \sqcup)$$a \sqsubseteq b$$a \sqcap b = a$
2. $(L, \sqsubseteq)$$L$

Un réseau est donc une structure mathématique qui peut être approchée du point de vue algébrique ou d'approximation. Le défaut ici est que les éléments d'un réseau eux-mêmes ne possèdent pas de structure de type qui est prise en compte dans la relation d'approximation. En d'autres termes, nous ne pouvons pas comparer des éléments basés sur la notion d'avoir plus ou moins de structure.

Dans le contexte de votre problème, vous pouvez considérer les catégories comme une généralisation naturelle des précommandes qui capturent à la fois la notion d'approximation (dans les morphismes) et la structure de type dans un cadre algébrique. Le cadre de la théorie des catégories nous permet de nous passer de diverses distinctions inutiles et de nous concentrer sur la structure des entités qui vous intéressent et l'approximation de cette structure. Les propriétés et adjonctions universelles vous donnent un vocabulaire et des outils très puissants pour comprendre le paysage des structures qui vous intéressent et permet un traitement mathématique rigoureux de notions même intuitives comme différents niveaux d'abstraction.

En ce qui concerne mon commentaire sur les deltoïdes abstraits, il semble que ce que vous voulez, c'est une catégorie. Le deltoïde abstrait est une catégorie spécifique analogue à la catégorie des ensembles. Il existe d'autres catégories que vous envisagez. J'ai d'abord pensé que vous définissiez un deltoïde qui, au sens de la théorie des catégories, serait un objet terminal (ou final).

Vous étudiez le genre de questions pour lesquelles la théorie des catégories fournit des réponses très satisfaisantes. J'espère que vous pourrez arriver vous-même à cette conclusion.

Références

1. Interprétation abstraite et application aux programmes logiques , Patrick Cousot et Radhia Cousot. La première moitié de cet article est une introduction générale de style tutoriel au sujet de l'interprétation abstraite.
2. Cadres d'interprétation abstraite , Patrick Cousot et Radhia Cousot. Cet article discute en détail toutes les possibilités que j'ai esquissées ci-dessus concernant les fonctions d'abstraction et de concrétisation.
3. Conception systématique des cadres d'analyse de programme , Patrick Cousot et Radhia Cousot. Ce document a introduit la notion de hiérarchies d'abstractions dans le contexte de l'analyse de programme.
4. Préservation forte généralisée par interprétation abstraite , Francesco Ranzato et Francesco Tapparo. Cet article applique ces idées dans un contexte différent d'abstractions qui préservent les formules de logique temporelle. Vous trouverez des exemples travaillés d'abstractions booléennes et distributives ici.
5. Interprétation abstraite, relations logiques et extensions Kan , Samson Abramsky. Présente une perspective de théorie des catégories sur le matériau théorique d'ordre ci-dessus.

$X$$X$

$\delta$$\delta$

$\delta$

Je ne suis pas sûr que vous souhaitiez formaliser trop sérieusement les téléphones portables LaTeX et Nokia dans la théorie générale. Mais bien sûr, votre théorie devrait être applicable à de tels exemples (ne vous bloquez pas lorsque vous découvrez que les téléphones mobiles n'ont pas réellement une sémantique bien définie).

Vous vous perdez vraiment en insistant sur une technologie prédéterminée (par votre conseiller?), Par son apparence.