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 th...
All content for Iowa Type Theory Commute is the property of Aaron Stump and is served directly from their servers
with no modification, redirects, or rehosting. The podcast is not affiliated with or endorsed by Podjoint in any way.
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 th...
Arithmetic operations in simply typed lambda calculus
Iowa Type Theory Commute
9 minutes
1 year ago
Arithmetic operations in simply typed lambda calculus
It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC). Church-encoded numbers can be given the simple type (A -> A) -> A -> A, for any simple type A. If we abbreviate that type as Nat_A, then addition and multiplication can both be typed in STLC, at type Nat_A -> Nat_A -> Nat_A. Interestingly, things change with exponentiation, which we will consider in the next episode.
Iowa Type Theory Commute
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 th...
