Semantics of Builtins
A builtin is a predicate (or a function symbol) with a fixed interpretation. This interpretation includes:
* A concrete domain.
For instance, ≤ can be interpreted over the domain of numbers and concat over the domain of strings.
* A concrete predicate over the above domain.
Satisfaction of an atomic expression that is based on a builtin is done with respect to the concrete domain with which this builtin is associated. For instance, the predicate corresponding to ≤ is going to contain the tuples of numbers of the form (a,b) such that a is less or equal than b (eg, (1,2), (3,3), etc.). Likewise, concat will be interpreted with a concrete predicate whose tuples are precisely the triples of strings of the form (s1,s2,s3) such that s3 is a concatenation of s1 and s2 (eg., (ab,cd,abcd)).
Some builtins may be polymorphic and have several associated domains. For instance, in the domain of strings, "<" can be viewed as lexicographics ordering and "+" as string concatenation. In that case, the proper interpretation of a builtin is determined by the arguments of the builtin predicate or function.
Note that while interpretations of non-builtin predicates can vary -- for instance, married(john,sally) can be true in one interpretation and false in another -- the interpretation of a builtin is always the same. For instance, 1 ≤ 2 is true at all times and 4 ≤ 3 is always false.
It is worth noting that the notion of negation as failure does not make sense in the context of a builtin predicate, and it is a frequent source of misconceptions. For instance, the statement naf (foo in http://example.com/foobar) is not using negation as failure in an appropriate way; it should be a statement with "classical" negation, neg (foo in http://example.com/foobar), whose truth is determined thus: The predicate in is a builtin. So, in(a, {a,b,c}) is always true and in(d,{a,b,c}) is always false (if d is not equal a, b, or c). This is because the interpretation of in is fixed and verification of in(x,y) does not involve any proof or failure to prove something. All that is needed is to look in a concrete relation that is always associated (in the same way) with the builtin.
RIF can support different sets of builtins. For instance, each builtin can be identified by an IRI, in which case support for SWRL, SPARQL, and XQuery builtins is feasible.
Note that, in general, satisfiability of a conjunction of builtin predicates may be undecidable. In RIF we should probably strive to allow only those sets of builtins for which satisfiability of conjunctive formulas is decidable.