Tuesday, 10 August 2010


Olivier Danvy's paper describing a rational deconstruction of the SECD machine is very interesting. It observes that if a machine uses lambda-abstractions to delay computations then this is equivalent, through a process called defunctionalization, to the use of stateful machine instructions and a separate auxiliary top-level interpreter. He uses this process to 'discover' the machine instructions of SECD. Effectively the free variables in the closures that are created in order to delay the computations are captured in data structures (the stateful instructions) that are subsequently fed to top-level functions. Defunctionalization was discovered by John Reynolds and, in a way, shows that higher-order functions are not fundamental to computation (a theory advocated  by Joseph Goguen). However, writing programs in a defunctionalized style would be a real pain because all lambdas would have to lifted to the top-level. So perhaps higher-order functions are fundamental to programming after all.