Correction: the Correct Author of the Proof from Last Episode, and an AI flop
I correct what I said in the last episode about the author of the proof of FD from last episode based on intersection types. I also describe AI flopping when I ask it a question about this.
--------
7:10
--------
7:10
Krivine's Proof of FD, Using Intersection Types
Krivine's book (Section 4.2) has a proof of the Finite Developments Theorem, based on intersection types. I discuss this proof in this episode.
--------
21:35
--------
21:35
A Measure-Based Proof of Finite Developments
I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer. See also the write-up at my blog.
--------
23:24
--------
23:24
Introduction to the Finite Developments Theorem
The finite developments theorem in pure lambda calculus says that if you select as set of redexes in a lambda term and reduce only those and their residuals (redexes that can be traced back as existing in the original set), then this process will always terminate. In this episode, I discuss the theorem and why I got interested in it.
--------
15:54
--------
15:54
Nominal Isabelle/HOL
In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL, by Christian Urban. This paper shows how to reason with terms modulo alpha-equivalence, using ideas from nominal logic. The basic idea is that instead of renamings, one works with permutations of names.
Sverige