Ancestors

Toot

Written by Andrej Bauer on 2024-12-31 at 17:05

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 | More toots from andrejbauer@mathstodon.xyz

Descendants

Written by ToucanIan on 2024-12-31 at 17:21

@andrejbauer typo in the set builder; should be x, y \in u?

=> View attached media

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

Written by Andrej Bauer on 2025-01-01 at 16:47

@ToucanIan Thanks.

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

Written by Yannick Forster on 2024-12-31 at 17:41

@andrejbauer Mario Carneiro's ITP 19 paper should have both smn and utm and is in mathlib

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

Written by Andrej Bauer on 2025-01-01 at 16:47

@yforster Yeah, I just found it, and it's in the mathlib. https://arxiv.org/abs/1810.08380

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

Written by Martin Escardo on 2024-12-31 at 19:04

@andrejbauer In formalization with computers, it is typically harder to define examples than to define the abstract objects and their theory.

An example is perfectoid spaces in Lean, with a long formalization of the notion, but really no example of interest formalized.

Similarly, with domain theory in TypeTopology, the general theory is easier than defining particular examples and doing something with them, although in this case @de_Jong_Tom did define relevant examples and applied the theory to them.

In any case, the same is true on paper generally. The reason examples feel easier on paper is that, currently, people tend to be rather rigorous regarding the theory, but at the same time rather hand wavy regarding the examples. I am not saying this is a problem or that it is not.

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

Written by ToucanIan on 2024-12-31 at 20:38

@MartinEscardo @andrejbauer @de_Jong_Tom I have found it to be a problem when I try to follow examples! But I do understand why things are that way.

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