Re: Distributivity in Tropashko's Lattice Algebra

Marshall Spight wrote:
> 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

OK, I see. Notation is unimportant at this stage. Some remarks:

1. You of course know that a simple function application to the columns in the select clause would give you the same result.
2. If you'd like to get rid of the select clause and use join, than we are back to the problem of infinite relations since our function is materialized in the hypothetical database as a relation (unless you can suggest another way of implementing the join).
3. You may be interested to know that Oracle (as well as MS SQL Server) has so-called table functions. The table function behaves as if it were a real table. One can say for example "select a,b,c from t1 join table(f)". If the table(f) cardinality is infinite, the query of course will never complete. One can parameterize the "f" function in order to make its cardinality finite, but parameterizing won't work in general, obviously.