Re: Principle of Orthogonal Design(B

On Feb 7, 3:19 pm, David BL <davi..._at_iinet.net.au> wrote:
> On Feb 8, 4:43 am, Marshall <marshall.spi..._at_gmail.com> wrote:
> > On Feb 7, 3:46 am, David BL <davi..._at_iinet.net.au> wrote:
> > > On Feb 7, 6:44 pm, JOG <j..._at_cs.nott.ac.uk> wrote:
>
> > > A minor comment: when I see '$B"N(B' I assume it means all apparently free
> > > variables are in fact bound and are implicitly universally
> > > quantified.
>
> > As I understand it, this is conventional for all theorems and axioms,
> > whether there is an <=> in them or not.
>
> Perhaps. I've seen some people only drop explicit universal
> quantifiers when they use =>.
>
> I had thought the reason for introducing '$B"*(B' was to avoid this
> implicit universal quantification that was customary with '=>'.

Okay. I haven't run in to that before.

> > Well, at the very least we have to be careful to distinguish
> > the use of the equals sign between its use as the equality
> > relation and its use as name-binding.
>
> In a way I don't really see a fundamental distinction. I think the
> special syntax is needed to deal with variable names that are local to
> a sub-expression, because with implicit variable names on predicates
> we can get name clashes. These would be impossible to deal with if
> all variables had global scope.

If we substitute "lexical scope" for "sub-expression" in the above then I agree. I recoil from the idea of names that are local just to a specific sub-expression.

> > But yeah, there is a close relationship between variable names
> > and attribute names.
>
> As an example, we could think of
>
> x > y
>
> as a relation with attributes named x,y

Absolutely!

> If relation P has attributes y,z then the expression
>
> P & (x > y)
>
> could be regarded as shorthand for
>
> P(y,z) & (x > y)
>
> which can be regarded as join between two relations using common
> attribute y.

Yes yes!

> Suppose we want to project away y so only x,z are left in the result
> set. Then we use existential quantification on y:
>
> (Ey) (P(y,z) & (x > y))

Hmmm. That strikes me as weird--using existential quantification as projection. Is that your idea or is that more widely used?

Marshall Received on Fri Feb 08 2008 - 18:12:58 CET