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
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