Ancestors

Toot

Written by Andrej Bauer on 2024-10-07 at 17:44

@jeanas @tito

The attribution about the discovery of the λ-calculus definition of predecessor in my realizability notes is mistaken (and now it has found its way into https://jean.abou-samra.fr/blog/science-amusante): it was Stephen Klenee, not Alfred Tarski, as documented at the bottom of page 56 of

Stephen C. Klene: Origins of Recursive Function Theory, IEEE Annals of the History of Computing, Jan.-Mar. 1981, pp. 52-67, vol. 3, https://doi.ieeecomputersociety.org/10.1109/MAHC.1981.10004

Let me fix the notes right away.

=> View attached media

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Descendants

Written by Andrej Bauer on 2024-10-07 at 19:30

@jeanas @tito Fixed: https://github.com/andrejbauer/notes-on-realizability/commit/0a161837161831650750a16cf0eda8636f84a278

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Written by Jean Abou Samra on 2024-10-07 at 17:53

@andrejbauer @tito Thanks for finding that! However, the purpose of the post was merely to have some fun (and distract myself from current geopolitical events which affect me indirectly) so the part of the quotation “Is programming the untyped 𝜆-calculus like pulling one's teeth out?” was important too.

=> More informations about this toot | More toots from jeanas@mathstodon.xyz

Written by Andrej Bauer on 2024-10-07 at 17:55

@jeanas @tito Sure, I appreciate your post! But still, one should not confuse Kleene and Tarski, and the humor is not decreased by a proper citation.

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Written by Jean Abou Samra on 2024-10-08 at 10:14

@andrejbauer @tito Thanks for correcting your notes. I've updated the quote accordingly. (I had (probably mis)understood that you were suggesting to change the post to quote Kleene directly instead.)

By the way, this might be a good opportunity for me to thank you for these notes: I've found it a bit difficult to find good sources on realizability, and this one has been the most helpful so far.

=> More informations about this toot | More toots from jeanas@mathstodon.xyz

Written by Martin Escardo on 2024-10-07 at 19:58

@andrejbauer @jeanas @tito

I thought everybody knew that Kleene solved this problem while he was in the dentist.

Edit. See e.g. https://iep.utm.edu/lambda-calculi/

=> More informations about this toot | More toots from MartinEscardo@mathstodon.xyz

Written by Martin Escardo on 2024-10-07 at 20:41

@andrejbauer @jeanas @tito

(This was not a joke, by the way.)

=> More informations about this toot | More toots from MartinEscardo@mathstodon.xyz

Written by Andrej Bauer on 2024-10-07 at 21:04

@MartinEscardo @jeanas @tito Yes, I thought it was general knowledge too, so imagine my shock when it turned out I confused Kleene and Tarski in my notes, and the confusion started propagating around the internet.

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Written by Cody on 2024-10-07 at 20:42

@MartinEscardo @andrejbauer @jeanas @tito I'd be trying to distract myself with hard problems if I was at the dentist in 1932 as well.

=> More informations about this toot | More toots from codyroux@mathstodon.xyz

Written by Yannick Forster on 2024-10-07 at 20:56

@MartinEscardo @andrejbauer @jeanas @tito I even believe I know for sure he specifically he got hid wisdom teeth extracted

=> More informations about this toot | More toots from yforster@types.pl