Formal representation of an abstraction hierarchy

Question

Introduction

I'm writing my PhD thesis on Abstract Delta Modeling (ADM), an abstract algebraic description of modifications (known as deltas) able to act on products (as in 'software products'). This can be used to organize a set of related products (a 'product line') as a simple core product and a set of conditionally applied deltas, and thus enable greater re-use of the underlying artefacts.

The details of delta modeling are not really important to my question, but ADM serves as a good example to explain the issue, so I will introduce the most important concepts.

Background

The main structure of interest is the deltoid $(\mathcal P, \mathcal D, \cdot, \epsilon, \mathbf{[\kern-1pt[-]\kern-1pt]})$. Products come from a universal set $\mathcal P$. Deltas come from a monoid $(\mathcal D, \cdot, \epsilon)$ with composition operator $\cdot : \mathcal D \times \mathcal D \to \mathcal D$ and neutral element $\epsilon \in \mathcal D$. The semantic evaluation operator $\mathbf{[\kern-1pt[-]\kern-1pt]} : \mathcal D \to 2^{\mathcal P \times \mathcal P}$ transforms a 'syntactic' delta $d \in \mathcal D$ into a relation $\mathbf{[\kern-1pt[}\,d\,\mathbf{]\kern-1.5pt]} \subseteq \mathcal P \times \mathcal P$ which decides how $d$ can modify a product.

Question

As ADM is an abstract algebra, most of my work abstracts from the concrete nature of products and deltas, and a number of results are proved without descending to a more concrete level. Those results are expected to carry over to a more concrete domain, but I haven't formalized this yet.

There are examples and case studies that do work in a concrete domain: object oriented source-code, $\small\mathrm{\LaTeX}$ code, natural numbers, mobile phone profiles, etc. There are also some intermediate stages of abstraction such as nested key-value pairs. For each I redefine (or 'refine') $(\mathcal P, \mathcal D, \cdot, \epsilon, \mathbf{[\kern-1pt[-]\kern-1pt]})$.

I'd like to make this hierarchy explicit: (1) to provide greater clarity for the reader and (2) to formally justify using results from more abstract levels.

My question: How should I formally organize these levels of abstraction?

I'm hoping to be able to reason with a simple refinement relation $\sqsubseteq$ on deltoids. And I feel like it could be defined simply by appealing to the subset relation on $\mathcal P$ and $\mathcal D$. But I'm not sure yet. Are there existing approaches to the kind of problem I'm describing? Publications I should read?

The Deltoid Hierarchy

To give you a better idea of what I mean, here's the deltoid abstraction hierarchy I have in mind:

• Abstract Deltoid: This is the basic deltoid in which products and deltas can still be anything. Most of the theory is based on this one and most results are proved on this level.
  • Relational Deltoid: Here, deltas are relations on $\mathcal P$ and $\mathbf{[\kern-1pt[-]\kern-1pt]}$ is the identity function.
    • Functional Deltoid: Here, deltas are functional (or 'deterministic').
  • Natural Number Deltoid: This is the simplest concrete deltoid, created just to illustrate deltoid refinement. Here, products $\mathcal P = \mathbb N$ are natural numbers and deltas $\mathcal D = \mathbb N^+$ are simple number sequences representing polynomial operations.
  • Nested Key-Value Pair Deltoid: An intermediate level of abstraction for any hierarchy in which keys are mapped to values or to sub-hierarchies. Deltas can perform modifications in this 'tree' at any depth.
    • OOP Deltoid: For abstract representations of object-oriented programs. They are basically nested key-value pairs, because programs map module-names to sets of classes, which map class-names to sets of methods, which map method-names to method-implementations.
      • ABS Deltoid: ABS is a real object oriented programming language.
    • Phone Profile Deltoid: Here, a product is a flat mapping of settings (such as volume, screen brightness, etc.) to values from a corresponding domain.
  • $\small\mathrm{\LaTeX}$ Deltoid: Products are $\small\mathrm{\LaTeX}$ documents and deltas modify them by redefining macros.

Well, that should give you a fair idea of what I have in mind. Note, by the way, that for any deltoid, $\mathbf{[\kern-1pt[-]\kern-1pt]}$ is a monoid homomorphism from $\mathcal D$ to the $\mathcal D'$ belonging to the corresponding relational deltoid.

The actual hierarchy may be larger. It may also be differently organized, based on what kind of refinement theory I'll use. For example, if I go for a simple subset-relation on $\mathcal P$ and $\mathcal D$ the ABS Deltoid would not fit under the Nested Key-Value Pair Deltoid, for its products and deltas are actually plain text (source-code). But the hierarchy as given may still work if I use homomorphisms.

