#computabilitytheory — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #computabilitytheory, aggregated by home.social.
-
#CS undergrads are taught #ComputabilityTheory—well, back in my day, at least. Regardless, every conscientious CS practitioner should study this foundational, almost-philosophical, subject. Of the many equivalent computational models, Turing's A Machine (augmented with von Neumann, Minskey, ...) and Church's 𝜆-Calculus (supplemented with Curry, Kleene, ...) are the ones commonly taught at the uni. Turing machine used to be the staple, back in the imperative 1980s. But FP-leaning modern students should study 𝜆-calculus, a simpler, more eloquent theory.
There are countless great textbooks on 𝜆-calculus, given its theoretical import and practical impact. Most are thick, heavy, dense. But the following are my favourite introductory-level lighter texts with a decidedly practical bent:
• An Introduction to Functional Programming through 𝜆-Calculus, Michaelson (the gentlest, detailed introduction)
• ML for the Working Programmer, Paulson (𝜆-calculus interpreter in ML)
• Programming Language Theory and its Implementation, Gordon (𝜆-calculus interpreter in LISP)
• The Implementation of Functional Programming Languages, Jones (compilation down to 𝜆-calculus)Use the above books to augment a university course, or to guide a self-study effort.
But please do not be swayed by the word "Introduction" in the title of Hindley's "𝜆-Calculus and Combinators: An Introduction" and reach for it right away, for it is intended as a comprehensive reference. And, most assuredly, do not dive head first into Barendregt's "The 𝜆-Calculus: Its Syntax and Semantics", which has been the final word on the subject for well over four decades.
A failure properly to control the knowledge 𝛿: that way lies heartburn and heartache.
-
#ComputabilityTheory is the normative ethics, #TypeTheory is the applied ethics, and #CategoryTheory is the meta ethics of #programming languages.
-
Many thanks to everyone who attended and made this an amazing day of #logic, #computabilitytheory and #categorytheory!
Recordings and slides will be available on the website sometime next week (hopefully)!
