The very lazy λ-calculus and the STEC machine. In Proceedings of the 21st international conference on Implementation and application of functional languages (IFL'09), Springer-Verlag, Berlin, Heidelberg.My doctoral research at the Department of Information and Computing Sciences at the University of Utrecht has resulted in a number of scientific papers and a Ph.D. thesis about functional programming presented here. My work was part of the NWO project Realising Optimal Sharing, a collaboration between the Center for Software Technology and the Department of Philosophy. The project was lead by Doaitse Swierstra and Vincent van Oostrom. Most of my research is due to joint efforts with Clemens Grabmayer. Here are some of my contributions.
letrecThe substance of my Ph.D. thesis is from the previous three papers and is presented here in a more coherent narrative with supplementary explanations and examples. Note, that the formalisms in the thesis deviate to varying degrees from their original form in the papers.
Jan Rochel, 2016. The Unfolding Semantics of the λ-Calculus with letrec
letrecApplying bisimulation on term graph interpretations of λ-letrec yields two results: a generalisation of common subexpression elimination; and an efficient method to determine whether two λ-letrec-terms have the same unfolding.
[doi] Clemens Grabmayer, Jan Rochel, 2014. Maximal Sharing in the Lambda Calculus with letrec. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014. For the accompanying implementation, see below.
We study various representations for cyclic λ-terms as higher-order or as first-order term graphs. It is intended as a stepping stone for a follow-up paper about maximal sharing in λ-letrec.
[doi] Clemens Grabmayer, Jan Rochel, 2013. Term Graph Representation for Cyclic Lambda-Terms, Proceedings of the 7th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2013, Rome, Italy, 23rd March 2013
letrecAn unpublished paper which has as its main result a characterisation of the class of infinite λ-terms that are expressible finitely using the letrec-construct. It generalises results of a published paper (see below), in which the calculus has μ instead of letrec.
Clemens Grabmayer, Jan Rochel, 2012. Expressibility in the Lambda Calculus with letrec.
[doi] Clemens Grabmayer, Jan Rochel, 2013. Expressibility in the Lambda Calculus with μ. Proceedings of RTA 2013.
letrecAn optimisation that reduces the amount of β-reductions required to evaluate a term by lifting a certain kind of ‘constant’ parameters out of recursive positions. It is a generalisation of what is called the static argument transformation in GHC terminology.
[doi] Clemens Grabmayer, Jan Rochel, 2011. Repetitive Reduction Patterns in Lambda Calculus with letrec. Proceedings of TERMGRAPH 2011.
My first publication describes a very lazy evaluation strategy (lazier than lazy evaluation, hence the name) on a generalised λ-calculus. In this early paper of mine I embarrassingly reinvented the wheel multiple times (different wheel each time), namely generalised β-reduction and head occurrence reduction.
[doi] Jan Rochel, 2009. The very lazy λ-calculus and the STEC machine. In Proceedings of the 21st international conference on Implementation and application of functional languages (IFL'09), Springer-Verlag, Berlin, Heidelberg.
The suite comes with a technical report as documention, which is unfortunately hardly complete. But together with the API documentation and the example implementations it should be possible to get by. The source code of the SKI combinator implementation is documented in tutorial style.
Investigating different evaluators for the λ-calculus involves a lot of graph rewriting. It turned out that there is a lack of tools for specifying such systems and experimenting with them. Consequently I have implemented a suite of Haskell libraries and applications for interactive port graph rewriting, available on HackageDB:
LambdascopeJan Rochel <jan@rochel.info>
