fast fractional number computation

Stream: general

[Kendall Frey]

What's the fastest way to perform calculations involving fractional numbers? Specifically, I defined a complex number as a pair of rational numbers, and performed a Mandelbrot set test for 100000 iterations, which took several seconds. This is pretty slow, so what would be a better solution?

[Scott Morrison]

:four_leaf_clover:? (i.e. wait until Lean4 which will be much faster?)

[Scott Morrison]

How are you doing the calculation?

[Kendall Frey]

It's pretty simple, no thought to optimization.

def comp_rat := ℚ × ℚ

notation `ℂ` := comp_rat

def cadd : ℂ → ℂ → ℂ
| (r₁, i₁) (r₂, i₂) := (r₁ + r₂, i₁ + i₂)

def cmul : ℂ → ℂ → ℂ
| (r₁, i₁) (r₂, i₂) := (r₁ * r₂ - i₁ * i₂, r₁ * i₂ + r₂ * i₁)

[Kendall Frey]

I see mathlib has a floating point implementation, so I may try that one as well for comparison

[Reid Barton]

I assume you're using #eval (or equivalent lean --run)

[Kendall Frey]

lean --run, yeah

[Kendall Frey]

I tried native.float, but it generates errors like:

kernel failed to type check declaration 'x' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  native.float
elaborated value:
  3927 / 1250
nested exception message:
invalid definition, it uses untrusted declaration 'native.float'

Can this error be suppressed or ignored in some way?

[Bryan Gin-ge Chen]

You might have to put meta in front of your definitions?

[Mario Carneiro]

The problem with rational number arithmetic is that the denominators (and usually numerators as well) grow exponentially in the number of operations

[Mario Carneiro]

You probably want to do some heuristic rounding and interval arithmetic once the denominator gets large enough

[Mario Carneiro]

What is your actual mandelbrot set test? I only see the core add/mul operations in your snippet. In order to know what kind of rounding is appropriate I would like to know how exactly you are doing the mandelbrot set test