In the formalization class I am teaching I am doing a class project on formalizing partial combinatory algebras https://andrejbauer.github.io/partial-combinatory-algebras/ (Isn't it a cool idea that the teacher should also do a class project?)
As expected, the genereralities, such as combinatory completeness, are easy. Defining concrete partial combinatory algebras is a whole different story, though. I got the graph model and the free combinatory algebra, but I shudder at the thought of defining Kleene's first and second algebras.
Is there a Lean formalization of partial recursive functions, with smn and utm theorems? That would be really helpful.
=> More informations about this toot | View the thread | More toots from andrejbauer@mathstodon.xyz
text/geminiThis content has been proxied by September (ba2dc).