The Stunner: Linear System T is Diverging!

Iowa Type Theory Commute

Вміст надано Aaron Stump. Весь вміст подкастів, включаючи епізоди, графіку та описи подкастів, завантажується та надається безпосередньо компанією Aaron Stump або його партнером по платформі подкастів. Якщо ви вважаєте, що хтось використовує ваш захищений авторським правом твір без вашого дозволу, ви можете виконати процедуру, описану тут https://uk.player.fm/legal.

3M ago 21:03

MP3•Головна епізоду

In this episode, I shoot down last episode's proposal -- at least in the version I discussed -- based on an amazing observation from an astonishing paper, "Gödel’s system T revisited", by Alves, Fernández, Florido, and Mackie. Linear System T is diverging, as they reveal through a short but clever example. It is even diverging if one requires that the iterator can only be reduced when the function to be iterated is closed (no free variables). This extraordinary observation does not sink Victor's idea of basing type theory on a terminating untyped core language, but it does sink the specific language he and I were thinking about, namely affine lambda calculus plus structural recursion.

My notes are here.

178 епізодів

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