Date: Tue, 23 Jul 91 17:39:17 EDT
From: Sandy Murphy <sandy@com.TIS>
Message-Id: <9107232139.AA23669@TIS.COM>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: select
Cc: sandy@com.TIS

It has now been nearly a month since this topic was active.  I have
been remiss in not answering some of the responses to my question.  I
can only cite the usual excuses of the pressure of work, meetings,
etc.  (the usual lame excuses).

Some of the responses seemed to indicate a confusion as to whether I was
suggesting @ would not work in a "specification" or an "implementation".
So I thought I would try to explain the framework to my question.

In hierarchical descriptions, there are usually (at least) three levels.
The top level is the property you wish to establish/ the service you
     wish to provide/ the function you wish to calculate, etc.
     For example, SortedList.
The mid level is the algorithm you use to do this (i.e. establish/provide/
     calculate the property/service/function)
     For example, QuickSort will give you a sorted list
The bottom level is the code level implementation of this algorithm.
     For example, a C code implementation of QuickSort from your
     neighborhood undergraduate C class.

In relating the top and mid levels or the mid and bottom levels, the
higher level is usually called a "specification" and the lower level an
"implementation".  This terminology causes confusion when you talk about
the algorithm.  It is a specification with respect to the code, and an
implementation with respect to the top level.

If the top level indicates an unspecific choice, i.e. to use David
Shepherd's example:

  >e.g. suppose your algorithm takes a value x and adds an odd number to
  >it. then the specification could be
  >ALG_SPEC x x' = ? y. IS_ODD y /\ (x' = x+y)

then using @ to specify that choice would be fine, i.e.

  >then a valid implmentation would be
  >f x = x + (@y.IS_ODD y)
  >and you could prove
  >! x. ALG_SPEC x (f x)

But if ALG_SPEC is the top level, and f x = x + (@y.IS_ODD y) is the mid
level algorithm, then how do you prove your code at the bottom level
implements this algorithm?  I.e. to use Paul Loewenstein's example,

  >there is no way to transform it into something
  >"real" such as:
  >                       f x = x + 3
  >since that cannot be shown to implement:
  >                     f x = x + (@y.IS_ODD y)


Another example: suppose that the top level was
         SortedList(in_list,out_list)
and the mid level used a merge sort.  At some point, MergeSort says
something like "take the sublist with the least head element of all the
sublists".  If there are more than one list whose head elements have this
same least value, the algorithm doesn't care which is chosen.  In stating
MergeSort, you could use @ to specify this choice,
            y = @i. head(list_i) = min {head(list_i),i=1,..n}
and still be able to prove
            SortedList(in_list,MergeSort(in_list))

The problem would come in trying to show that your C code implements
MergeSort.  Your code will have to pick some method for making the choice
among all the lists whose head elements have the same least value.  The
code might take the first list with the least head element, or the last,
or whatever.  You can't show that the code's method of making the choice
implements the same choice as @.

In other words,

    y = @x.Px   ==>   P y

so @ is suited for use in an "implementation", but

    ~(P y   ==>   y = @x.Px)

so @ is not suited for use in a "specification".

My next comment has to do with the "meta-theorem" I posited.  I inserted
that conjecture as an after-thought, and I now regret it.  It was not
important to the point I was trying to make, and distracted some people
from my basic question about epsilon.  But even worse, as Rob Arthan
pointed out, it was incorrect.

--Sandy Murphy
  Trusted Information Systems
  Glenwood,MD