Open linas opened 1 year ago
For the output, the "full form" would be
(LinkValue ; set of all results...
(List ; list of left-right pairs
(List ; list of all left-var groundings
(List (Variable $left-var-1") (Atom gnd-in-right))
(List (Variable $left-var-2") (Atom another gnd-in-right)))
(List ; list of all right-var groundings
(List (Variable $right-var-1") (Atom gnd-in-left))
(List (Variable $right-var-2") (Atom another gnd-in-left)))))
This seems terribly verbose. Nasty-ugly verbose. Unusable from the usability perspective. So, a better variant would be to make it rewrite, just like a rule would:
(UnifierLink
(VariableList left-vars...)
left-expr
(VariableList right-vars..)
right-expr
result-expr)
where result-expr
can use any of the variables appearing in left-vars
or in right-vars
. Perhaps an even more natural form would be
(UnifierLink
(Lambda
(VariableList left-vars...)
left-expr)
(Lambda
(VariableList right-vars..)
right-expr)
result-expr)
The above seems to match what conventional books on proof write for a typed rule ... @ngeiswei any comments or corrections?
I do not understand the use-case for the unifier. I am guessing that it is this: There are two rules, written as RuleLink
s of the form
(Rule
(VariableList X ...)
(And
(Premise A)
(Premise B)
...)
(Conclusion F))
and similarly (Rule (VariableList Y...)(And (Premise C) (Premise D) ...) (Conclusion G))
Now, (I am guessing) you want to see if these two rules can be joined together. The chainer(s) try to figure out if (Conclusion F)
can be unified with (Premise C)
and use the unifier to try to figure this out, right?
The corresponding Unifier then has the form
(Unifier
(Lambda
(VariableList vars X ... that are in F)
(Conclusion F))
(Lambda
(VariableList vars Y... that are in C)
(Premise C))
(Rule
(Varible List X... Y...)
(And
(Premise A)
(Premise B)
...
(Premise D)
...))
(Conclusion G)))
So that a new RuleLink is constructed, without (Conclusion F)
or (Premise C)
in it, any more; but all the others remain, as before. Is this correct? Is this how the URE actually uses the unifier?
FYI @ngeiswei the demo https://github.com/opencog/unify/blob/master/examples/unifier-tree.scm provides an example of chaining together two rules, using "pure Atomese" (no C++ or scheme code). Note the chaining direction is ambiguous: it can be read as going either "forwards" and "backwards" .
Very cool work!
Thank you!
I mean, @ngeiswei you did all the hard work of making the unifier actually work. I did the easy part of slapping a coat of paint on the thing.
Provide an Atomese wrapper for Unify.
So, here's the deal:
(Unify A B)
is more or less the same thing as(Meet (Identical A B))
. However... There are some conceptual differences. Unify allows the form:where
left-vars...
are the things to be taken as variables inleft-expr
. There's nothing like this forIdenticalLink
orMeetLink
. We can almost get the same thing by writingexcept that this can fail if
(Variable "$X")
appears inleft-vars
, and also appears inright-expr
, but not inright-vars
. There is no way to handle this case in any kind of easy or natural way usingMeetLink
. And that is how Unify is different from(Meet (Identical ..))
The proposal is then to provide two forms: either a simple form, with no vardecls
or the full form, with vardecls.
Maybe also provide
(VariableListAuto)
which means "yank them out for me".What about the output? (next post)