# Re: Distributivity in Tropashko's Lattice Algebra

Date: 16 Aug 2005 00:55:54 -0700

Message-ID: <1124178954.235852.266690_at_g14g2000cwa.googlegroups.com>

> 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

}

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 - 09:55:54 CEST