Re: Distributivity in Tropashko's Lattice Algebra

vc wrote:

> Marshall  Spight wrote:
> > >
> > > The reason for this kind of infinity is the selection and rename
> > > definitions both of which rely on joining with infinite relations, the
> > > number of potentially required relations being infinite itself.
> >
> > The reason this doesn't bother me is that I believe the same
> > functionality can be had from functions. Functions can model
> > some infinite relations quite well. For example, the paper
> > mentions the infinite < relation, but the < function would
> > work just as well.
>
> Could you please provide an example of an algebraic expression where an
> infinite relation is replaced with  a function?  I am too exhausted by
> the symbol discussion to think of such example myself ;)

We have to consider some fairly specific features of a type system to permit us to do what I wish to do. However my expectation is that if I start throwing around tagged unions you will not be much put out.

Consider a definition of a function such that it is a mapping from values of one type to values of another. (Not very interesting so far.) Let us further suppose that these input and output types may be product types, where each attribute of the product is named and not ordered, similar to the definition of relations.
(This actually introduces some severe notational problems,
but let's ignore that for now.) Once we can express a function such that its domain and range are both product types, compatibly with the set-of-product type that is a relation, then we can consider the semantics of applying the join operator to two relations OR to a relation and a function. This is fairly straightforward. Note that we only have total functions so far; the cardinality of the input relation will equal (will determine, in fact) the cardinality of the result.

Now let us extend this idea a little bit and allow the range of the function to be a union type, specifically union of
(Nothing | Some producttype). We could call this a partial
function; it's only "defined" (that is, it only returns a product type) some of the time.

Here's a lame but illustrative example. Let's imagine a function f : (a:int, b:int -> Maybe root:float)

f = {
  if (a-b) >= 0)
    (root=sqrt(a-b))
  else
    Nothing
}

f is a partial function that returns the positive square root of the difference of a and b, if there is one.

Let R(a:int, b:int) = {
(5,1),
(8,-1),
(2,3),
(1,111)

}

Then we can calculate f join R

The result is:

(a:int, b:int, root:int) = {
(5,1,2.0),
(8,-1,3.0)

}

Does this make sense? I realize that f isn't strictly "infinite" because it is bound by the implementation of the int and float types, and possibly also by the size of memory, but it is at least no *more* bound than we would have been anyway for a given implementation of int or float. (That is, it introduces no limits the implementation didn't already necessarily have.)

I believe this approach to be mathematically sound and am working towards a notation, and I hope eventually an operational semantics for it. I have been working on it for quite some time; there is some chance it may actually be interesting when I am done. I am quite aware that the odds are against this.

Feedback welcome.

> Besides, I am not sure the function belongs to the NA (new algebra).

It may well not be any part of what Mr. Tropashko is thinking, but it is certainly part of the algebra that I am trying to construct,
(which has been greatly advanced by his paper.) One goal I have
for this algebra is that it be implementable, so it cannot allow constructs where we simply wave our hand and join with an infinite relation, however appropriate that may be for the mathematical point of view. I am (to my occasional dismay) not much of a mathematician, but I will claim to be a passable software engineer.

Marshall Received on Tue Aug 16 2005 - 02:55:54 CDT