Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: comp.lang.prolog
Subject: Re: failure of formal verification [software.imdea.org] (Was: The
 issue with free speech)
Date: Wed, 6 Nov 2024 09:35:17 +0100
Message-ID: <vgf9o4$i114$2@solani.org>
References: <db8a6771-3e54-485b-b391-310658dd6f52n@googlegroups.com>
 <aa869ef6-7f90-405b-a84a-2c11ac7979a3n@googlegroups.com>
 <vcukob$n3q2$1@solani.org> <ve60f6$6sl8$1@solani.org>
 <vgf9k7$i114$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 6 Nov 2024 08:35:16 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="590884"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:nAFf9P/bADexUDQQrhB1Cd2i0gE=
X-User-ID: eJwNyMEBwCAIA8CVRCDAOBFl/xHae54rBB0Gh/n4GPiEHWpZV+7O5YtdMQdKWYqz2dAu6p7KcEr/9WLM+K58TN8VsA==
In-Reply-To: <vgf9k7$i114$1@solani.org>
Bytes: 3835
Lines: 84

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.
>>
>