RE: [BLD] Action on Uniterms in XML -- Proposed Poll

This email contains a proposed 'negation as silence' poll
(OK, it might not reach you in time or your response might
not reach me in time, but this discussion started at F2F9).
Proposed uniterm deadline: Friday, March 14, 12Noon EDT

I have been assuming an HLD (HiLog Dialect) that takes up
the neutrality of Hterms (Uniterms) in the W3C Submission
of SWSL-Rules: http://www.w3.org/Submission/SWSF-SWSL

The HiLog term ?Z(?X,a)(b,?X(?Y)(d)) there is serialized
according to our current BLD draft as shown below (as in
the previous examples, I omit "^^" types for simplicity):

	    <Uniterm>
	       <op>
	          <Uniterm>
	             <op><Var>Z</Var></op>
	             <arg><Var>X</Var></arg>
	             <arg><Const>a</Const></arg>
	          </Uniterm>
	       </op>
	       <arg><Const>b</Const></arg>
	       <arg>
               <Uniterm>
	           <op>
	             <Uniterm>
                      <op><Var>X</Var></op>
                      <arg><Var>Y</Var></arg>
	             </Uniterm>
	           </op>
	           <arg><Const>d</Const></arg>
	         </Uniterm>
             </arg>
	    </Uniterm>

The neutrality of that term permits to assign it to a
variable which can occur in other terms, where it will
be contextually interpreted by the HLD semantics.

Let me again use our smaller example, employing the
simplified XML-like presentation.

> > With uniterms, HLD also allows cross-contextual uses
> > such as
> > 
> > And ( ?x = Uniterm(f c d)
> >       Uniterm(a ?x e)
> >       ?x )
>
> You're doing stealth (implicit) reification here.  I strongly suggest
we
> don't do that.  I'd like reification (even before HiLog, maybe), but I
> want it to be explicit in the syntax.
>
> Something like:
>
>  And ( ?x = Uniterm(f c d)
>        Uniterm(a ?x e)
>        true(?x) )

This true operator, like John McCarthy's ist (is true)
operator would normally be considered as a modal operator
with an atomic rather than a term argument (no reification).
It has also been called 'holds', which I'd prefer since
this avoids confusion with the truth value true.

> > After two ?x substitutions this becomes
> > 
> > And ( ?x = Uniterm(f c d)
> >       Uniterm(a Uniterm(f c d) e)
> >       Uniterm(f c d) )
>
> I suggest, instead:
>
>  And ( ?x = Uniterm(f c d)
>        Uniterm(a Uniterm(f c d) e)
>        true(Uniterm(f c d)) )
>
> which the parser will understand as:
>
>  And ( ?x = expr(f c d)
>        atom(a expr(f c d) e)
>        true(expr(f c d)) )

With uniterms, HLD now allows:

And ( ?x = Uniterm(f c d)
      Uniterm(a ?x e)
      holds(?x) )

--substitutions-->

And ( ?x = Uniterm(f c d)
      Uniterm(a Uniterm(f c d) e)
      holds(Uniterm(f c d)) )

--contextual interpretation-->

And ( ?x = Expr(f c d)
      Atom(a Expr(f c d) e)
      holds(Atom(f c d)) )

Without uniterms, we'd need to perform some
Prolog-"call"-like Expr-to-Atom conversion:

And ( ?x = Expr(f c d)
      Atom(a ?x e)
      holds(Expr2Atom(?x)) )

--substitutions-->

And ( ?x = Expr(f c d)
      Atom(a Expr(f c d) e)
      holds(Expr2Atom(Expr(f c d))) )

--Expr-to-Atom conversion-->

And ( ?x = Expr(f c d)
      Atom(a Expr(f c d) e)
      holds(Atom(f c d)) )

I think we should limit the discussion about
this to Friday, March 14, 12Noon EDT, given
the few remaining weeks of Phase 1.
If no one wants to keep uniterms (I abstain)
then let's go with the atom/expression
distinction. You only need to email if you
want to keep uniterms (+1) or abstain (0).
I'll take silence as abandoning them (-1).

-- Harold


-----Original Message-----
From: Sandro Hawke [mailto:sandro@w3.org] 
Sent: March 12, 2008 1:56 AM
To: Boley, Harold
Cc: Public-Rif-Wg (E-mail)
Subject: Re: [BLD] Action on Uniterms in XML 


