Discussion of definitions in "Pre-logical relations" by Honsell and Sannella, particularly the notion of a lambda applicative structure (similar to a definition in John C. Mitchell's book "Foundations for Programming Languages').  In short, lambda abstractions get interpreted in combinatory algebras by compiling away the lambda abstractions in favor of S and K combinators, which are then interpreted by the combinatory algebra.  I complain about the fact that the definition of a lambda applicative structure is required to come with an interpretation function for terms (hence tying the semantics to the syntax).

Also known as the Fundamental Property, this is a theorem stating that for every well-typed term t : T, and every logical relation R between algebraic structures A and B, the meaning of t in A is related by R to the meaning of t in B.  I view it as a straightforward semantic soundness property, but where the semantics of types is this somewhat interesting one that interprets types as binary relations on structures A and B.  I muse on these matters a bit in the episode.

In this episode, I talk through a small (but intricate) example from a paper titled "Pre-logical relations" by Honsell and Sannella, showing that the set of logical relations is not closed under composition.  That is, you can have a logical relation between structure A and structure B, and one between B and C, but the composition (while a relation) is not a logical relation between A and C.  This took me three takes to get to where I wasn't tripping over my tongue, so enjoy.

Logical relations are the relational generalization of the algebraic concept of a homomorphism -- but they go further in extending the notion of structure-preservation to higher-order structures.  We discuss the basic definition in this episode.

Start of Chapter 10, on logical relations and parametricity.  Basic idea of logical relation as the relational generalization of the algebraic idea of homomorphism.  This is also the start of Season 2, as the fall academic year is just beginning here in Iowa.

The simplified version of Lamping's algorithm for optimal beta-reduction is discussed.  We have duplicators which eat their way through lambda graphs.  When copying a lambda abstraction, we send one duplicator down the variable port, and another down the body port.  When they meet, they cancel each other and the duplication is done.  But duplication can get paused waiting for a value to come in on a wire from outside the lambda abstraction.  This can lead to a situation where some other duplication needs to duplicate a lambda graph containing frozen duplicators.  Then we have to decide, when two duplicators meet, should they cancel each other (signalling the end of a duplication on one level), or should one duplicate the duplicators (for an outer duplication of some lambda graph containing frozen duplicators).  The abstract algorithm leaves this choice undetermined.  The hairy versions of the algorithm add complex additional machinery to keep track of these levels of duplication to resolve that nondeterminism.

I discuss some examples posted on my blog, QA9, which show that executables produced by ghc (the main implementation of Haskell) can exhibit non-optimal beta-reduction.  Thanks to Victor Maia for major help with these.

In this episode I talk about how to represent lambda terms as graphs with duplicator nodes for splitting edges corresponding to bound variables.  I also start discussing the beginning of Lampings' abstract algorithm for optimal beta-reduction, in particular how we need to push duplicators inside lambda abstractions to initiate a lazy duplication.

We discussed last time how with a graph-sharing implementation of untyped lambda calculus, it can happen that you are forced to break sharing and copy a lambda abstraction.  We discuss in this episode the central issue with doing that, namely copying redexes and copying applications which could turn into redexes following other beta reductions.  The high-level idea of the proposed solution is also discussed, namely lazy graph duplication.

Some background on optimal beta reduction: Levy, Lamping.  The main problem to overcome is duplicating a lambda abstraction that is used in two different places in your term.  The solution is to try to duplicate it incrementally.