Re: General confusion on lists and implication

Dear Gregg,

I will try to answer some questions here.

> I’m hoping for some insight into the defined semantics of log:implies 
> and various list tests I’m working through. (Sorry, long email).
>
> Lists in N3 are a bit challenging (to me, anyway), as they have a dual 
> nature of first-class resources and first/rest ladders. In the first 
> case, when given a list in the antecedent, it can be considered to be 
> a constant of that formula, in the second, a pattern of existential 
> variables connecting to resources in the knowledge-base.
>
> The working definition of log:implies I’m working off is the following:
>
>     Logical implication is the relation between the antecedent
>     (subject) and conclusion (object) of a rule. The application of a
>     rule to a knowledge-base is as follows. For every substitution
>     which, applied to the antecedent, gives a formula which is a
>     subset of the knowledge-base, then the result of applying that
>     same substitution to the conclusion may be added to
>     the knowledge-base.
>
>
> (The definition in Notation 3 Logic is somewhat different).

Depending on how "substitution" is meant, the above is not that 
different from N3's semantics. If you assume universals to be quantified 
on top level, you can do what you say here. It is not clear for me what 
you do with blank nodes. If your substitution is only for non-nested 
blank nodes, you are again in line with our definition. For built-in 
functions you can now imagine that there is an infinite amount of 
additional triples implicitly stated in the knowledge base like for example

(1 1) math:sum 2.
(1 2) math:sum 3.
(1 3) math:sum 4.
etc.

and also

1 list:in (1 2 3 4 5).
2 list:in (1 2 3 4 5).
etc.


>
> So, this would imply that for an antecedent containing a list, that 
> that list must also be in the knowledge-base, but this may be a 
> misunderstanding of exactly what constitutes the knowledge-base, and 
> is inconsistent with tests.
OK, yes, here is the difference. As stated above, I would consider 
built-ins in a certain sense as some extra true triples in the knowledge 
base which you cannot all explicitly state since there is an infinite 
number of true triples (as you easily see with my sum example).
>
> On test taken from swap/test/list/last.n3 includes the following 
> implication:
>
>     { 1 list:in  (  1 2 3 4 5 ) } => { test4a a SUCCESS }.
>
>
> However, the containing (base) formula does not, itself, contain the 
> list (  1 2 3 4 5 ). This could be interpreted as 1 list:in  (  1 2 3 
> 4 5 )  being a constant, and the truth of the assertion is  true 
> without examining the knowledge-base, but it fails the requirement 
> that (after substitution), the antecedent formula is a subset of the 
> knowledge-base, or perhaps constants in the antecedent are inherently 
> parts of the knowledge base (or all patterns which become constant 
> after replacing variables with those already bound), but this would 
> seem to imply some merge process that I haven’t seen reference to.

So, I would say: everything which is explicitly stated in the knowledge 
base is true (as you also state) and for built-in functions everything 
which can be evaluated as true should also be considered true.

Your remark reminds me that I actually should also start to write down 
the semantics of built-ins, currently they are not in our semantics.

>
> Alternatively, the following is somewhat equivalent;
>
>     { 1 list:in  [rdf:first 1; rdf:rest ( 2 3 4 5 )] } => { test4a a
>     SUCCESS }.
>
>
> Except that here, but implicit blank node is considered as an 
> existential variable, and so must match something in the 
> knowledge-base, and is not itself a fact.

This is not true. If you have a blank node here it indeed needs indeed 
to be understood as an existentially quantified variable. If you would 
add explicit quantification, you would get:

{ ∃ :x. 1 list:in  :x. :x rdf:first 1; rdf:rest ( 2 3 4 5 ) } => { 
test4a a SUCCESS }.

This is actually the same as saying

∀ :x. { 1 list:in  :x. :x rdf:first 1; rdf:rest ( 2 3 4 5 ) } => { 
test4a a SUCCESS }.

And this can be translated back into

