Iowa Type Theory Commute

The curious case of exponentiation in simply typed lambda calculus


Listen Later

Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC).  But surprisingly, the type is non-uniform.  If we abbreviate (A -> A) -> A -> A as Nat_A, then exponentiation, which is defined as \ x . \ y . y x, can be assigned type Nat_A -> Nat_(A -> A) -> Nat_A.  The second argument needs to have type at strictly higher order than the first argument.  This has the fascinating consequence that we cannot define self-exponentiation, \ x . exp x x.  That term would reduce to \ x . x x, which is provably not typable in STLC.  

...more
View all episodesView all episodes
Download on the App Store

Iowa Type Theory CommuteBy Aaron Stump

  • 5
  • 5
  • 5
  • 5
  • 5

5

17 ratings


More shows like Iowa Type Theory Commute

View all
Software Engineering Radio - the podcast for professional software developers by se-radio@computer.org

Software Engineering Radio - the podcast for professional software developers

272 Listeners

This American Life by This American Life

This American Life

90,587 Listeners

Planet Money by NPR

Planet Money

30,971 Listeners

CppCast by Phil Nash & Timur Doumler

CppCast

109 Listeners

Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas by Sean Carroll | Wondery

Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas

4,128 Listeners

Algorithms + Data Structures = Programs by Conor Hoekstra, Bryce Adelstein Lelbach & Ben Deane

Algorithms + Data Structures = Programs

31 Listeners

The Ezra Klein Show by New York Times Opinion

The Ezra Klein Show

15,313 Listeners

The Array Cast by The Array Cast

The Array Cast

34 Listeners

The Haskell Interlude by Haskell Podcast

The Haskell Interlude

11 Listeners

The Weekly Show with Jon Stewart by Comedy Central

The Weekly Show with Jon Stewart

10,252 Listeners

The Rest Is Politics by Goalhanger

The Rest Is Politics

3,110 Listeners

Oxide and Friends by Oxide Computer Company

Oxide and Friends

47 Listeners

Developer Voices by Kris Jenkins

Developer Voices

21 Listeners