You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
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
I tried to provide the simplest possible knowledge base, thus the moronic theory used here.
Expected behavior
It should output
Actual behavior
It outputs instead
Additional context
(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)))
.!(bc &kb (: $prf (0⍃' 2)) (S (S Z)))
, meaning that$x
is already grounded, then the backward chainer is able to find the proof.is-closed
in the body of0<
, as followsNotReducible
may help but I did not succeed so far.The text was updated successfully, but these errors were encountered: