Zulip Chat Archive

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.

Patrick Massot (May 21 2018 at 16:00):

Congratulations!

Patrick Massot (May 21 2018 at 16:01):

Do you plan to return to maths now?

Mario Carneiro (May 21 2018 at 16:04):

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

Patrick Massot (May 21 2018 at 16:09):

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: Dec 20 2023 at 11:08 UTC