feat: initial properties to test squiggle validity

This commit is contained in:
NunoSempere 2022-04-12 17:50:53 -04:00
parent ecfd8deece
commit bfae8b0e6d
4 changed files with 44 additions and 3 deletions

View File

@ -1,15 +1,17 @@
# Properties # Properties
Using `nix`. Where `o` is `open` on OSX and `xdg-open` on linux, Using `nix`. Where `o` is `open` on OSX and `xdg-open` on linux,
```sh ```sh
nix-build nix-build
o result/properties.pdf o result/property-tests.pdf
``` ```
Without `nix`, you can install `pandoc` yourself and run Without `nix`, you can install `pandoc` yourself and run
```sh ```sh
pandoc --from markdown --to latex --out properties.pdf --pdf-engine xelatex properties.md pandoc -s property-tests.md -o property-tests.pdf
``` ```
## _Details_ ## _Details_
The `properties.pdf` document is _normative and aspirational_. It does not document tests as they exist in the codebase, but somewhat represents how we think squiggle ought to be tested. The `properties-tests.pdf` document is _normative and aspirational_. It does not document tests as they exist in the codebase, but somewhat represents how we think squiggle ought to be tested.

View File

@ -0,0 +1 @@
pandoc -s property-tests.md -o property-tests.pdf

View File

@ -0,0 +1,38 @@
# Property tests for squiggle
Here are some property tests for squiggle. I am testing mostly for the mean and the standard deviation. I know that squiggle doesn't yet have functions for the standard deviation, but they could be added.
The keywords to search for are "[algebra of random variables](https://wikiless.org/wiki/Algebra_of_random_variables?lang=en)".
## Sums
$$ mean(f+g) = mean(f) + mean(g) $$
$$ Std(f+g) = sqrt(std(f)^2 + std(g)^2) $$
In the case of normal distributions,
$$ normal(a,b) + normal(c,d) = normal(a+c, sqrt(b^2 + d^2) $$
## Substractions
$$ mean(f-g) = mean(f) - mean(g) $$
$$ std(f-g) = sqrt(std(f)^2 + std(g)^2) $$
## Multiplications
$$ mean(f \cdot g) = mean(f) \cdot mean(g) $$
$$ std(f \cdot g) = sqrt( (std(f)^2 + mean(f)) \cdot (std(g)^2 + mean(g)) - (mean(f) \cdot mean(y))^2) $$
## Divisions
Divisions are tricky, and in general we don't have good expressions to characterize properties of ratios. In particular, the ratio of two normals is a Cauchy distribution, which doesn't have to have a mean.
## To do:
- Provide sources or derivations, useful as this document becomes more complicated
- Provide definitions for the probability density function, exponential, inverse, log, etc.
- Provide at least some tests for division
- See if playing around with characteristic functions turns out anything useful