The beta-cube. A space of evaluation strategies for the untyped lambda-calculus

December 15, 2009

Álvaro García Pérez


The beta-cube. A space of evaluation strategies for the untyped lambda-calculus

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

Different evaluation orders for the untyped(1) lambda-calculus exists (call-by-value, call-by-name, normal order, applicative order…), reflecting the nuances in the evaluation of a system which serves as the foundation of functional programming languages.

In this talk, I will introduce a generic evaluator (written in Haskell) which can be instantiated to any evaluator realising a particular evaluation order. For this purpose, I will recall some notions of the untyped lambda-calculus, give an algebraic data type representing lambda-terms, present the big-step semantics of the evaluation orders using natural deduction rules, implement them (using CPS following Reynolds’ advice and showing alternative solutions in Haskell), show how monads can help to write neater code, present a way to hybridate existing evaluation orders to produce new ones, comment about an absortion theorem regarding hybridation and describe something I call the “beta-cube”.

(1) We prefer to use “untyped” rather than “pure” so as to avoid recent controversy regarding the latter word.