Friday, December 17, 2010

SECD, G-Machines, Combinatorial Machines and DOTs

I am wondering whether I should sit down and write down my musings on DOT evaluation, I once dubbed it the C-Machine, as a pun at the G-Machine and my target language C. Thing is, I devised it myself and don't really know what to think about it.

On first glance, it is just a reverse polish term rewrite system with eager semantics which is compiled down to a machine. It doesn't really make sense to see the DOT notation as a machine like SECD; for example, there is no code stack. On the other hand, it's not very complex, but there are a bunch of restrictions, invariants, and extra rules, which make it somewhat baroque for a notation.

Still, it is the simplest I could come up with, and it is a lot simpler than SECD or ZINC. It would make a lot more sense for people to, for instance, verify this simple scheme than a SECD machine which has its roots in Lisp and for which there are no real design rationale except for the fact that it works.

I also wonder whether SECD is faster by design, since lambda terms are mapped to it trivially (I guess), and I need the extra overhead of compiling down to combinators.

Moreover, why bother? I thought it might be fast, but at the moment, I overshot three performance metrics, code size, running time and memory consumption, each by a factor ten. Still, I am not sure that is the result of the scheme used. Or rather, the explosion seems to occur in the translation from combinators in Dot notation to abstract assembly, so, I probably messed up there. Does GHC still compile down to combinators internally?

No comments:

Post a Comment