Floating point arithmetic

Stream: general

[Scott Morrison]

A student here has a lovely suggestion for a simple application of machine learning to automation. I’d love to try implementing it with her, but quickly realised that we’d need to do floating point arithmetic (just some gradient descent problems, so essentially inverting numerical matrices).

[Scott Morrison]

It seems the options would be:
1. Do this directly in Lean
2. Do it in C++, and have to compile our own branch of Lean to run it
3. Call external processes via the io monad

[Scott Morrison]

If anyone has advice or suggestions choosing between these, I’d love to hear.

[Simon Hudon]

Any chance that representing your numbers as fractions like Q does would be good enough?

[Simon Hudon]

The other idea I can think of is to use the C api to call a lean function that takes the float type and its operations as parameters.

[Simon Hudon]

In the second case, that means that you don't need your own branch of Lean which might make it easier to evolve along the successive versions of Lean

[Simon Hudon]

(deleted)

[Andrew Ashworth]

i would try and write it in C++ for now; when lean 4 rolls around there should be a ffi we can interface with

[Andrew Ashworth]

ironically it might be less work, since there's no notion of matrix computations in lean

[Mario Carneiro]

There is an experimental implementation of floating point arithmetic in data.fp.basic in mathlib. I'm not certain about all the modeling choices yet, especially considering how inconsistent hardware support is for floats, even when IEEE-conforming. I know Leo is also tackling this problem; the last version of the lean IR I saw supported floats at the low level, so I expect that Lean 4 will have a float datatype, and I'm not sure what he intends to do about the inconsistencies (probably just ignore them, but that means going meta which I'd like to avoid).

[Scott Morrison]

The other idea I can think of is to use the C api to call a lean function that takes the float type and its operations as parameters.

@Simon Hudon, where can I read about / see an example of the C api?

[Simon Hudon]

I don't know of any good documentation. Beside the source code, you could look at Joe Hendrix' Haskell binding for Lean: https://github.com/GaloisInc/lean-haskell-bindings/tree/master/src/Language/Lean/Internal

[Scott Morrison]

Maybe before I get started: I'm looking to write most of my tactic in Lean, and just farm out the numerics to C. Is this API suitable for doing that kind of thing? Or just for calling Lean from C?

[Simon Hudon]

I think just calling Lean from C should be sufficient. You can do a bit like the old IO interface and make a type class:

class float.interface :=
  (float : Type)
  (add : float -> float -> float)
  (mul : floal -> float -> float)
  -- ...

Then, on the lean side, all you need is variable [float.interface] at the beginning of the files that need access to float. On the C side, you create an instance and you call main with that instance as a parameter.

[Scott Morrison]

Okay, but I want to initiate all this running from inside the tactic monad. How do I even tell Lean about the existence of that C code?

[Simon Hudon]

I see, yeah, that's tricky. Maybe forking Lean would be easier for that

[Kevin Buzzard]

Would the Lean Mathematica interface be useful here?

[Kevin Buzzard]

[I don't really know what I'm talking about]

[Simon Hudon]

That sounds like a good idea to me. It might simplify things even more because matrix multiplication / inversion is already implemented in Mathematical