I got very curious about the EML paper.

The idea there is eml(x,y) = exp(x) - ln(y), and trees of this and the constant 1 can implement ~36 of the elementary functions sin(x) etc. It’s a bit like boolean logic gates for elementary functions.

I tried implementing it in Lean but ran into a limitation wherein Lean requires total functions, and some math functions are partial (e.g. ln(0) = 0 in Lean). I’m still not sure if it’s possible to implement the ideas from this paper in Lean Someone implemented this in Lean! tomdif/eml-lean They avoided the partiality because every argument to ln in an EML tree is an exp(…) and therefore always > 0. They also added some new things not present in the paper - some algebraic properties, calculus of EML, and more.

(n.b. the complex case gets trickier - something called a branch cut).

I thought a bit about implementing this as a gate unit in hardware using continuous analog components but I suspect that the numerical accuracy would be substantially less than what you could achieve by modeling these digitally (maybe on the order of only ~8 bits or less). Also, the EML paper gets i from ln(-1) = iπ, which then gives e^(ix) -> sin/cos. Voltages are real, so you’d need two wires per number (like I/Q in radio). But exp of a complex number a + ib is e^a (cos b + i sin b), so every EML cell would need sin/cos circuitry inside of it, which would be circular.

Still! I wonder if EML might have any applications!