How to delay reduction until bindings are ready?

[ngeiswei]

Describe the bug

The backward chainer requires the interpreter to be able to delay reduction under certain conditions, such as the arguments are fully grounded.

To Reproduce

Run the following MeTTa script

;; Define Nat
(: Nat Type)
(: Z Nat)
(: S (-> Nat Nat))

;; Define greater than zero
(: 0< (-> Number Bool))
(= (0< $x) (< 0 $x))

;; Define backward chainer
(: bc (-> $a                            ; Knowledge base space
          $b                            ; Query
          Nat                           ; Maximum depth
          $b))                          ; Result
;; Base cases
(= (bc $kb (: $prf $ccln) $_) ; Kownledge base look-up
   (match $kb (: $prf $ccln) (: $prf $ccln)))
(= (bc $kb (: CPU (0⍃ $x)) $_) ; CPU check
   (if (0< $x) (: CPU (0⍃ $x)) (empty)))
;; Recursive step
(= (bc $kb (: ($prfabs $prfarg) $ccln) (S $k))
   (let* (((: $prfabs (-> (: $prfarg $prms) $ccln)) ; Recurse on proof abstraction
           (bc $kb (: $prfabs (-> (: $prfarg $prms) $ccln)) $k))
          ((: $prfarg $prms) ; Recurse on proof argument
           (bc $kb (: $prfarg $prms) $k)))
     (: ($prfabs $prfarg) $ccln)))

