General confusion on lists and implication

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).

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.

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.

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.

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?

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.

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 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.

Gregg Kellogg
gregg@greggkellogg.net