Answer 1

I believe it would be beneficial for you to look up the theory of abstract interpretation, which provides very thorough answers to similar questions in the slightly different area of lattice-based program analysis.

It appears to me that you are using a framework based on algebras. I'm using the word algebra here in the sense of universal algebra, where I assume that constraints on the structure of the algebra are given by equalities between terms. There are two different senses in which abstractions (or hierarchies) enter the picture.

1. Abstraction as a relationship between two specific algebras.You might want to say that one algebra has a richer structure than another algebra, or that every problem you can solve with one algebra you can solve with the other. This kind of relationship is what would be formalised buy homomorphisms, or some other mapping between algebras.
2. Abstraction hierarchies as families of algebras. In your case, these would be families of deltoids with certain properties. As a more general example, consider all partially ordered sets. We can think of lattices, distributive lattices, and Boolean lattices as a sequence of sub-families that have richer properties.

The two notions are closely related but different.

Abstraction between two structures

The insight of abstract interpretation is that it is useful to endow the structures you consider with a notion of order. Consider two structures

$(M, f_M)$ and $(N, f_N)$, with $f_M: M \to M$ and $f_N:N \to N$ as the operations of interest.

A homomorphism in the universal algebra sense would look something like this:

$h:M \to N$ is a function satisfying the equality $h(f_M(a)) = f_N(h(a))$.

We can view the two structures appearing above as pre-ordered structures

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

and the homomorphism we can rewrite to be a function satisfying

1. that if $a = b$ then $h(a) = h(b)$, and
2. for all $a$ in $M$, $h(f_M(a)) = f_N(h(a))$.

Now, suppose you have some other notion of approximation available that makes sense. For example, when we deal with sets of states in program verification, subset inclusion makes sense for certain application, or when dealing with formulae in automated deduction, implication makes sense. More generally, we can consider

$(M, \preceq, f_M)$ and $(N,\sqsubseteq, f_N)$, where $\preceq$ and $\sqsubseteq$ are preorders.

Now, instead of homomorphism, we can have an abstraction function

$\alpha: M \to N$ which is

1. monotone, meaning that whenever $a \preceq b$ we have $\alpha(a) \sqsubseteq \alpha(b)$, and
2. semi-commutes with the operations: $\alpha(f_M(a)) \sqsubseteq f_N(\alpha(a))$ for all $a$ in $M$.

The abstraction function makes explicit the idea that if the structure over $N$ is an abstraction of the structure over $M$, then evaluating a term in $N$ cannot produce more precise results (with respect to the notion of approximation in $N$) than evaluating the same term in $M$ and then mapping it to $N$.

Now we can ask if it is necessary to approach the problem in terms of abstraction as opposed to refinement. Meaning, can we not say that $M$ is a refinement of $N$ and formulate conditions in terms terms. This is exactly what a concretisation function does.

A concretisation function $\gamma: N \to M$ is monotone and satisfies the inequality $f_M(\gamma(b)) \preceq \gamma(f_N(b))$.

The abstraction and concretisation conditions are called soundness conditions in abstract interpretation. In the special case that $\alpha$ and $\gamma$ form a Galois connection, the abstraction and concretisation conditions are equivalent. In general, they are not equivalent.

Everything we have done so far only formalises the notion of abstraction between a pair of structures. The things I have said can be summarised far more succinctly in the language of category theory. I have avoided categories because of your comment above.

Abstraction Hierarchies

