LAWS.bend open laws/TODOs

raw source on the hub · import 0x53dde92df75268075f1bc6c33ecbb079/LAWS.bend as LAWS

bend-ml: machine learning in Bend 2. Parallel linear regression, batches, statistics, and metrics. https://github.com/LVTD-LLC/bend-ml

3 imports

import Base
import ./src/batch.bend as Batch
import ./src/linear_regression.bend as Linear

Laws

law prediction_count provedin PROOF.bendsource · line 9 · raw

@+model:0x53dde92df75268075f1bc6c33ecbb079/src/linear_regression.Model -> @+rows:0x53dde92df75268075f1bc6c33ecbb079/src/batch.Batch<F32> -> {0x53dde92df75268075f1bc6c33ecbb079/src/batch.count(F32, 0x53dde92df75268075f1bc6c33ecbb079/src/linear_regression.predict_batch(model, rows)) == 0x53dde92df75268075f1bc6c33ecbb079/src/batch.count(F32, rows) : Nat}

Structural guarantees only: these make no claims about F32 accuracy.

law rejects_empty_training provedin PROOF.bendsource · line 14 · raw

{0x53dde92df75268075f1bc6c33ecbb079/src/linear_regression.fit(0x53dde92df75268075f1bc6c33ecbb079/src/batch.Empty{}) == Fail{0x53dde92df75268075f1bc6c33ecbb079/src/linear_regression.NotEnoughSamples{}} : Result<&2, &2, 0x53dde92df75268075f1bc6c33ecbb079/src/linear_regression.FitError, 0x53dde92df75268075f1bc6c33ecbb079/src/linear_regression.Model>}