{ 1 list:in  ?x. ?x rdf:first 1; rdf:rest ( 2 3 4 5 ) } => { test4a a 
SUCCESS }.

which gives you the exact same problem as before.


Your question now makes me wonder how your substitution works (as 
mentioned above, it cold be in-line with our semantics definition). So 
some example:

How would you deal with

{_:x a :Unicorn}=> {:Unicorn a :existingSpecies.}.

Does your rule trigger for

1.  :tom a :Unicorn.

2. _:x a :Unicorn.

3. _:y a :Unicorn.

Your answer would help me to understand your intuition here. Maybe I can 
then also better explain in the spec how to deal with blank nodes 
(additionally to the definition).


>
> Another way to test this would be with the following:
>
>     (  1 2 3 4 5 ).
>
>     { 1 list:in  (  1 2 ?three 4 5 ) } => { :result :contains ?three }.
>
>
> Should this fire :result :contains 3. ? Is the the list a constant 
> including a variable, or is it a pattern to match a sequence of 
> statements in the knowledge-base?

The problem with your example case is that  (  1 2 3 4 5 ). is not a 
triple so it has no meaning (according to our semantics but also 
following Cwm's and EYE's interpretation). But what would indeed work 
with these two reasoners is:

    :greggsList :is (  1 2 3 4 5 ).

    {:greggsList :is ?list. ?list log:equalTo (  1 2 ?three 4 5 ). 1
    list:in  (  1 2 ?three 4 5 ) } => { :result :contains ?three }.

Here, both reasoners give you

     :result     :contains 3 .

This would also be in-line with our semantics (in how far it is 
defined). But I agree that this example is not that interesting any more 
since it would now also work without the list:in.

Another example could be

     { 1 list:in  (  1 2 ?three 4 5 ) } => { :test :is :successful}.

Here, EYE indeed derives

     :test :is :successful.

This is also what I would expect according to the semantics, Cwm does 
not give a result and I suspect that this is because the ?three is not 
specified.

>
> I have yet to get to a list:append implementation, which would 
> certainly be something that is intended to construct information not 
> already contained in the knowledge-base.

I would again say that all the true triples are implicitly in the 
knowledge-base, but for the case of append I would also recommend to 
have a look at Prolog. At least from my own experience I would say that 
append is one of the most important predicates there so you will find a 
lot of explanations how implementations deal with that function.


>
> Another hypothesis I’ve had some success with is not to treat the 
> resulting antecedent formula as something which must be a subset of 
> the knowledge-base, but to instead see if all of the universal 
> variables contained in the antecedent are bound after evaluation. This 
> (mostly) has the same affect, but allows the antecedent to contain 
> constant statements that aren’t, themselves, in the parent formula.

I am not entirely sure whether I understand you here. Would you think 
that corresponds to how I explained it above. From the logical point of 
view the formula should fire for all formulas which are known to be 
true. We know that everything which is explicitly stated in the 
knowledge base is true and from the definitions of the built-in 
functions we know which built-in triples are true.


>
> I think there’s a similar line or reason for formulae, themselves.
>
> For my part, it would be great if the semantics document clarified 
> this, in a way which is helpful to developers, such as myself. Much of 
> my implementation leverages the BGP matching, and builtin functions of 
> my SPARQL implementation. But, it’s been a bit of trial and error for 
> me thus far.
If you help me with the clarifications, I am willing to write it down. I 
just really need your help to understand possible problems since I come 
from the Prolog-worl which also means that I have an intuition for most 
of the functions and no "fresh" view any more.


I hope that at least some of my answers help you.

Kind regards,
Doerthe

-- 
Dörthe Arndt
Researcher Semantic Web
imec - Ghent University - IDLab | Faculty of Engineering and Architecture | Department of Electronics and Information Systems
Technologiepark-Zwijnaarde 122, 9052 Ghent, Belgium
t: +32 9 331 49 59 | e: doerthe.arndt@ugent.be