Kleene normal form theorem

Stream: general

[Mario Carneiro]

Yay, milestone achieved. The statement that I actually proved shows that eval : code -> N ->. N which evaluates a partial recursive function given by a code, is itself a partial recursive function. This is also known as a universal Turing machine in the language of Turing machines.

[Patrick Massot]

Congratulations!

[Patrick Massot]

Do you plan to return to maths now?

[Mario Carneiro]

Lol this is math

[Mario Carneiro]

I'm aiming for proper computability theory at the moment, with r.e. sets and such

[Patrick Massot]

What is "r.e. sets"?

[Mario Carneiro]

recursively enumerable

[Mario Carneiro]

the set of turing machines that halt is a r.e. set

[Mario Carneiro]

but its complement isn't

[Sebastian Ullrich]

IOW the set of machines that reset is a r.e.set

[Patrick Massot]

Thanks

[Sebastian Ullrich]

This looks like a really nice development. Though I have to wonder what we did wrong when building leanpkg to encourage putting everything in a single monolithic package :smile: .

[Mario Carneiro]

I want to finish the MDRP theorem I started last year

[Patrick Massot]

Sebastian: do you refer to mathlib here?

[Sebastian Ullrich]

@Patrick Massot Yes. Not that it's a real issue until we start prebuilding dependencies on leanpkg configure.

[Patrick Massot]

It seems it makes it easier for Mario and Johannes to guarantee a consistent mathlib

[Patrick Massot]

But I think we really need precompiled mathlib nightlies