## Stream: general

### Topic: Kleene normal form theorem

#### Mario Carneiro (May 21 2018 at 15:48):

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.

Congratulations!

Lol this is math

#### Mario Carneiro (May 21 2018 at 16:05):

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

#### Patrick Massot (May 21 2018 at 16:06):

What is "r.e. sets"?

#### Mario Carneiro (May 21 2018 at 16:06):

recursively enumerable

#### Mario Carneiro (May 21 2018 at 16:06):

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

#### Mario Carneiro (May 21 2018 at 16:07):

but its complement isn't

#### Sebastian Ullrich (May 21 2018 at 16:08):

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

Thanks

#### Sebastian Ullrich (May 21 2018 at 16:10):

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 (May 21 2018 at 16:10):

I want to finish the MDRP theorem I started last year

#### Patrick Massot (May 21 2018 at 16:35):

Sebastian: do you refer to mathlib here?

#### Sebastian Ullrich (May 21 2018 at 19:36):

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

#### Patrick Massot (May 21 2018 at 19:37):

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

#### Patrick Massot (May 21 2018 at 19:37):

But I think we really need precompiled mathlib nightlies

Last updated: May 08 2021 at 19:11 UTC