Interchangeability of "facts" and "rules"

[nasser]

We are finding ourselves in situations where we have facts and rules with the same structure but querying them seems to be different. In particular we start out with concrete facts and abstract them into rules. We would like to be able to query a space for both facts an rules transparently -- what's the best way to do this?

Some examples

(father sally john)
(child john billy)

(= (father $a $b) (child $b $a))

! (match &self (father sally $x) $x)
;; [[john]]
! (let $q (father billy $x) (match &self $q $x))
;; [[john]]
! (let $q (father sally $x) (match &self $q $x))
;; [[]]

Would expect [[john]] for all, but I suppose the last one is empty because the let evaluates (father sally $x) to (child $x sally) which is not in the space.

(father sally john)
(child john billy)

;; (= (father $a $b) (child $b $a))

! (match &self (father sally $x) $x)
;; [[john]]
! (let $q (father billy $x) (match &self $q $x))
;; [[]]
! (let $q (father sally $x) (match &self $q $x))
;; [[john]]

As expected the second one is empty now, but the last one produces [[john]] because in the absence of a (father ...) rule the expression remains unevaluated and is passed as such to match.

Is my reasoning correct?

[Necr0x0Der]

Yes, your reasoning is correct. In the expression (let $q (father billy $x) (match &self $q $x)), $q will always be reduced to (child $x billy), because you have the corresponding equality (= (father $a $b) (child $b $a)), and thus (child $x billy) will be used for querying. In the expression, (match &self (father sally $x) $x), (father sally $x) will not be reduced, because match doesn't reduce its argument (pattern), because it is declared as having the Atom type.

There are different ways to mitigate this issue. Generally speaking, it's not a good idea to mix up functional and triplet representations. You may either have both declarative with additional inference rules, or both functional. In the latter case, you can write something like this:

(= (father sally john) True)
(= (child john billy) True)

(= (father $a $b) (child $b $a))

(= (if-true True $x) $x)
(= (if-true $_ $x) Empty)

! (if-true (father sally $x) $x) ;; [[john]]
! (if-true (father billy $x) $x) ;; [[john]]

I'm not advocating for this particular approach. It's just an example.