search

trueagi-io / hyperon-experimental

MeTTa programming language implementation
https://metta-lang.dev
MIT License
151 stars 49 forks source link

How to delay reduction until bindings are ready? #659

Open ngeiswei opened 7 months ago

ngeiswei commented 7 months ago

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

ngeiswei commented 3 months ago

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 commented 3 months ago

cargo run which runs Rust implementation, produces different result: 

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

I will try looking to it.

vsbogd commented 1 month ago

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 (0< $x) is calculated and it returns Error because < is a grounded operation and $x has no value yet.

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 commented 1 month ago

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 commented 1 month ago

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

On the one hand it is very similar to https://github.com/trueagi-io/hyperon-experimental/issues/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 commented 2 weeks ago

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 commented 2 weeks ago

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.