<p>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. </p>

<p>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.</p>

<ol>
<li>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.</li>
<li>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. </li>
</ol>

<p>The two notions are closely related but different. </p>

<p><strong>Abstraction between two structures</strong></p>

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

<blockquote>
  <p>$(M, f_M)$ and $(N, f_N)$, with $f_M: M \to M$ and $f_N:N \to N$ as the operations of interest.</p>
</blockquote>

<p>A homomorphism in the universal algebra sense would look something like this:</p>

<blockquote>
  <p>$h:M \to N$ is a function satisfying the equality $h(f_M(a)) = f_N(h(a))$.</p>
</blockquote>

<p>We can view the two structures appearing above as pre-ordered structures</p>

<blockquote>
  <p>$(M, =, f_M)$ and $(N, =, f_N)$</p>
</blockquote>

<p>and the homomorphism we can rewrite to be a function satisfying</p>

<blockquote>
  <ol>
  <li>that if $a = b$ then $h(a) = h(b)$, and</li>
  <li>for all $a$ in $M$,  $h(f_M(a)) = f_N(h(a))$.</li>
  </ol>
</blockquote>

<p>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</p>

<blockquote>
  <p>$(M, \preceq, f_M)$ and $(N,\sqsubseteq, f_N)$, where  $\preceq$ and $\sqsubseteq$ are preorders.</p>
</blockquote>

<p>Now, instead of homomorphism, we can have an <em>abstraction function</em></p>

<blockquote>
  <p>$\alpha: M \to N$ which is</p>
  
  <ol>
  <li>monotone, meaning that whenever $a \preceq b$ we have $\alpha(a) \sqsubseteq \alpha(b)$, and</li>
  <li>semi-commutes with the operations: $\alpha(f_M(a)) \sqsubseteq f_N(\alpha(a))$ for all $a$ in $M$.</li>
  </ol>
</blockquote>

<p>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$.</p>

<p>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 <em>concretisation function</em> does. </p>

<blockquote>
  <p>A <em>concretisation function</em> $\gamma: N \to M$ is <em>monotone</em> and satisfies the inequality $f_M(\gamma(b)) \preceq \gamma(f_N(b))$.</p>
</blockquote>

<p>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.</p>

<p>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.</p>

<p><strong>Abstraction Hierarchies</strong></p>

