Closed tanksha closed 1 month ago
Related to #127. As we discussed it is not a bug per se, because variables are replaced uniformly at least in the example from description. Anyway I will look at it to find out whether I can keep variable name in this case.
@tanksha could you please also give a link to the full example because I would like to understand why variable replacement breaks the code?
Example usage in the Pattern Miner work,
;; Define List
(: List (-> $a Type))
(: Cons (-> $a (List $a) (List $a)))
(: Nil (List $a))
;; Define DeBruijn Index
(: DeBruijn Type)
(: VarIdx (-> Nat DeBruijn))
;; Map a DeBruijn Index to an given variable
(: idx2var (-> DeBruijn (List Variable) Atom))
(= (idx2var (VarIdx Z) (Cons $head $tail)) $head)
(= (idx2var (VarIdx (S $k)) (Cons $head $tail)) (idx2var (VarIdx $k) $tail))
;; Map a DeBruijn Index in a given pattern to a variable
(: Debruijn2var (-> Atom (List Variable) Atom))
(= (Debruijn2var (VarIdx $k) $varlist)
(idx2var (VarIdx $k) $varlist))
(= (Debruijn2var $symbol $varlist)
(if (== (get-type $symbol) %Undefined%) $symbol (empty)))
(= (Debruijn2var ($link $first $second) $varlist)
($link (Debruijn2var $first $varlist) (Debruijn2var $second $varlist)))
The Debruijn index here is used to wrap the MeTTa Variables to make it easy for the synthesizer to do the unification. And during the match query, we unwrap them to variables and Debruijn2var function above is doing that.
(, (Debruijn2var (Inheritance (VarIdx Z) human) (Cons $Xvar (Cons $Yvar Nil)))
(Debruijn2var (Inheritance (VarIdx Z) man) (Cons $Xvar (Cons $Yvar Nil))))
returns
[(, (Inheritance $Xvar human) (Inheritance $X#311 man))]
Expected result, to be able to do pattern matching is,
[(, (Inheritance $Xvar human) (Inheritance $Xvar man))]
Probably it was fixed by #530 , I tried small example from description. @tanksha could you please check the pattern miner code.
Well, I should take my words back. Literally speaking example from description doesn't work because variable names returned are random but as I said before they are renamed uniformly. So to say whether it is an issue and how to fix it I still need to check the full example.
I would say it is an issue. For instance the following
;; Define foo
(: foo (-> Atom Variable Atom))
(= (foo Z $var) $var)
(= (foo (R Z) $var) (R (foo Z $var)))
;; Test
!(assertEqual (foo (R Z) $a) (R $a))
randomly fails, though you may need to run it several times before failing.
The same with the above (Debruijn example), its not consistent with each run it fails or passes the test. check the test here
I have tested both examples from https://github.com/trueagi-io/hyperon-experimental/issues/516#issuecomment-1911621862 and from https://github.com/trueagi-io/hyperon-experimental/issues/516#issuecomment-1912912179 using minimal MeTTa on a main
branch and both work. I still going to look at logs of the small example suggested by Nil to see how it works.
It seems to be reliably fixed with minimal MeTTa! :-)
I'll let you close, @vsbogd, since you wish to understand the how.
@vsbogd I tested with minimal metta and It works. Thank you!
reduced example