It seems that Popper can't find a rule for increment by one
Closed this issue · 6 comments
I'm most likely making a rookie mistake, since this is my first encounter with Popper. I'm trying to make it synthesize an increment by one rule, i.e:
f(X, Y) :- plus(X, 1, Y).
I gave it this exs file:
pos(f(1, 2)).
pos(f(2, 3)).
pos(f(3, 4)).
pos(f(4, 5)).
this bk file:
one(1).
and this bias file:
max_vars(2).
head_pred(f, 2).
body_pred(plus, 3).
body_pred(one, 1).
type(one,(int,)).
type(plus, (int, int, int)).
direction(one,(out,)).
direction(plus,(in, in, out)).
The example Python script:
from popper.util import Settings, print_prog_score
from popper.loop import learn_solution
settings = Settings(kbpath='ex0')
prog, score, stats = learn_solution(settings)
if prog != None:
print_prog_score(prog, score)
outputs:
10:35:27 Searching programs of size: 3
or
10:21:31 SIZE: 1 MAX_SIZE: 40
10:21:31 SIZE: 2 MAX_SIZE: 40
10:21:31 SIZE: 3 MAX_SIZE: 40
10:21:31 SIZE: 4 MAX_SIZE: 40
10:21:31 SIZE: 5 MAX_SIZE: 40
10:21:31 SIZE: 6 MAX_SIZE: 40
10:21:31 SIZE: 7 MAX_SIZE: 40
10:21:31 SIZE: 8 MAX_SIZE: 40
10:21:31 SIZE: 9 MAX_SIZE: 40
when I use enable_pi.. What am I doing wrong?
Your target hypothesis has 3 variables (Popper needs one extra variable to represent the constant symbol 1), therefore you should increase the number of variables to at least 3:
max_vars(3).
Moreover, Popper currently does not support partial directions (see #31), therefore you should provide none or all of the directions, including directions for head predicates:
direction(f,(in,out)).
and the same with types:
type(f,(int,int)).
Then Popper learns the following hypothesis:
f(A,B):- one(C),plus(C,A,B).
Predicate invention (enable_pi) does not seem needed for this problem.
I changed the bias file to:
max_vars(3).
head_pred(f, 2).
body_pred(plus, 3).
body_pred(one, 1).
type(f, (int, int)).
type(one, (int,)).
type(plus, (int, int, int)).
The rest is unchanged. I'm getting:
Traceback (most recent call last):
File "/home/paul/st-python/prolog/popper-0.py", line 5, in <module>
prog, score, stats = learn_solution(settings)
^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/paul/st-python/prolog/.venv/lib/python3.11/site-packages/popper/loop.py", line 414, in learn_solution
timeout(settings, popper, (settings,), timeout_duration=int(settings.timeout),)
File "/home/paul/st-python/prolog/.venv/lib/python3.11/site-packages/popper/util.py", line 54, in timeout
result = func(*args, **kwargs)
^^^^^^^^^^^^^^^^^^^^^
File "/home/paul/st-python/prolog/.venv/lib/python3.11/site-packages/popper/loop.py", line 214, in popper
pruned_sub_incomplete = explain_incomplete(settings, generator, explainer, prog, directions, new_cons, all_handles, bad_handles, new_ground_cons)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/paul/st-python/prolog/.venv/lib/python3.11/site-packages/popper/loop.py", line 23, in explain_incomplete
for subprog, unsat_body in explainer.explain_totally_incomplete(prog, directions):
File "/home/paul/st-python/prolog/.venv/lib/python3.11/site-packages/popper/explain.py", line 132, in explain_totally_incomplete_aux
if self.tester.is_body_sat(order_body(body)):
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/paul/st-python/prolog/.venv/lib/python3.11/site-packages/popper/tester.py", line 159, in is_body_sat
return self.bool_query(query)
^^^^^^^^^^^^^^^^^^^^^^
File "/home/paul/st-python/prolog/.venv/lib/python3.11/site-packages/popper/tester.py", line 24, in bool_query
return len(list(self.prolog.query(query))) > 0
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/paul/st-python/prolog/.venv/lib/python3.11/site-packages/pyswip/prolog.py", line 128, in __call__
raise PrologError("".join(["Caused by: '", query, "'. ",
pyswip.prolog.PrologError: Caused by: 'plus(C,B,A),plus(C,A,B),!'. Returned: 'error(instantiation_error, context(:(system, /(plus, 3)), _1084))'.
The Prolog predicate plus/3 requires at least two of its arguments to be instantiated:
https://www.swi-prolog.org/pldoc/man?predicate=plus/3
Therefore, you should provide directions to ensure Popper never generates an hypothesis which raises such an instantiation error during its execution.
Thanks a lot. I misunderstood your comment about partial directions. It works fine now.
Is it possible to use + and is notation instead of plus(), in order to get a solution like this:
f(X, Y) :- Y is X+1.
Popper does not support the use of operators in this way.