On 01/02/2018 11:41 PM, Linas Vepstas wrote:
So: English: "every sweep boat is a boat"
written in ASP: boat(BOAT) :- sweep_boat(BOAT).
written in Atomese:
Implication
Evaluation
Predicate "sweep_boat"
List
Variable BOAT
Evaluation
Predicate "boat"
List
Variable BOAT
Actually you'd have to use an ImplicationScope, not an Implication
Clearly Atomese is verbose.
Yes although due to eta-conversion between
(Lambda (Evaluation <predicate> <argument>))
and
<predicate>
this can be simplified into
Implication
Predicate "sweep boat"
Predicate "boat"
which PLN already supports.
% A boat is available if its not in use by any crew.
available(RACE, BOAT) :- racenum(RACE), crew(CREW), boat(BOAT),
not inuse(RACE, CREW, BOAT).
The first three clauses are "typechecking": the variable CREW must be of
type "crew", etc.
The last clause is a non-trivial constraint.
Implication
And
Evaluation
Predicate "racenum"
List
Variable RACE
Evaluation
Predicate "crew"
List
Variable CREW
Evaluation
Predicate "boat"
List
Variable BOAT
Not
Evaluation
Predicate "inuse"
List
Variable RACE
Variable CREW
Variable BOAT
Evaluation
Predicate "available"
List
Variable RACE
Variable BOAT
Correct with the exception again that it should be an ImplicationScope,
also the List over the unary arguments can be removed, so it becomes
ImplicationScope
And
Evaluation
Predicate "racenum"
Variable RACE
Evaluation
Predicate "crew"
Variable CREW
Evaluation
Predicate "boat"
Variable BOAT
Not
Evaluation
Predicate "inuse"
List
Variable RACE
Variable CREW
Variable BOAT
Evaluation
Predicate "available"
List
Variable RACE
Variable BOAT
Which is still verbose. However I believed it can be simplify that by
using Cartesian product (via ListLink) and
function-composition/beta-reduction (via PutLink). For instance
Lambda
Variable RACE
Variable CREW
Variable BOAT
And
Evaluation
Predicate "racenum"
Variable RACE
Evaluation
Predicate "crew"
Variable CREW
Evaluation
Predicate "boat"
Variable BOAT
is equivalent to
List
Predicate "racenum"
Predicate "crew"
Predicate "boat"
I don't think PLN supports that though, not yet.
I'm totally unclear on the performance profile for atomese. So, for
example: one could use the pattern matcher only, and implement naive
forward chaining. The statement "eight(sophie)" declares a fact
without any variables: "sophie" is an "eight", and since
"sweep_boat(BOAT) :- eight(BOAT)" then one run of the pattern matcher
will generate the fact that "sophie" is a "sweep_boat", and a second
pass will generate the fact that "sophie" is a "boat". Turning the
crank in this way will eventually generate every possible fact that can
be deduced.
This naive approach pollutes the atomspace with lots and lots of
redundant facts. In this particular case, its manageable: although a
combinatorial explosion is possible in principle, its absent in practice
(there are just barely enough boats for everyone, and sometimes not
enough - the problem is sometimes not satisfiable)
The forward chainer is supposed to avoid this pollution. I'm somewhat
unclear on how its actually implemented. I'm also unclear on the
backward chainer.
I don't think the forward chainer avoids this pollution. The backward
chainer does however, by only executing inference trees that can
possibly infer the target, and by only adding the proven targets to the
atomspace, not the intermediary results (well, users might want to
change that though).
The forward chainer is much less mature that the backward chainer, and
ultimately both should be unified into one elegant chainer that can go
both backward and forward (I more or less see how it should be done,
just need the time).
The ASP solver treats the assertions as a graph: In my infamous,
unfinished, unliked "sheaf" paper, the expression "available(RACE, BOAT)
:- racenum(RACE), crew(CREW), boat(BOAT), not inuse(RACE, CREW, BOAT)."
would be a "seed" (jigsaw-puzzle piece) having three connectors - BOAT,
CREW and RACE, and the task is to connect together all such "puzzle
pieces" to find the answer. The ASP solvers do this by pruning all
trivial, unidirectional connections (e.g. "sophie" is a "sweep_boat" is
trivial, since there are no conflicts that prevent the deduction of this
fact). After pruning all deductions that are not conflicting, what is
left is some tight knot of conflicting deductions, which the ASP solver
examines exhaustively, exploring every possible case. Then for each
possible solution, the trivial connections are reattached, and the
result is reported to the user. Bingo.
Oh, very much like a type checker engine in fact (where mutual recursive
functions form cliques of bidirectional connections). Unsurprisingly
since both are satisfyability solvers. Certainly one should be able to
emulate that sort of strategy with adequate inference control rules, not
sure how hard that would be though. But as efficient as it might be in
practice I suspect there are cases where open-ended inference can solve
the problem in a few steps while such a solver would take millions.
Nil
--
You received this message because you are subscribed to the Google Groups
"opencog" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/opencog.
To view this discussion on the web visit
https://groups.google.com/d/msgid/opencog/dd019e8c-844f-af68-572f-6a7c45de4613%40gmail.com.
For more options, visit https://groups.google.com/d/optout.
