Iowa Type Theory Commute

Latest Episodes:

Introduction to Logical Relations Aug 16, 2020

Show notes

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.

Lamping's abstract algorithm Jul 25, 2020

Show notes

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.

Examples showing non-optimality of Haskell Jul 14, 2020

Show notes

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.

Lambda graphs with duplicators and start of Lamping's abstract algorithm Jul 03, 2020

Show notes

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.

Duplicating redexes as the central problem of optimal reduction Jun 20, 2020

Show notes

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.

Introduction to optimal beta reduction Jun 16, 2020

Show notes

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.

Lexicographic termination Jun 02, 2020

Show notes

Many termination checkers support lexicographic (structural) recursion. The lexicographic combination of orderings on sets A and B is an ordering on A x B where a pair decreases if the A component does (and then the B component can increase unboundedly) or else the A component stays the same and the B component decreases. Connections with nested recursion and ordinals discussed.

Mendler-style iteration May 18, 2020

Show notes

Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration. On this approach, we write recursive functions by coding against a certain interface that features an abstract type R, which abstracts the datatype over which we are recursing; and a function from R to the result type of the recursion. Subdata of the input data are available at type R only, not at the original datatype. This allows us to make explicit recursive calls, but only on subdata.

Well-founded recursion May 18, 2020

Show notes

Well-founded recursion is a technique to turn recursion which decreases along a well-founded ordering into a structural recursion.

Compositional termination checking with sized types Mar 30, 2020

Show notes

Discussion of a compositional method of termination checking using so-called sized types. Datatypes are indexed by sizes, and recursive calls can only be made on data of strictly smaller size than the data as input to the recursion. Since the method is type-based, it is compositional: we can break out helper functions from a recursive function and not upset the termination checker. A readable and interesting tutorial on the subject is here.

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected