Re: failure of formal verification [software.imdea.org] (Was: The issue with free speech)

Results of a fuzzer comparison:
library(nb_rbtrees) from 2014 in SWI-Prolog:
/* SWI-Prolog 9.3.14 */
?- L = [16,10,12,13,15,5,11,8,14,1,7,6,3,2,4,9], rb_new(T),
      (member(X,L), nb_rb_insert(T, X, true),
      fail; true), rb_display(T, 0).
$BLK 12-true
    $RED 5-true
       $BLK 2-true
          $BLK 1-true
             $NIL
             $NIL
          $BLK 3-true
             $NIL
             $RED 4-true
                $NIL
                $NIL
       $BLK 10-true
          $RED 7-true
             $BLK 6-true
                $NIL
                $NIL
             $BLK 8-true
                $NIL
                $RED 9-true
                   $NIL
                   $NIL
          $BLK 11-true
             $NIL
             $NIL
    $BLK 15-true
       $BLK 13-true
          $NIL
          $RED 14-true
             $NIL
             $NIL
       $BLK 16-true
          $NIL
          $NIL
On the other hand the rules by Okasaki give a
different resulting tree, which is better balanced,
has less overall depth and doesn’t have a root 12,
rather the root 8. Implementation based on change_arg/3:
/* Dogelog Player 1.2.5 */
?- L = [16,10,12,13,15,5,11,8,14,1,7,6,3,2,4,9], tree_new(T),
    (member(X,L), tree_set(T, X, true),
    fail; true), tree_display(T, 0).
$BLK 8-true
    $BLK 6-true
       $RED 3-true
          $BLK 1-true
             $NIL
             $RED 2-true
                $NIL
                $NIL
          $BLK 5-true
             $RED 4-true
                $NIL
                $NIL
             $NIL
       $BLK 7-true
          $NIL
          $NIL
    $BLK 12-true
       $BLK 10-true
          $RED 9-true
             $NIL
             $NIL
          $RED 11-true
             $NIL
             $NIL
       $RED 15-true
          $BLK 13-true
             $NIL
             $RED 14-true
                $NIL
                $NIL
          $BLK 16-true
             $NIL
             $NIL
I think Okasaki is the more common red-black
trees implementation, if I am not mistaken Java’s
method fixAfterInsertion() from the class TreeMap,
does also implement the Okasaki rules. Bug or
Feature that SWI-Prolog doesn’t use Okasaki?
Mild Shock schrieb:

So what is the spec. Well one can use:
 Red-Black Trees in a Functional Setting
https://www.cs.tufts.edu/~nr/cs257/archive/chris-okasaki/redblack99.pdf
 insert :: (Ord a) => a -> Tree a -> Tree a
insert x s = makeBlack $ ins s
   where ins E  = T R E x E
         ins (T color a y b)
           | x < y  = balance color (ins a) y b
           | x == y = T color a y b
           | x > y  = balance color a y (ins b)
         makeBlack (T _ a y b) = T B a y b
 The balancing would be as follows, again Haskell code:
 balance :: Color -> Tree a -> a -> Tree a -> Tree a
balance B (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
balance B (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
balance B a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
balance B a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
balance color a x b = T color a x b
 Does SWI-Prolog implement somewhere Okasaki red-black trees.
 Mild Shock schrieb:

Hi,
>
Not only are the fucking PIPs behind a
login wall that doesn't work:
>
Dictionaries in Prolog
https://gitlab.software.imdea.org/prolog-lang/pip-0102
>
I cannot read gitlab.software.imdea.org,
since it redirects to some internal server
during login.
>
Also formal verification doesn't have the
same track record as fuzzying. Take the SWI-Prolog
red-black trees. Are they really red-black trees?
>
I used fuzzy testing to find the test case.
Exhaustive enumeration of permutation seemed to
be out of reach computationally.
>
So I used these random permutations to find a
discrepancy in resulting tree depth:
>
fuzzer(R) :-
    numlist(1, 16, L),
    between(1, 1000, _),
    random_permutation(L, R).
>
Maybe the same technique can use to find smaller
discrepancies, and then use the smaller examples to
pin down difference in implemented balance
>
rules or implement rebalancing strategy.
>
Bye
>
Mild Shock schrieb:

@herme wrote:
>
Just a quick comment: note that you can make
and discuss the PIP proposals directly on
the PIPs discourse.
>
Here my response:
>
I will probably never go there since somebody
tried censoring my comments and said I don’t
work towards the Prolog cause. The good thing
about SWI-Prolog discourse, it has become
>
quite calm cocerning attempts to censor people,
possibly because some particular people left.
Which is in my opinion the best thing that
could happen to this forum. There is no
>
guarantee in other forums to really have free speech.
>

>