Re: Expressions versus the value they represent

On Apr 12, 11:35 pm, Keith H Duggar <dug..._at_alum.mit.edu> wrote:
> On Apr 12, 7:09 am, David BL <davi..._at_iinet.net.au> wrote:
>
> > On Apr 12, 2:37 pm, Keith H Duggar <dug..._at_alum.mit.edu> wrote:
> > > Hopefully we can agree that since there is no interpretation defined
> > > in the RM nor FOL that there are not "multiple phases" nor "playing
> > > around" nor any other of the problems above.
>
> > Yes I agree with that, but I actually want to consider the problems
> > that arise under interpretations.
>
> Ok, cool. Thanks for this and the other clarifications. Now I'm
> a bit clearer on understanding what you are exploring. However,
> are we agreed that in the context of RM this is what we would
> call the "physical" layer?

I don't know if I fully appreciate what the "physical layer" means. I thought it had to do with database implementation details, such as memory and disk layout, hashing, B+Trees etc.

> For example, suppose that we define a particular interpretation
> that maps the ellipse and circle terms to particular structures
> say sets over which we define various other axioms (perhaps even
> including axioms referring to natural (as in physical world)
> observations.

I'm treating an interpretation (on a FOL) as a very formal concept. A set must be given over which quantification takes place, each function symbol must be associated with a particular function and each predicate symbol with a particular relation. An interpretation is parameterised by particular functions and relations that are pure mathematical abstractions that cannot be defined in terms of informal objects that exist in time and space.

> Then I would argue that even though these sets
> are not bits and bytes they are, none-the-less, "physical" in
> so far as the RM is concerned. Would you agree?

I would tend to say no although I'm not entirely sure what you mean. I would say all pure mathematical formalisms like the RM, FOL or a formal semantics over a FOL give us physical independence because they are mathematical formalisms divorced from the physical.

> > I think the problem is how to define a formal semantics, such that
> > under interpretation a relation or tuple is able to encode something
> > else (e.g. an image, string, triangulated surface etc). More
> > importantly, how is the equality operator which can be regarded as
> > predefined on relations and tuples somehow overridden to comply with
> > the interpretation? Also note that the RM operators are defined in
> > terms of equality of attribute values. So which version of equality
> > is used on RVAs?
>
> > An interpretation on nested terms is very simple and elegant.
> > Equality can be treated as a predicate symbol. How is an
> > interpretation defined on nested relations?
>
> Ok, let me make sure I understand this correctly by making up
> a concrete example. Suppose for example I have a relation with
> a DirectedGraph attribute where DirectedGraph is a relation
> valued attribute with header {NodeA : Node, NodeB : Node} under
> an interpretation "there is an edge from NodeA to NodeB".
>
> Now given those choices the question arises how to define
> "equality" because The RM already defines a strict equality
> for relations which would/could be applied to these RVAs but
> under our interpretation we may require that "equality"
> instead be defined as graph isomorphism.
>
> So it seems we have a problem of how to "override" the equality
> operator (say "=") such that it is consistent with our desired
> semantic interpretation.
>
> Is this what you mean?

Yes.

Consider a FOL term (call it T) that under interpretation represents a particular relation of type DirectedGraph. Let GRAPH be a function symbol of arity 1. Under interpretation let GRAPH(T) denote the graph represented by T. This unary function isn't 1-1 and nicely handles the "override" of equality. Indeed GRAPH represents none other than the canonical projection map of the equivalence classes according to graph isomorphism.

It would seem that the equivalent in the D&D RM would be to introduce a type named GRAPH and its selector function is the canonical projection map described above. Received on Tue Apr 13 2010 - 09:42:45 CEST