Incomplete substitutions in (composite) queries

[Necr0x0Der]

For the program

(implies (Frog $x) (Green $x))
(implies (Frog $x) (Eats-flies $x))
(Frog Sam)
(Robot Sophia)

the result of the query

!(match &self
  (, (Frog $x)
     (implies (Frog $x) $y))
  $y)

is correct ([(Green Sam), (Eats-flies Sam)]). However, if the query expressions are swapped

!(match &self
  (, (implies (Frog $x) $y)
     (Frog $x))
  $y)

then the output is [(Green $x-23), (Eats-flies $x-24)].

Also, the query

!(match &self
    (, (implies ($P $x) (Green $x))
        (implies ($P $x) (Eats-flies $x)))
    ($x is definitely $P))

returns [($x-73 is definitely Frog)], which is not incorrect, because $x remains unbound, but could the final result of match restore original variables? There are tricky situations, e.g.

(equals $x $x)
!(match &self
    (equals $y $z)
    ($y $z))

should not return ($y $z). Ideally, it should return ($y $y). Now, it returns ($x-96 $x-96), which is ok, but not always convenient. Possibly, this is connected with the main issue, but if not, we can leave it as is for now.

[Necr0x0Der]

b2_backchain.metta contains other examples with incomplete bindings - check (ift (deduce (Evaluation (mortal $x))) $x) and (explain (Evaluation (mortal $x))). Interestingly, in b3_direct.metta ift works in (ift (green $x) $x) (line 21).

[vsbogd]

Issue with unbounded variable names is partially connected to the first example but mainly it is a separate issue. It is caused by the fact that when both query and atom has variable in the same position the query's variable is grounded by the atom variable. This logic allows us propagate value of $then in (= (if T $then) $then) when it is matched with (= (if T (do-something)) $X) during interpretation. Finally $X bound to (do-something) because $X is bound to $then and $then is bound to (do-something).

[vsbogd]

I almost resolved the issue, but this example is tricky:

(equals $x $x)
!(match &self
    (equals $y $z)
    ($y $z))

I can implement it as suggested but there is a conflict with current interpreter code. It matches expressions like (= .... $%X%) and when it executes:

(= (plus Z $y) $y)
!(plus Z $n)

then matcher returns bindings {$n: $%X%} interpreter cannot find value for $%X%. Internally matcher knows that both $n and $%X% are equal but it doesn't have reason to prefer expressing $%X% via $n or vice versa. Situation may be even worse when more than two variables are equal for example when matching ($a $a $a) with ($x $y $z).

I see two solutions for this issue:

• change API and return information about variable equality, then when one is asking about value for $%X% $n can be returned as an answer and vice versa; actually I am almost sure it should break current code for examples when binding like { $x = $y } is applied to atom ($x $y) and $x is replaced by $y and $y is replaced by $x with result ($y $x).
• introduce new variable and assign both $n and $%X% this variable as a value.

[Necr0x0Der]

Some cases still don't work. Need to analyze them in more detail.

[vsbogd]

Do you mean variable substitution, or other matching cases?

[vsbogd]

I propose closing this after merging #245 because now variables equalities are explicitly represented in Bindings.

[Necr0x0Der]

I propose closing this after merging #245 because now variables equalities are explicitly represented in Bindings.

Well, from the MeTTa-user side,

(equals $x $x)
!(match &self
    (equals $y $z)
    ($y $z))

still returns ($z $y). Do you mean that it is possible to recover equalities for $z and $y? I wonder how to do this better...

This example

(implies (Frog $x) (Green $x))
(implies (Frog $x) (Eats-flies $x))
(Frog Sam)
(Robot Sophia)

!(match &self
    (, (implies ($P $x) (Green $x))
       (implies ($P $x) (Eats-flies $x)))
    ($x is definitely $P))

in the initial comment seems to be not precise. $x should not be bound to Sam in it. If we replace the query with

!(match &self
    (, (implies ($P $x) (Green $x))
       (implies ($P $x) (Eats-flies $x))
       ($P $x))
    ($x is definitely $P))

then we get what we want: (Sam is definitely Frog). Thus, "incomplete substitutions in composite queries" seems to be solved, indeed. I wonder why (ift (deduce (Evaluation (mortal $x))) $x) still doesn't work, but it might be another issue.

[vsbogd]

Do you mean that it is possible to recover equalities for $z and $y?

Yes, they are encoded inside bindings. Yes it is interesting question if we can extract this fact from bindings. But in any further evaluation if one of this variables will get value then another will get the same value.