;; Define knowledge base
!(bind! &kb (new-space))
!(add-atom &kb (: 2 Prime)) ; 2 is a prime number
!(add-atom &kb (: Rule (-> (: $_ (0⍃ $x))   ; If $x is greater than 0
                           (-> (: $x Prime) ; and is a prime number, then
                               (0⍃' $x))))) ; $x is a prime number greater than zero

;; Test backward chainer
!(bc &kb (: $prf (0⍃' $x)) (S (S Z)))

I tried to provide the simplest possible knowledge base, thus the moronic theory used here.

Expected behavior

It should output

[(: ((Rule CPU) 2) (0⍃' 2))]

Actual behavior

It outputs instead

[]

Additional context

• MeTTa version: 0.1.8.dev36+g0e4b76e.d20240411, compiled with "minimal".
• Without "minimal", the output is
  (let* (((: $prfabs#34 (-> (: $prfarg#35 $prms#38) (0⍃' $x))) (bc GroundingSpace-0x2b472b8 (: $prfabs#34 (-> (: $prfarg#35 $prms#38) (0⍃' $x))) (S Z))) ((: $prfarg#35 $prms#38) (bc GroundingSpace-0x2b472b8 (: $prfarg#35 $prms#38) (S Z)))) (: ($prfabs#34 $prfarg#35) (0⍃' $x))).
• It should be noted that if the query is replaced by !(bc &kb (: $prf (0⍃' 2)) (S (S Z))), meaning that $x is already grounded, then the backward chainer is able to find the proof.
• It should also be noted that if the order of the premises is swapped, as in

  !(add-atom &kb (: Rule (-> (: $x Prime)       ; If $x is a prime number
                             (-> (: $_ (0⍃ $x)) ; and is greater than 0, then
                                 (0⍃' $x)))))   ; $x is a prime number greater than zero
  

  then it also find the proof. Unfortunately this ordering trick can not always be used for more intricate theories.
• Additionally I tried to wrap a conditional using is-closed in the body of 0<, as follows

  ;; Return True iff $x is closed
  (: is-closed (-> Atom Bool))
  (= (is-closed $x) (case (get-metatype $x)
                      ((Symbol True)
                       (Grounded True)
                       (Variable False)
                       (Expression (if (== $x ())
                                       True
                                       (and (let $head (car-atom $x) (is-closed $head))
                                            (let $tail (cdr-atom $x) (is-closed $tail))))))))
  
  ;; Greater than zero
  (: 0< (-> Number Bool))
  (= (0< $x) (if (is-closed $x) (< 0 $x) (empty)))
  

  but without success. I suppose a clever use of NotReducible may help but I did not succeed so far.

[ngeiswei]

Maybe one could solve that problem by supporting guards, as in functional programming (see https://downloads.haskell.org/~ghc/5.02/docs/set/pattern-guards.html). For instance, in my case, one could write

(=| (0< $x) (is-closed $x) (< 0 $x))

where =| would be like = but would take a guard as second argument.

[vsbogd]

cargo run which runs Rust implementation, produces different result:

[()]
[()]
[()]
[(Error (< 0 $x) < expects two number arguments)]

I will try looking to it.

[vsbogd]

First I would like to list what happens here and why it fails. First bc constructs complex proof recursively:

(bc &kb (: $prf (0⍃' $x)) (S (S Z)))
=> (bc &kb (: $prfabs1 (-> (: $prfarg1 $prms1) (0⍃' $x))) (S Z))
==> (bc &kb (: $prfabs2 (-> (: $prfarg2 $prms2)  (-> (: $prfarg1 $prms1) (0⍃' $x)))) Z)

At this point recursive call is matched with the first bc definition with the following variable values:

$prfarg2 ; no value
$prfabs2 <- Rule
$prms2 <- (0< $x)
$prfarg1 = $x
$prfabs1 ; no value
$prms1 <- Prime

bc returns (: Rule (-> (: $prfarg2 (0> $x)) (-> (: $x Prime) (0⍃' $x)))) and starts searching proof for $prms2 == (0< $x) which is the second let* condition:

(bc &kb (: $prfarg2 (0< $x)) Z)
=> (if (0< $x) (: CPU (0< $x)) (empty))
==> (< 0 $x)

Here in metta-repl (0< $x) is calculated and it returns Error because < is a grounded operation and $x has no value yet. In metta-python and metta-repl after #809 it returns unreduced (if (0< $x) (: CPU (0< $x)) (empty)) which is not matched with (: $prfabs (-> (: $prfarg $prms) $ccln)) and let* returns (empty).

Using is-closed definition doesn't work I believe because when is-closed returns False the whole branch is emptied by (if (is-closed $x) (< 0 $x) (empty)) and thus proof which were successfully found is removed from results.

[vsbogd]

Simple way of fixing it in this specific rule base is changing "CPU check" by removing proof only when we are sure the result is False:

(= (bc $kb (: CPU (0⍃ $x)) $_1) ; CPU check
   (case (0< $x)
     ((False (empty))
      ($_2 (: CPU (0⍃ $x))))))

This works successfully and returns:

[(: ((Rule CPU) 2) (0⍃' 2))]

[vsbogd]

I don't know how the proper general case fix show look like.

On the one hand it is very similar to #546 raised by Alexey. Following this logic (< 0 $x) could return True with adding a restriction on the value of $x. But on the other hand keeping such restrictions in variable bindings is not supported and supporting it means more execution logic is sneaking into a unification algorithm.

Another way is to code bc in a way which allows proving parts of the final proof in an arbitrary order. Thus if (< 0 $x) cannot be proved nor disproved at the moment then bc looks into another part of the final proof and returns to (< 0 $x) later. I think it is more promising approach in this specific case.

[rTreutlein]

This implements you suggestion of proving parts in arbitrary order. It might still fail if there are dependencies between multiple CPU terms. Do do that we would need a Set type where order of elements is always the same even if added in different order (so it stays unifiable).
Also tried just using an Expression instead of a List but without #546 that makes handle-prmlst harder to read.

;; ===== Type Definitions =====
;; Natural Numbers
(: Nat Type)
(: Z Nat)
(: S (-> Nat Nat))

;; Lists
(: List Type)
(: Nil List)
(: Cons (-> $a List List))

;; ===== Utility Functions =====
;; Greater than zero predicate
(: 0< (-> Number Bool))
(= (0< $x) (< 0 $x))


;; ===== Backward Chainer =====
(: bc (-> $a    ; Knowledge base space
          $b    ; Query
          Nat   ; Maximum depth
          $b))  ; Result

;; Base cases
(= (bc $kb (: $prf $ccln) $_)
   (match $kb (: $prf $ccln) (: $prf $ccln)))

(= (bc $kb (: CPU $check (0⍃ $x)) $_)
   (if (0< $x) (: CPU $check (0⍃ $x)) (empty)))

;; Recursive step
(= (bc $kb (: ($prfabs $prmlst) $ccln) (S $k))
   (let* (((: $prfabs (-> $prmlst $ccln))
           (bc $kb (: $prfabs (-> $prmlst $ccln)) $k))
          ($prmlst (handle-prmlst $kb $k $prmlst)))
     (: ($prfabs $prmlst) $ccln)))

;; ===== Parameter List Handler =====
(: handle-prmlst (-> $a $b List $d))
(= (handle-prmlst $kb $k Nil) Nil)
(= (handle-prmlst $kb $k (Cons (: $prfarg $prms) $xs))
   (Cons (bc $kb (: $prfarg $prms) $k) (handle-prmlst $kb $k $xs)))
(= (handle-prmlst $kb $k (Cons (: CPU $check $prms) $xs))
   (if $check
       ;; If check is true, evaluate CPU term first, then rest of list
       (Cons (bc $kb (: CPU $var $prms) $k) (handle-prmlst $kb $k $xs))
       ;; If check is false, evaluate rest of list first, then CPU term
       (let $xs (handle-prmlst $kb $k $xs)
            (Cons (bc $kb (: CPU $var $prms) $k) $xs))))

;; ===== Closure Check =====
(: is-closed (-> Atom Bool))
(= (is-closed $x)
   (case (get-metatype $x)
         ((Symbol True)
          (Grounded True)
          (Variable False)
          (Expression (if (== $x ())
                         True
                         (and (let $head (car-atom $x) (is-closed $head))
                              (let $tail (cdr-atom $x) (is-closed $tail))))))))

;; ===== Knowledge Base Setup =====
!(bind! &kb (new-space))
!(add-atom &kb (: 2 Prime))
!(add-atom &kb (: Rule (-> (Cons (: CPU (is-closed $x) (0⍃ $x)) (Cons (: $x Prime) Nil))
                          (0⍃' $x))))

;; ===== Test =====
!(bc &kb (: $prf (0⍃' $x)) (S (S Z)))

[vsbogd]

Do do that we would need a Set type where order of elements is always the same even if added in different order (so it stays unifiable).

It is not required to keep elements in some predictable order to make Set type unifiable. One can introduce a grounded type Set with custom match implementation which checks the sets are equal instead.