> This expands on the case for Uniterms in XML I made in
> today's telecon (ACTION-445).
> 
> -- Harold
> 
> 
> When moving upward the hierarchy of language extensions
> one should be allowed to reuse instance documents of
> less expressive layers unchanged as instance documents
> of more expressive layers.
> 
> E.g., when moving upward from Datalog to Horn logic,
> the function-free atomic Datalog terms should be legal
> as Horn logic terms, where function applications can
> then be added as well.

Absolutely.  We want to maximize overlap between dialects to maximize
reuse.  If two dialects can have a superset/subset relation in their
syntax, that very nice and simple.  (And, of course, for any given
document, its (observable) meaning should be the same in all dialects
for which it is syntactically valid.)

> Also, when moving upward from BLD to HLD (HiLog Dialect),
> the contextually differentiated BLD uniterms should be
> legal as HLD terms, where cross-contextual use is then
> permitted as well.
>
> If we don't use Uniterms with contextual differentiation
> but go back to an explicit Atom/Expr differentiation,
> such uniform instance-document reuse would be prevented.

I don't see how that is the case.

I see nothing about HiLog that says the parser is not allowed to tell,
when it comes across something like x(y), whether that is a
function-term or an atomic-formula.  Rather, as in HornLog, it should be
able to tell from where it is in the parse tree.   All I want is for
that information to also be in XML tag.

> In the following let's employ a simplified XML-like
> presentation, where <Element>c1 ... cN</Element> is
> transformed to Element(c1' ... cN'), with primes
> indicating recursive transformation.
> 
> Then, for example, a BLD instance document using facts
> of the form Atom(a Expr(f c d) e) could not be imported
> unchanged into an HLD instance document.

Why not?   I see no problem using that in HLD.

The difference between BLD and HLD, as I understand it, is that where
you have "a" and "f" in that example, in HLD the grammar would also
allow you to put a term or variable.  But the above formula would also
be perfectly legal.

> However, our current BLD with facts of the neutral form
> Uniterm(a Uniterm(f c d) e) could be imported unchanged
> into HLD.

I don't see how it helps.  The parse tree still tells you that the outer
Uniterm is an Atom and the inner Uniterm is a Term.   

> With uniterms, HLD also allows cross-contextual uses
> such as
> 
> And ( ?x = Uniterm(f c d)
>       Uniterm(a ?x e)
>       ?x )

You're doing stealth (implicit) reification here.  I strongly suggest we
don't do that.  I'd like reification (even before HiLog, maybe), but I
want it to be explicit in the syntax.

Something like:

 And ( ?x = Uniterm(f c d)
       Uniterm(a ?x e)
       true(?x) )

Perhaps "true" is not a good name for it.  Prolog calls it "call", which
sounds too procedural for BLD, I think.  Some prologs (including SWIPL
and XSB) allow you to just use a variable -- as you did -- saying it
means exactly the same thing as using "call".  The XSB 3.1 manual notes,
"the explicit use of call/1 is considered better programming practice."

> After two ?x substitutions this becomes
> 
> And ( ?x = Uniterm(f c d)
>       Uniterm(a Uniterm(f c d) e)
>       Uniterm(f c d) )

I suggest, instead:

 And ( ?x = Uniterm(f c d)
       Uniterm(a Uniterm(f c d) e)
       true(Uniterm(f c d)) )

which the parser will understand as:

 And ( ?x = expr(f c d)
       atom(a expr(f c d) e)
       true(expr(f c d)) )

To allow more syntax checking by the parser, and to allow tools (like
XTAN) to work without a full parse tree, I would like those tags in the
XML.

Note that the semantics of "true" are something like:
    true(expr(f c d)) iff atom(f c d)
or maybe:
    true(expr(f c d)) iff atom(f' c d)


> Since ?x = Uniterm(f c d) uses a neutral Uniterm, the
> first ?x substitution can be contextually interpreted
> as if it was Expr(f c d), and the second as if it was
> Atom(f c d):
> 
> And ( ?x =3D Uniterm(f c d)
>       Atom(a Expr(f c d) e)
>       Atom(f c d) )
> 
> Uniterm neutrality is particularly important for an
> interchange format.

Yeah, so I think that kind of reification, not flagged by anything
explicit in the syntax, is likely to make things harder for
implementors.

     -- Sandro

Received on Wednesday, 12 March 2008 22:41:04 UTC