<p>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 <em>`is an abstraction of'</em> allows us to define a preorder between structures. Let us call a family of structures ordered by abstraction a <em>hierarchy</em>. </p>

<p>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.</p>

<p>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.</p>

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

<p><strong>A Categorical Perspective</strong></p>

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

<p>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. </p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

<ol>
<li>We can define a lattice equationally as a set $(L, \sqcap, \sqcup)$ equipped with a meet and a join operation. We can then <em>derive</em> the partial order by defining $a \sqsubseteq b$ to hold whenever $a \sqcap b = a$. </li>
<li>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 <em>derive</em> the meet and join operations from the partial order.</li>
</ol>

<p>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. </p>

<p>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.</p>

<p>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. </p>

<p>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.</p>

<p><strong>References</strong></p>

<ol>
<li><a href="http://www.di.ens.fr/~cousot/COUSOTpapers/JLP92.shtml" rel="nofollow">Abstract interpretation and application to logic programs</a>, Patrick Cousot and Radhia Cousot. The first half of this article is a general tutorial style introduction to the topic of abstract interpretation.</li>
<li><a href="http://www.di.ens.fr/~cousot/COUSOTpapers/JLC92.shtml" rel="nofollow">Abstract interpretation frameworks</a>, Patrick Cousot and Radhia Cousot. This article discusses all the possibilities I sketched above concerning abstraction and concretisation functions in great detail.</li>
<li><a href="http://www.di.ens.fr/~cousot/COUSOTpapers/POPL79.shtml" rel="nofollow">Systematic Design of Program Analysis Frameworks</a>, Patrick Cousot and Radhia Cousot. This was the paper which introduced the notion of hierarchies of abstractions in the program analysis context. </li>
<li><a href="http://arxiv.org/abs/cs/0401016" rel="nofollow">Generalized Strong Preservation by Abstract Interpretation</a>, 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.</li>
<li><a href="http://logcom.oxfordjournals.org/content/1/1/5.abstract" rel="nofollow">Abstract Interpretation, Logical Relations, and Kan Extensions</a>, Samson Abramsky. Presents a category theory perspective on the order theoretic material above.</li>
</ol>

CC BY-SA 3.0
2013-04-14T10:21:22.290Z
Thanks for your thorough answer! And the lack of categories is much appreciated. ;-) (I'll have to study some intermediate category theory in the future.) I'll take a look at your references. -=#=- In the mean time, I have a question about your statement "the abstract deltoid appears to be a family of deltoids rather than a specific deltoid". Could you explain how the abstract deltoid is different in this respect than the others? Can't any algebraic structure be seen as the family of all its refinements?
mhelvens
CC BY-SA 3.0
2013-04-16T01:58:44.777Z
@VijayD Thanks for the update on CT. I am the one guilty of making the comment and then deleted it. I deeply believe that CT is more suitable for OP's issue. I am even more convinced after seeing your update. I think if the OP doesn't want to do it using CT, somebody else will.
Nobody
CC BY-SA 3.0
2013-04-18T17:34:22.117Z
It seems very likely that category theory provides the best answers to my questions. And I'm looking forward to studying it and understanding those answers better. And indeed, my lack of time to study and apply category theory should not be an excuse to give an 'inferior' answer on this website. -=#=- Nonetheless, I greatly appreciate Vijay's consideration. His answer on the monoid level was quite useful. -=#=- So I can't use categories right now. But I'll definitely explore the option in future work. Thanks all!
mhelvens
CC BY-SA 3.0
2013-04-19T00:19:09.943Z
You are in an excellent position to pick up the subject because you have before you a problem that you understand well and can directly analyse from the categorical perspective. I find this the best way to learn something and would urge you not to delay because texts on category theory seem intimidating. I'm sure there are bite-size portions to study. Good luck for the defense.
Vijay D
CC BY-SA 3.0
2013-04-13T06:37:55.373Z
2013-04-16T00:22:03.167Z
2013-04-16T00:22:03.167Z
Vijay D
<p>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.</p>

<p>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.</p>

<p>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. </p>

<p>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).</p>

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

CC BY-SA 3.0
2013-04-15T06:51:26.577Z
In general I agree with you. And I've never used either as an excuse. :-) But in this case, most of my thesis is already written and the monoid has been used in all my publications. -=#=- That being said, you make an excellent point. In the plastic/metal casing example, I now handle it by allowing the composition, but having the resulting delta evaluate to the empty relation (as you've guessed). It's all well defined, so it's sufficient for now. But I can see that your suggestion is more elegant. You've given me another good reason to study category theory. Thanks!
mhelvens
CC BY-SA 3.0
2013-04-15T09:03:27.037Z
@mhelvens I am a retired software engineer living in industry for long time. Came **back** to TCS after retirement. I'll ask you a real life question. Suppose you successfully formalize Nokia phone products using monoid in your thesis, what are you going to say in the oral defense if Apple announces that it acquires Nokia? Will that announcement break your model? It seems to me the more general the theory is, the better model it would be.
Nobody
CC BY-SA 3.0
2013-04-15T12:01:05.823Z
@scaaahu Interesting question. :-) Let me start by answering: "No, not at all." The theory is independent from the 'type' of device. -=#=- I assure you there's no need to convince me of the benefits of generalization. (In fact, I think I sometimes overdo it.) It just so happens that I didn't come across category theory in time for it to be useful for my PhD work. As I said, I do agree that it may be a valuable approach. But two months from my thesis deadline is not the time to fundamentally change my approach.
mhelvens
CC BY-SA 3.0
2013-04-16T09:09:48.703Z
Clearly, you are ready for a postdoc ;-)
Andrej Bauer
CC BY-SA 3.0
2013-04-18T17:21:33.000Z
Grant application already sent out. :-) I hope I'll be able to continue in this field.
mhelvens
CC BY-SA 3.0
2013-04-15T06:32:37.457Z
2013-04-15T06:32:37.457Z
Andrej Bauer
<h2>Introduction</h2>

<p>I'm writing my PhD thesis on <a href="http://www.mhelvens.net/professional/publications?view=publication&amp;task=show&amp;id=3" rel="nofollow">Abstract Delta Modeling</a> (ADM), an abstract algebraic description of modifications (known as <em>deltas</em>) able to act on <em>products</em> (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.</p>

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

<h2>Background</h2>

<p>The main structure of interest is the <em>deltoid</em> $(\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.</p>

<h2>Question</h2>

<p>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.</p>

<p>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]})$.</p>

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

<p><strong>My question:</strong> How should I formally organize these levels of abstraction?</p>

<p>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?</p>

<h2>The Deltoid Hierarchy</h2>

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

<ul>
<li><strong>Abstract Deltoid</strong>: 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.
<ul>
<li><strong>Relational Deltoid</strong>: Here, deltas are relations on $\mathcal P$ and $\mathbf{[\kern-1pt[-]\kern-1pt]}$ is the identity function.
<ul>
<li><strong>Functional Deltoid</strong>: Here, deltas are functional (or 'deterministic').</li>
</ul></li>
<li><strong>Natural Number Deltoid</strong>: 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. </li>
<li><strong>Nested Key-Value Pair Deltoid</strong>: 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.
<ul>
<li><strong>OOP Deltoid</strong>: 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.
<ul>
<li><strong>ABS Deltoid</strong>: ABS is a real object oriented programming language.</li>
</ul></li>
<li><strong>Phone Profile Deltoid</strong>: Here, a product is a flat mapping of settings (such as volume, screen brightness, etc.) to values from a corresponding domain.</li>
</ul></li>
<li><strong>$\small\mathrm{\LaTeX}$ Deltoid</strong>: Products are $\small\mathrm{\LaTeX}$ documents and deltas modify them by redefining macros.</li>
</ul></li>
</ul>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2013-04-11T19:14:09.033Z
Can you make it more explicit what the abstraction hierarchy is? What things are abstractions of what other things?
Dave Clarke
CC BY-SA 3.0
2013-04-12T08:06:39.333Z
Hi Dave! I updated my question. I hope this clarifies things a bit.
mhelvens
CC BY-SA 3.0
2013-04-12T14:36:18.903Z
How about building categories for each kind of deltoid, and then study the left and right adjoint functors (if any) between them?
Martin Berger
CC BY-SA 3.0
2013-04-12T15:28:09.900Z
I'm afraid I'm not well-versed in category theory. :-(
mhelvens
<pl.programming-languages><algebra><monoid>
Formal representation of an abstraction hierarchy
mhelvens
# Formal representation of an abstraction hierarchy

(Asked by: username_0 on 2013-04-11)

## Introduction

I'm writing my PhD thesis on [Abstract Delta Modeling](http://www.mhelvens.net/professional/publications?view=publication&task=show&id=3) (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.

**Tags:** pl.programming-languages, algebra, monoid
> **Comments:**
> **username_1**: Can you make it more explicit what the abstraction hierarchy is? What things are abstractions of what other things?  
> **username_0**: Hi Dave! I updated my question. I hope this clarifies things a bit.  
> **username_2**: How about building categories for each kind of deltoid, and then study the left and right adjoint functors (if any) between them?  
> **username_0**: I'm afraid I'm not well-versed in category theory. :-(  

---

## 2 answers

### Answer by username_3 on 2013-04-13. Score: 8 | Accepted answer

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](http://www.di.ens.fr/~cousot/COUSOTpapers/JLP92.shtml), 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](http://www.di.ens.fr/~cousot/COUSOTpapers/JLC92.shtml), 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](http://www.di.ens.fr/~cousot/COUSOTpapers/POPL79.shtml), 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](http://arxiv.org/abs/cs/0401016), 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](http://logcom.oxfordjournals.org/content/1/1/5.abstract), Samson Abramsky. Presents a category theory perspective on the order theoretic material above.

> **Comments:**
> **username_0**: Thanks for your thorough answer! And the lack of categories is much appreciated. ;-) (I'll have to study some intermediate category theory in the future.) I'll take a look at your references. -=#=- In the mean time, I have a question about your statement "the abstract deltoid appears to be a family of deltoids rather than a specific deltoid". Could you explain how the abstract deltoid is different in this respect than the others? Can't any algebraic structure be seen as the family of all its refinements?  
> **username_4**: @VijayD Thanks for the update on CT. I am the one guilty of making the comment and then deleted it. I deeply believe that CT is more suitable for OP's issue. I am even more convinced after seeing your update. I think if the OP doesn't want to do it using CT, somebody else will.  
> **username_0**: It seems very likely that category theory provides the best answers to my questions. And I'm looking forward to studying it and understanding those answers better. And indeed, my lack of time to study and apply category theory should not be an excuse to give an 'inferior' answer on this website. -=#=- Nonetheless, I greatly appreciate Vijay's consideration. His answer on the monoid level was quite useful. -=#=- So I can't use categories right now. But I'll definitely explore the option in future work. Thanks all!  
> **username_3**: You are in an excellent position to pick up the subject because you have before you a problem that you understand well and can directly analyse from the categorical perspective. I find this the best way to learn something and would urge you not to delay because texts on category theory seem intimidating. I'm sure there are bite-size portions to study. Good luck for the defense.  

---

### Answer by username_5 on 2013-04-15. Score: 9

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.

> **Comments:**
> **username_0**: In general I agree with you. And I've never used either as an excuse. :-) But in this case, most of my thesis is already written and the monoid has been used in all my publications. -=#=- That being said, you make an excellent point. In the plastic/metal casing example, I now handle it by allowing the composition, but having the resulting delta evaluate to the empty relation (as you've guessed). It's all well defined, so it's sufficient for now. But I can see that your suggestion is more elegant. You've given me another good reason to study category theory. Thanks!  
> **username_4**: @mhelvens I am a retired software engineer living in industry for long time. Came **back** to TCS after retirement. I'll ask you a real life question. Suppose you successfully formalize Nokia phone products using monoid in your thesis, what are you going to say in the oral defense if Apple announces that it acquires Nokia? Will that announcement break your model? It seems to me the more general the theory is, the better model it would be.  
> **username_0**: @scaaahu Interesting question. :-) Let me start by answering: "No, not at all." The theory is independent from the 'type' of device. -=#=- I assure you there's no need to convince me of the benefits of generalization. (In fact, I think I sometimes overdo it.) It just so happens that I didn't come across category theory in time for it to be useful for my PhD work. As I said, I do agree that it may be a valuable approach. But two months from my thesis deadline is not the time to fundamentally change my approach.  
> **username_5**: Clearly, you are ready for a postdoc ;-)  
> **username_0**: Grant application already sent out. :-) I hope I'll be able to continue in this field.  

---

