13 Abstraction Functions and Commutative Diagrams

Say we have an obect, and we want to perform an operation on it. There are two ways of thinking of it

1. We can apply abstraction function on the implemented type, then perform the abstract operation on the abstract type
2. We can perfom the implemented operation on the concrete type, then apply the abstractin function on the concrete type.

This is a commutitive diagram. Both paths lead to the same place.

               Abstract
               Operation
             •----------------→•
 Abstraction ↑                 ↑ Abstraction
        Func |                 | Func
             •----------------→•
               Implemented
               Operation

For example, if we're representing sets as lists with duplicates, we can start of with the concrete value [1;2]:

               
               Abstract
               Operation – union {2, 3}
             {1,2}----------------→{1,2,3}
 Abstraction ↑                       ↑ Abstraction
        Func |                       | Func
             [1;2]----------------→[1;2;2;3]
               Implemented
               Operation – append [2;3]

The implementation is correct if the abstraction function commutes:

$$op_{abs}(AF(c))=AF(op_{conc}(c))$$