search

curry-packages / prolog2curry

A tool to transform Prolog programs to Curry programs
BSD 3-Clause "New" or "Revised" License
1 stars 1 forks source link

Timeout with Curry program #2

Open william-vw opened 3 months ago

william-vw commented 3 months ago

Thanks very much for making this tool available (and your prior help with getting it to work :). I've been playing around with it a bit!

When converting simple "ancestor" Prolog rules:

ancestor(D, A) :- parent(D, P), ancestor(P, A).
ancestor(D, D) .

parent(c, b) .
parent(b, a) .

I get the following Curry code:

module Ancestor where

data Term = C | B | A
 deriving (Eq,Show)

ancestor d a | ancestor (parent d) a = True
ancestor d d = True

parent C = B
parent B = A

(It seems correct but I don't know enough about Curry to be sure ; e.g., it seems similar to the plus 0 y y example in the paper.)

When trying to run this using pakcs with query ancestor C A, the tool runs for a while and then returns without any output.

I tried using the online editor and got an explicit timeout with the following:

data Term = C | B | A
 deriving (Eq,Show)

ancestor d a | ancestor (parent d) a = True
ancestor d d = True

parent C = B
parent B = A

main = ancestor C A
mihanus commented 3 months ago

Thanks for the interesting example which addresses an issue on which I recently worked. Since PAKCS is based on Prolog, it uses backtracking search which is incomplete. If you execute this program with a complete search strategy, like KiCS2 or Curry2Go, then you get a result True (but, after that, it does not terminate due to the recursive ancestor call).

It is interesting that Prolog has a finite search space here. The reason is that parent produces failures which do not appear in the transformed Curry program due to its lazy evaluation. If it is evaluated strictly (call-by-value), then it has the same behavior. I mentioned in my ICLP'22 paper that a switch from Prolog to Curry might have an influence on the computed answers due to laziness. Very recently, I considered this again and realized that this change in computed answers occurs only if operations (after the transformation) are not totally defined. For instance, parent is not totally defined since it fails on parent A.

To get a transformation which keeps the set of computed answers, possibly failing computations in arguments must be strictly evaluated. This can be enforced with the predefined operator $! which applies a function after evaluating its argument. Thus, the transformed program is as follows:

data Term = C | B | A
 deriving (Eq,Show)

ancestor d a | (ancestor $! parent d) a = True
ancestor d d = True

parent C = B
parent B = A

With this version, even PAKCS has a finite search space.

All this can be implemented with a failure analysis and the package prolog2curry contains also a script https://github.com/curry-packages/prolog2curry/blob/master/scripts/pl2curry-failsensitive.sh for this "fail-sensitive" transformation (this script requires the installation of another Curry tool to analyze Curry programs for failures).

I hope this explanation helps.