Skip to content

GitLab

Open
Created by Michael Hanus @mhOwner

Wrong solutions for combination of blackhole and non-determinism

Consider the following program:

main = let x = True ? fcase x of True -> False in x

With respect to the corrected natural semantics of FlatCurry, this defition has only one value: True. However, PAKCS computes both True and False as solutions before it enters an infinite loop:

blackhole> main
True
False
Prolog interruption (h for help)?

In contrast, the KiCS2 computes only the single value True before it enters the infinite loop.