Suppose we have a structure $\mathcal{M}$ endowed with a preorder and some operations. We can consider all structures $\mathcal{N}$ such that $\mathcal{N}$ is an abstraction of $\mathcal{M}$ in the sense above. If we have that $\mathcal{N}_1$ is an abstraction of $\mathcal{N}_2$ and both are abstractions of $\mathcal{M}$, we have three elements of the hierarchy. The relation `is an abstraction of' allows us to define a preorder between structures. Let us call a family of structures ordered by abstraction a hierarchy.

If I consider your example, it appears that your abstract deltoid may be a candidate for the maximal element in some hierarchy. I'm not entirely sure because the abstract deltoid appears to be a family of deltoids rather than a specific deltoid.

What you can now do is consider different hierarchies. The hierarchy of all deltoids. A sub-hierarchy based on various considerations you have above. A specific example in the abstract interpretation context is a hierarchy of complete lattices that are in a Galois connection with a given powerset lattice, and sub-hierarchies consisting of only distributive or only Boolean lattices.

As Martin Berger points out in the comments, this notion of abstraction between hierarchies is captured by that of adjunctions between categories.

A Categorical Perspective

There was a comment requesting for more comments on categories. That comment is no longer there but I will respond anyway.

Let's step back and look at what you are doing in designing deltoids and what I have described above from a more general perspective. We are interested in understanding the essential structure of the entities we manipulate in a software context and the relationship between these entities.

The first important realisation is that we are not just interested in a set of elements but in the operations that we can perform on those elements and the properties of those operations. This intuition drives the design of classes in object oriented programming and the definition of algebraic structures. You have already made this intuition explicit in the definition of a deltoid which has identified a few operations of interest. More generally, this is the thought process underlying algebraic descriptions. We need to identify what our operations are and what properties they have. This step tell us the type structure that we are working with.

The second realisation is that we are not just interested in a set of elements but abstraction relationships. The simplest formalisation I can imagine of abstraction is to consider a preordered set. We can think of a preordered set as a strict generalisation of a set to something that comes with a notion of approximation baked in.

We ideally want to work in a setting where both the insights above are first-class citizens. Meaning, we want a typed setting like that of an algebra, but also the approximation aware setting of a preorder. A first step in this direction is to consider a lattice. A lattice is a conceptually interesting structure because we can define it in two equivalent ways.

1. We can define a lattice equationally as a set $(L, \sqcap, \sqcup)$ equipped with a meet and a join operation. We can then derive the partial order by defining $a \sqsubseteq b$ to hold whenever $a \sqcap b = a$.
2. An alternative is to define a lattice as a partially ordered set $(L, \sqsubseteq)$ satisfying that every pair of elements in $L$ has a unique greatest lower bound and least upper bound. We can then derive the meet and join operations from the partial order.

A lattice is thus a mathematical structure which can be approached from the algebraic or the approximation perspective. The shortcoming here is that the elements of a lattice themselves do not possess a type structure that is factored into the approximation relationship. Meaning, we cannot compare elements based on the notion of having more or less structure.

In the context of your problem, you can think of categories as a natural generalisation of preorders that capture both the notion of approximation (in the morphisms) and type structure in an algebraic setting. The setting of category theory allows us to dispense with various unnecessary distinctions and focus on the structure of entities you care about and approximation of that structure. Universal properties and adjunctions give you a very powerful vocabulary and tools to understand the landscape of structures you are interested in and enables a rigorous mathematical treatment of even intuitive notions like different levels of abstraction.

Regarding my comment about abstract deltoids, it appears that what you want is a category. The abstract deltoid is a specific category analogous to the category of sets. There are other categories you are considering. I initially thought you were defining a deltoid that in the sense of category theory would be a terminal (or final) object.

You are studying the kind of questions that category theory provides a very satisfying answers for. I hope you will be able to come to that conclusion yourself.

References

1. Abstract interpretation and application to logic programs, Patrick Cousot and Radhia Cousot. The first half of this article is a general tutorial style introduction to the topic of abstract interpretation.
2. Abstract interpretation frameworks, Patrick Cousot and Radhia Cousot. This article discusses all the possibilities I sketched above concerning abstraction and concretisation functions in great detail.
3. Systematic Design of Program Analysis Frameworks, Patrick Cousot and Radhia Cousot. This was the paper which introduced the notion of hierarchies of abstractions in the program analysis context.
4. Generalized Strong Preservation by Abstract Interpretation, Francesco Ranzato and Francesco Tapparo. This paper applies these ideas in a different context of abstractions that preserve temporal logic formulae. You will find worked examples of Boolean and distributive abstractions here.
5. Abstract Interpretation, Logical Relations, and Kan Extensions, Samson Abramsky. Presents a category theory perspective on the order theoretic material above.

Answer 2

You are working on your PhD. Saying "I am not well versed in $X$" is not an excuse. And if you're good, then saying "my advisor does not know $X$" is not an excuse either.

You are using monoids where you should be using categories. Your monoid operations presupposes that you can combine any $\delta$'s together. But does this really make sense, for example, how would you compose "add plastic casing" and "add metal casing"? I suppose some of your $\delta$'s result in empty relations because they make no sense. You should be suspicious of that sort of thing.

As an interested observer it seems that the monoid should be a category, so we can compose two $\delta$'s only if it makes sense for them to be composed. Then your semantic evaluation is just a functor into the category of sets and relations. And then you see that there are lots of other categories that you could use. Functional deltas will correspond to a functor which maps into the category of sets and functions, the natural numbers deltoid is a functor into the monoid of polynomials on natural numbers (seen as a category), etc.

I am not sure you want to formalize LaTeX and Nokia mobile phones too seriously in the general theory. But of course your theory should be applicable to such examples (just don't get hung up when you discover that mobile phones do not actually have a well-defined semantics).

You are really shortchanging yourself by insisting on a predetermined technology (by your advisor?), by the looks of it.