Computational Abstraction

Abstract

Representation and abstraction are two of the fundamental concepts of computer science. Together they enable "high-level" programming: without abstraction programming would be tied to machine code; without a machine representation, it would be a pure mathematical exercise. Representation begins with an abstract structure and seeks to find a more concrete one. Abstraction does the reverse: it starts with concrete structures and abstracts away. While formal accounts of representation are easy to find, abstraction is a different matter. In this paper, we provide an analysis of data abstraction based upon some contemporary work in the philosophy of mathematics. The paper contains a mathematical account of how Frege's approach to abstraction may be interpreted, modified, extended and imported into type theory. We argue that representation and abstraction, while mathematical siblings, are philosophically quite different. A case of special interest concerns the abstract/physical interface which houses both the physical representation of abstract structures and the abstraction of physical systems.

Keywords: Frege; abstraction; computation; representation; specification.

Figure 1

$append:L\left[T\right]\otimes L\left[T\right]\Rightarrow L\left[T\right]$.

Figure 2

List Equality.

Figure 3

$mem:L\left[T\right]\otimes T\Rightarrow Bool$.

Figure 4

Quantification Over Lists.

Figure 5

$\equiv :L\left[T\right]\otimes L\left[T\right]\Rightarrow Bool$.

Figure 6

Equality.

Figure 7

$union:S\left[T\right]\otimes S\left[T\right]\Rightarrow S\left[T\right]$.

Figure 8

Reversing a List.

Figure 9

$perm:L\left[T\right]\otimes L\left[T\right]\Rightarrow Bool$.

Figure 10

$duplicate:L\left[T\right]\Rightarrow L\left[T\right]$.

Figure 11

Extensional Equivalence.