Re: [isabelle] 64-bit Java is 6x faster than 32-bit for a recursive fibonacci

On Fri, 16 May 2014, Gottfried Barrow wrote:

A starting point is to try to and find as many languages that perform good with recursive functions that use pattern matching.

You should look in the vicinity of ML and Haskell. The latter is particularly well-known to beat most other languages in the usual benchmarks.

If a recursive fibonacci function isn't relevant, then why is Isabelle/HOL filled with impractical recursive functions?

There is nothing impractical about recursion. The slowness of the naive fibonacci implementation is caused by the non-linearity of the invocation, which causes an exponential blowup. But the slightly tuned linear implementation demonstrates that the complexity is actually not there.

What is nice about a mathematical language like Isabelle/HOL is that you don't have to care about complexity. You just do symbolic reasoning, and you can e.g. make some equivalence proof of a term that represents the naive implementation to the tuned one. Then you give the latter to the code generator to run it on the machine.

I know that recursive functions are bad performers, and recursive functions with pattern matching are even worse.

This was disproven in the 1980s or so, when the first efficient implementations of ML came about. Recursion without pattern matching was already known to be efficient much earlier, in the olden days of LISP.

It is just due to technical accidents in C or Java that these guys are still lagging begind some decades. The Scala guys have to play a lot of funny tricks to cope with the tiny constant-sized stack on the JVM and lack of tail recursion.

In Poly/ML you can be relaxed about this, and allocate hundreds of MB or some GB of stack without too much worrying, or no stack at all if written slightly differently. But the art of tail-call optimization is often irrelevant these days.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.