search

well-typed / falsify

Other
38 stars 6 forks source link

Introduce a uniform `signedFraction` generator #67

Open edsko opened 12 months ago

edsko commented 12 months ago

The paper describes a way to generate signed fractions (Section 5.3), but the resulting generator will not be uniform in the range. @brunjlar proposes the following approach instead:

I think I have a relatively elegant solution for the problem, using the "Probability Integral Transform": https://en.wikipedia.org/wiki/Probability_integral_transform

First, we need to determine the CDF of your construction, i.e. the CDF of taking the minimum of two uniformely distributed random variables from [0,1], but that's easy:

P(min X Y < a) = 1 - P(x >= a && y >= a) = 1 - (1 - a)(1 - a) = 2a - a^2.

This also shows that I was right, and the minimum is NOT uniformly distributed. However, using the theorem from above link, we get that 

let m = min x y in 2 * m - m * m

IS uniformly distributed in [0,1]. Furthermore, f(a)=2a-a^2 is positive on [0,1], so this transformation is strictly monotonous increasing, which means that you still get the desired effect of being shrunk towards zero.

So to sum up, if I'm not mistaken, all you have to do is use your method from the library and the paper and then - instead of taking min X Y directly - apply f(a)=2a-a^2 to it.