What Is Control Flow Analysis for Lambda Calculus? – Iowa Type Theory Commute

Summary

Measure Functions and Termination of STLC Measure Functions and Termination of STLC In this episode, I talk about what we should consider to be a measure function. Such functions can be used to show termination of some process or program, by assigning a measure to each program, and showing that as the program computes, the measure decreases in some well-founded ordering. But what should count as a measure function? The context for this is RTA Open Problem 19, on showing termination for the simply typed lambda calculus using a measure function.Let's call this the start of season 7, because it seems about time for that.]]> In this episode, I talk about what we should consider to be a measure function. Such functions can be used to show termination of some process or program, by assigning a measure to each program, and showing that as the program computes, the measure decreases in some well-founded ordering. But what should count as a measure function? The context for this is RTA Open Problem 19, on showing termination for the simply typed lambda calculus using a measure function.Let's call this the start of season 7, because it seems about time for that.]]> Aaron Stump Buzzsprout-18193512 Fri, 14 Nov 2025 17:00:00 -0600 1302 7 1 full false