Honest Implementation

A function f over some concrete domain C honestly implements a function f over an abstract domain A if it preserves the functionality of f under the representation, while also preserving the meaning of the domain elements as given by the domain generators.

We formally consider a (computational) family F over a domain A to be an algebra (in the universal-algebra sense), consisting of the domain (universe) A and operations F over A (of any arity), along with a matching vocabulary. Our definition of honest implementation will require the simulation of the desired function together with a set of generators. The implementation notion is then really about an algebra as a whole.

When we have cause to care about the intensionality (internal workings) of a computational mechanism, we will talk about a (computational) model comprising a set of algorithms, each of which involves a set of states, a subset of which are initial states, and a (partial and/or multivalued) transition function over states [18].

Definition 6.3 (Simulation [multivalued representation])

  • • A function f over a domain C simulates a function f of arity t over a domain A via representation p : A ^ C if, for every x e At, we have f (p(x)) c p( f (x)).
  • • Likewise, a family of functions F over C simulates a family F over A (via representation p) if each f e F is simulated via the same p by some f e F.

As usual, functions are extended to operate over sets by letting f (S) := {f (x) | x e S}.

Definition 6.4 (Honest Implementation) Consider an abstract domain A with generators G.

  • • A family of functions F over C provides an implementation of a family F over A if F is simulated by F.
  • • We will refer to the implementation as close if the simulation is via a bijection.
  • • An implementation F over C is honest as long as F includes the generators G as well as equality.
  • • We will say that a function f over C honestly implements a single function f over A if the implementation also supplies simulations g of each generator g e G including equality over A. In other words, we require that {f} U G implement {f} U G, for some set G of concrete generators and implementation = of abstract equality.

See the illustration in Fig. 6.1.

The point is that f implements a function f with respect to a specific set of generators. If Abe considers an abstract domain with generators that are natural, computable, and trackable for him, but completely useless for his sister, Sal, then f is an honest implementation of f for Abe but not for Sal.

We give next an example of an honest implementation of an abstract function over the rationals Q by means of a concrete function over strings.

Example 6.2 The task is to implement rational multiplication, m : Q x Q ^ Q, by means of a string-based model of computation.

• The abstract domain (A in the definition) is the set of rational numbers Q (with the subset of integers Z and its subsets the positive integers Z+ and negative integers Z-, plus the truth values), along with the following generators: Representing abstract rational numbers by concrete strings, and implementing the multiplication function

Fig. 6.3 Representing abstract rational numbers by concrete strings, and implementing the multiplication function

  • • The concrete domain (C) is the set ?* of finite strings over the symbols {0, 1, 2, 3,
  • 4, 5, 6, 7, 8, 9, -, #}, plus true and false.
  • • Let x e ? * denote the number x e Z in decimal notation.
  • 1-1
  • • The representation p : Q ^ ? * is defined by p(r) := {x # y | r = x/y, x e Z, y e Z+}.
  • • The implementations of the generators and equality are as follows:

О returns the string 0 Treturns the string 1

s» : If w is the decimal representation x of x e Z+, then 's(w) returns

the decimal representation x + 1 of x + 1. Otherwise it is undefined.

"n(w) returns the string -w qu, v) returns the string u # v

=(u, v) returns true iff u = x 1 # x2, v = y 1 # y2, and x1/x2 = y1/y2, for

some x1, y1 e Z and x2, y2 e Z+.

• The implementation m(u, v) of multiplication is the following: If u = x 1 # x2 and v = y1 # y2, where x1, y1 e Z and x2, y2 e Z+, then the implementation returns the string x 1 ? y1 # x2 ? y . Otherwise, multiplication is not defined.

See Fig. 6.3.

An implementation of multiplication that reduces the resulting fraction is as honest an implementation as the above one. ?

< Prev   CONTENTS   Source   Next >