Re: Understanding Logics with Aggregate Operators

From: Jan Hidders <hidders_at_gmail.com>
Date: 26 Jan 2007 06:01:16 -0800
Message-ID: <1169820075.986951.58340_at_v45g2000cwv.googlegroups.com>


On Jan 25, 11:06 pm, "arthernan" <arther..._at_hotmail.com> wrote:
> I agree with the saying "go to the source". So I did. I do database
> programming for a living. And I want to know what else is out there,
> that is based in formal methods. I just hear that there is all this
> great research already done and we are not using it.
>
> Aggregates seem to be one missing piece in most logic description
> languages. So I decided to look up articles in the subject and I found
> this one.
>
> Logics with Aggregate Operators. (2000) (Lauri Hella).
>
> I read the first four pages just fine, but I am stuck (for now) on page
> 5. Anyway here is my problem:
>
> Notes: 1)The link to the original PDF article is at the bottom. 2) The
> symbol φ in case it's hard to read here is the Greek letter phi)
>
> I'm not sure what this formula means
>
> t(x) = y.φ(x,y) (x and y have a vector sign on top of them)
>
> And then from there I think I am also missing.
>
> Aggr f y.(φ(x,y),t(x,y))
>
> I don't think I know which one is the free variable.

The direct answer to that question is "the variables in x (which is a vector of variables)".

I'll try to explain a bit more. Note that they are inductively defining what the formulas in the logic are, and as part of that they are definiting here terms and in particular terms of the second sort, i.e., terms that evaluate to a number. So things like "1" or "1 + 2" or "1 - x" (if x is of the second sort).

Since aggregation operations also return a number they can also be used to construct a term. For example, from the formula

  R(x1,x2, y1, y2) AND x1>x2

we can construct

  # (y1,y2) . R(x1,x2, y1, y2) AND x1>x2

which counts the number of pairs (y1,y2) such that the formula R(x1,x2, y1, y2) AND x1>x2 holds. Clearly its result is defined if you know R and the values of x1 and x2, so this is a term with free variables x1 and x2. Observe that this term can be used in a formula in any place where a number is expected. So, the following is a valid formula:

  5 = # (y1,y2) . R(x1,x2, y1, y2) AND x1>x2

The case for other aggregation operators is analogous.

Hope that helped,

  • Jan Hidders
Received on Fri Jan 26 2007 - 15:01:16 CET

Original text of this message