Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.prolog > #14254
| 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 | 2024-11-06 09:35 +0100 |
| Message-ID | <vgf9o4$i114$2@solani.org> (permalink) |
| 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> |
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.
>>
>
Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-17 05:18 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-17 06:37 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-17 07:00 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-17 13:28 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-31 02:59 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-31 03:04 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-31 03:10 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-31 10:18 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-08-31 10:22 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-09 16:06 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-09 16:12 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-09 16:13 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-09 16:14 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-09 23:57 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-09 23:59 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-12 05:11 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-12 10:46 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-12 10:48 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-12 13:22 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-13 05:53 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-13 07:32 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-13 11:16 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-13 11:18 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-13 11:36 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-13 13:28 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-14 01:41 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-14 01:43 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-14 07:41 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <janburse@fastmail.fm> - 2022-10-15 14:30 +0200
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-19 07:42 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-19 07:50 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-19 07:51 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-19 07:52 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-19 18:55 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-19 18:58 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-19 19:46 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-25 05:55 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-25 05:59 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-25 08:36 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-25 10:53 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-26 07:01 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-10-26 07:02 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-11-14 14:21 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-11-14 14:31 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-11-17 06:08 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2022-11-17 06:21 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-11 12:45 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-11 12:52 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-11 14:24 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-13 01:56 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-13 01:58 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-13 01:59 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-13 02:01 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-13 04:49 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-16 15:03 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-16 15:07 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-17 00:49 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-01-17 03:22 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-02-27 03:08 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-02-27 03:08 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-02-27 10:31 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-02-27 10:33 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-02-27 16:05 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-01 09:01 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-01 09:02 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-02 04:06 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-02 04:08 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-08 01:45 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-08 01:47 -0800
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-18 05:55 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-18 05:56 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-18 06:01 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-03-18 06:06 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-05-13 06:36 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-05-13 06:41 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mostowski Collapse <bursejan@gmail.com> - 2023-05-21 03:54 -0700
Differences among the "bomb" and "xbetween" (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-09-24 17:10 +0200
The issue with free speech Mild Shock <janburse@fastmail.fm> - 2024-10-09 15:29 +0200
failure of formal verification [software.imdea.org] (Was: The issue with free speech) Mild Shock <janburse@fastmail.fm> - 2024-11-06 09:33 +0100
Re: failure of formal verification [software.imdea.org] (Was: The issue with free speech) Mild Shock <janburse@fastmail.fm> - 2024-11-06 09:35 +0100
Re: failure of formal verification [software.imdea.org] (Was: The issue with free speech) Mild Shock <janburse@fastmail.fm> - 2024-11-06 09:37 +0100
variant_term/2 is faster than variant/1 (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-10-12 22:02 +0200
Re: variant_term/2 is faster than variant/1 (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-10-12 23:16 +0200
Re: variant_term/2 is faster than variant/1 (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-10-12 23:34 +0200
Re: variant_term/2 is faster than variant/1 (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-10-13 00:54 +0200
Re: Request for comments, Novacore the sequel to ISO modules Mild Shock <bursejan@gmail.com> - 2023-07-29 04:51 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mild Shock <bursejan@gmail.com> - 2023-09-07 17:15 -0700
Re: Request for comments, Novacore the sequel to ISO modules Mild Shock <janburse@fastmail.fm> - 2023-11-19 19:56 +0100
Re: Request for comments, Novacore the sequel to ISO modules Mild Shock <janburse@fastmail.fm> - 2023-11-19 19:59 +0100
Re: Request for comments, Novacore the sequel to ISO modules Mild Shock <janburse@fastmail.fm> - 2023-11-19 20:01 +0100
New milestone float formatting [LoL] (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-07-28 14:32 +0200
Re: New milestone float formatting [LoL] (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-07-28 14:38 +0200
Re: New milestone float formatting [LoL] (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-07-28 16:42 +0200
Re: Differences among the "bomb" and "xbetween" (Was: New milestone float formatting [LoL]) Mild Shock <janburse@fastmail.fm> - 2024-09-24 17:20 +0200
New milestone time formatting (Was: Differences among the "bomb" and "xbetween") Mild Shock <janburse@fastmail.fm> - 2024-09-26 13:22 +0200
More Prolog Improvement Proposals (PIPs) [PIP401 - PIP404] Mild Shock <janburse@fastmail.fm> - 2024-10-09 09:43 +0200
Even More Prolog Improvement Proposals (PIPs) [PIP301 - PIP303] (Was: More Prolog Improvement Proposals (PIPs) [PIP401 - PIP404]) Mild Shock <janburse@fastmail.fm> - 2024-10-09 09:45 +0200
Re: Even More Prolog Improvement Proposals (PIPs) [PIP301 - PIP303] (Was: More Prolog Improvement Proposals (PIPs) [PIP401 - PIP404]) Mild Shock <janburse@fastmail.fm> - 2024-10-09 10:00 +0200
Re: Even More Prolog Improvement Proposals (PIPs) [PIP301 - PIP303] (Was: More Prolog Improvement Proposals (PIPs) [PIP401 - PIP404]) Mild Shock <janburse@fastmail.fm> - 2024-10-09 11:22 +0200
A FFI for evaluable functions Mild Shock <janburse@fastmail.fm> - 2024-10-10 00:14 +0200
Name resolution is a blackbox (Re: A FFI for evaluable functions) Mild Shock <janburse@fastmail.fm> - 2024-10-10 00:16 +0200
plonk in discourse (Was: The issue with free speech) Mild Shock <janburse@fastmail.fm> - 2024-10-10 00:48 +0200
When do two Prolog terms marry? (Was: The issue with free speech) Mild Shock <janburse@fastmail.fm> - 2024-10-14 19:15 +0200
Re: When do two Prolog terms marry? (Was: The issue with free speech) Mild Shock <janburse@fastmail.fm> - 2024-10-14 19:22 +0200
native implementation of variant/2 can be fast (Was: When do two Prolog terms marry?) Mild Shock <janburse@fastmail.fm> - 2024-10-15 01:35 +0200
KISS principle pays off (Was: A FFI for evaluable functions) Mild Shock <janburse@fastmail.fm> - 2024-11-03 00:52 +0100
Waste of EU money / bread and butter of statistics (Was: failure of formal verification [software.imdea.org]) Mild Shock <janburse@fastmail.fm> - 2024-11-06 09:51 +0100
Re: Waste of EU money / bread and butter of statistics (Was: failure of formal verification [software.imdea.org]) Mild Shock <janburse@fastmail.fm> - 2024-11-06 10:09 +0100
Re: Waste of EU money / bread and butter of statistics (Was: failure of formal verification [software.imdea.org]) Julio Di Egidio <julio@diegidio.name> - 2024-11-06 10:43 +0100
SICStus Prolog is overrated (Was: Waste of EU money / bread and butter of statistics) Mild Shock <janburse@fastmail.fm> - 2024-11-06 12:57 +0100
Crashing under its own bloath, Scryer Prolog (Was: SICStus Prolog is overrated) Mild Shock <janburse@fastmail.fm> - 2024-11-06 13:03 +0100
“Luce,” which is Italian for “light.” (Was: Crashing under its own bloath, Scryer Prolog) Mild Shock <janburse@fastmail.fm> - 2024-11-06 13:12 +0100
More Poisened Meat balls? [NIVIDIA & OpenAI] (Way: “Luce,” which is Italian for “light.”) Mild Shock <janburse@fastmail.fm> - 2024-11-06 13:33 +0100
Re: More Poisened Meat balls? [NIVIDIA & OpenAI] (Way: “Luce,” which is Italian for “light.”) Julio Di Egidio <julio@diegidio.name> - 2024-11-06 14:17 +0100
Not all Red-Black Trees are Okasaki (Was: Request for comments, Novacore the sequel to ISO modules) Mild Shock <janburse@fastmail.fm> - 2024-11-07 00:59 +0100
Re: Request for comments, Novacore the sequel to ISO modules Mild Shock <bursejan@gmail.com> - 2023-11-19 10:54 -0800
csiph-web