~/bend-docscommunity

src/math/natural.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/src/math/natural.bend as Natural

2 imports
import Base
import ./pow2.bend as P2

Types

type MathError source · line 33 · raw

Data

type Bezout source · line 40 · raw

Data

the last nonzero remainder of the extended Euclid loop and its coefficient: a * coef == gcd (mod m)

type QuotRem source · line 44 · raw

Data

a // b and a % b

Definitions

def gcd_go source · line 50 · raw

@fuel:Nat -> @+a:Nat -> @+b:Nat -> Nat

Euclid's algorithm; b <= fuel throughout (every step lowers b).

def gcd source · line 59 · raw

@+a:Nat -> @+b:Nat -> Nat

def lcm source · line 62 · raw

@+a:Nat -> @+b:Nat -> Nat

def gcd_all_go source · line 71 · raw

@xs:List<&2, Nat> -> @+acc:Nat -> Nat

def gcd_all source · line 78 · raw

@xs:List<&2, Nat> -> Nat

def lcm_all_go source · line 81 · raw

@xs:List<&2, Nat> -> @+acc:Nat -> Nat

def lcm_all source · line 88 · raw

@xs:List<&2, Nat> -> Nat

def sum_go source · line 93 · raw

@xs:List<&2, Nat> -> @+acc:Nat -> Nat

def sum source · line 100 · raw

@xs:List<&2, Nat> -> Nat

def prod_go source · line 103 · raw

@xs:List<&2, Nat> -> @+acc:Nat -> Nat

def prod source · line 110 · raw

@xs:List<&2, Nat> -> Nat

def factorial_go source · line 115 · raw

@n:Nat -> @+acc:Nat -> Nat

def factorial source · line 122 · raw

@+n:Nat -> Nat

def perm_go source · line 126 · raw

@k:Nat -> @+m:Nat -> @+acc:Nat -> Nat

n * (n - 1) * ... * (n - k + 1)

def perm source · line 133 · raw

@+n:Nat -> @+k:Nat -> Nat

def comb_go source · line 138 · raw

@j:Nat -> @+n:Nat -> @+i:Nat -> @+r:Nat -> Nat

r_{i+1} = r_i * (n - i) / (i + 1): every r_i is C(n, i), so the division is exact (reference section 8.6).

def comb_small source · line 145 · raw

@+n:Nat -> @+k:Nat -> @+big:Bool -> Nat

def comb source · line 152 · raw

@+n:Nat -> @+k:Nat -> Nat

def bit_length_go source · line 157 · raw

@fuel:Nat -> @+n:Nat -> @+k:Nat -> Nat

def bit_length source · line 166 · raw

@+n:Nat -> Nat

def mid source · line 175 · raw

@+lo:Nat -> @+hi:Nat -> Nat

Binary search for the last r in [lo, hi) where the test holds, given it holds at lo and fails at hi (reference section 8.5 notes the float-sqrt shortcut is wrong above 2^52; this search is exact). more is lo + 1 < hi and ok is the test at the midpoint; the fuel bounds the halvings.

def pow_le_go source · line 180 · raw

@k:Nat -> @+r:Nat -> @+acc:Nat -> @+n:Nat -> @+ok:Bool -> Bool

r^k <= n without forming a product above n: ok is acc * r <= n, asked as acc <= n / r, and acc * r is only formed once it is known to fit.

def root_le source · line 189 · raw

@+n:Nat -> @+k:Nat -> @+r:Nat -> Bool

def search_go source · line 199 · raw

@fuel:Nat -> @+n:Nat -> @+k:Nat -> @+lo:Nat -> @+hi:Nat -> @+more:Bool -> @+ok:Bool -> Nat

the test is r^k <= n

def sqrt_next source · line 217 · raw

@+n:Nat -> @+g:Nat -> Nat

the largest r with r * r <= n, by Heron's (Newton's) iteration as in Lean 4 Mathlib's Nat.sqrt: g := (g + n / g) / 2 while that decreases g. Started from 2^(b/2 + 1) >= sqrt(n) (n < 2^b, b = bit_length(n)) it converges in O(log b) steps; the fuel g bounds the (strictly decreasing) steps.

def sqrt_iter source · line 220 · raw

@fuel:Nat -> @+n:Nat -> @+g:Nat -> @+m:Nat -> @+down:Bool -> Nat

def isqrt_from source · line 229 · raw

@+n:Nat -> @+g:Nat -> Nat

def isqrt source · line 232 · raw

@+n:Nat -> Nat

def iroot_k source · line 236 · raw

@+n:Nat -> @+k:Nat -> Nat

the largest r with r^k <= n (k >= 1)

def iroot source · line 245 · raw

@+n:Nat -> @+k:Nat -> Result<&2, &2, MathError, Nat>

def ilog_go source · line 254 · raw

@fuel:Nat -> @+n:Nat -> @+b:Nat -> @+k:Nat -> @+p:Nat -> @+up:Bool -> Nat

the largest k with b^k <= n: p is b^k, up is p * b <= n, asked as p <= n / b so no product above n is formed

def ilog_ok source · line 263 · raw

@+n:Nat -> @+b:Nat -> @+bad:Bool -> Result<&2, &2, MathError, Nat>

def ilog source · line 270 · raw

@+n:Nat -> @+b:Nat -> Result<&2, &2, MathError, Nat>

def pow_mod_odd source · line 277 · raw

@+m:Nat -> @+bit:Nat -> @+base:Nat -> @+acc:Nat -> Nat

right-to-left binary exponentiation, reducing mod m after every product: acc * base^e == b^e0 (mod m) throughout

def pow_mod_go source · line 284 · raw

@fuel:Nat -> @+m:Nat -> @+e:Nat -> @+base:Nat -> @+acc:Nat -> Nat

def pow_mod source · line 293 · raw

@+b:Nat -> @+e:Nat -> @+m:Nat -> Result<&2, &2, MathError, Nat>

def inv_step source · line 302 · raw

@+m:Nat -> @+q:Nat -> @+s0:Nat -> @+s1:Nat -> Nat

Extended Euclid on (m, a mod m) keeping only the coefficient of a, mod m: a * s0 == r0 and a * s1 == r1 (mod m). The remainders are gcd's.

def inv_go source · line 305 · raw

@fuel:Nat -> @+m:Nat -> @+r0:Nat -> @+s0:Nat -> @+r1:Nat -> @+s1:Nat -> Bezout

def inv_fin source · line 314 · raw

@+m:Nat -> @bz:Bezout -> Result<&2, &2, MathError, Nat>

def mod_inverse source · line 324 · raw

@+a:Nat -> @+m:Nat -> Result<&2, &2, MathError, Nat>

pow(a, -1, m): the x < m with a * x == 1 (mod m)

def divmod source · line 333 · raw

@+a:Nat -> @+b:Nat -> Result<&2, &2, MathError, QuotRem>

def clamp_ok source · line 340 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+bad:Bool -> Result<&2, &2, MathError, Nat>

def clamp source · line 347 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> Result<&2, &2, MathError, Nat>