Re: cheating about reification

>Pat Hayes wrote:
>>  ...
>>  Right, but one would not use IEXT for reification. I introduced a
>>  REIF mapping from the syntax into IR, but one could do it more simply
>>  just by requiring IR to contain a suitable set of expressions, by
>>  semantic fiat, so that REIF is defined to be the identity.
>>
>>  >
>>  >What about the following addition to the MT. Let a ternary relationship
>>  >Reif be defined as:
>>  >
>>  >1) IR x IR x (IR union LV) <= Reif
>>  >2) If (x,y,z) in (IR union Reif) x IR x (IR union LV union Reif),
>>  >    then (x,y,z) in Reif
>>  >3) Reif is the smallest set with (1), (2)
>>  >
>>  >In other words, Reif contains all reified statements that can possibly
>>  >be constructed under a given interpretation I.
>>
>>  Right, that is almost the version I had at the F2F. (I used a mapping
>>  from the syntax into the domain, you use a three-place predicate
>>  defined recursively on the domain.) However, it was resoundingly
>>  criticized as not what reification actually means, in practice. (Dan
>>  C. told me that this was what reification *ought* to have been, but
>>  in fact it wasn't that.) I am still waiting to discover what
>>  reification actually is, in practice (as opposed to what the M&S says
>>  it is.)
>
>Maybe the confusion arose because in your original version reification
>mapped directly from the syntax. I must confess that I thought (and
>possibly other F2Fers did) that your definition treated reification as
>some kind of special syntactic mapping that needs to be established in
>addition to I.

Well, in a sense it is, though its an embedding rather than an 
interpretation (mention, not use!).

If I follow what Jeremy C. was saying in his whats-the-fuss-about 
message concerning reification, then *some* kind of embedding from 
the syntax seems to be essential, since the rdf:subject and 
rdf:object arcs both point and refer to the very pieces of syntax 
that are in the triple being reified. If we can find a way to avoid 
the use/mention confusion (and Im rapidly coming to think that we 
can, and it would be based on the same trick that we used to handle 
literal overloading, by allowing the objects of the reification arcs 
to be the nodes themselves, rather than what the node labels denote) 
then this would I think be able to handle reification in just the way 
that users intend it to be used. The resulting system would be a 
rather unorthodox logic, and the reification relations would have a 
very odd relationship to the syntax; but that is OK, since they do :-)

>Of course, from the logical perspective both approaches
>may well be equivalent. However, reification as defined above is easier
>to capture by people with limited background in logics like me. The
>above definition suggests that all reified statements always exist in
>each interpretation of a given set of statements.

Well....yes, IF we accept that IR satisfies the recursion theorems. 
BUt that seems like a very strong and unnecessary assumption. I 
prefer to leave the recursions in the syntax (where we have them 
anyway) and just say that there have to be enough 'things' in IR to 
stand for all the reified forms. You get the same set in the end, but 
you don't have to make so many assumptions about it.

>It's just that there
>is no a priori relationship between those reified thingies and the other
>resources in the domain of discourse. Then, special-purpose vocabularies
>like rdf:subject, rdf:object etc. could be introduced to define such
>relationship. I guess all this is obvious for you...
>
>>  >Now we have some
>>  >"thingies" to reason about. By the way, it can be shown that the set
>>  >Reif indeed exists, but the proof is non-trivial.
>>
>>  Its just a variation on Herbrand's theorem. If you want to get very
>>  strict, you need the second recursion theorem, I guess, but I'm
>>  willing to just accept that the syntax BNF has a minimal fixedpoint,
>>  and take that as read; after all, without that assumption, there
>>  isn't a language there to give a semantics to in the first place.
>
>Excellent! That makes life even easier. In fact, the proof that you
>suggest hints that reification is more like a mapping from some kind of
>syntax, supporting your point. Still, I think it has certain didactical
>benefits to settle reification directly within DD.
>
>Do you think it's worth a try to revamp reification in a manner similar
>to the above and sell it again to the WG? I'd support you, I promise ;)

Sure, lets give it a go. I need to get the current MT draft finished 
first, though. Friday morning approaches.....

Pat
-- 
---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Thursday, 25 October 2001 18:17:08 UTC