The curious case of exponentiation in simply typed lambda calculus

Iowa Type Theory Commute

Contenido proporcionado por Aaron Stump. Todo el contenido del podcast, incluidos episodios, gráficos y descripciones de podcast, lo carga y proporciona directamente Aaron Stump o su socio de plataforma de podcast. Si cree que alguien está utilizando su trabajo protegido por derechos de autor sin su permiso, puede seguir el proceso descrito aquí https://es.player.fm/legal.

1+ y ago 7:29

MP3•Episodio en casa

Fetch error

Hmmm there seems to be a problem fetching this series right now. Last successful fetch was on November 14, 2025 23:41 (1M ago)

What now? This series will be checked again in the next day. If you believe it should be working, please verify the publisher's feed link below is valid and includes actual episode links. You can contact support to request the feed be immediately fetched.

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.

179 episodios

#Science #Tech #Math #Aaron Stump #Programming Language #Computational Logic #Type Theory #Proof Assistants #Cedille