Zulip Chat Archive

Stream: general

Topic: Kleene normal form theorem


view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 21 2018 at 16:00):

Congratulations!

view this post on Zulip Patrick Massot (May 21 2018 at 16:01):

Do you plan to return to maths now?

view this post on Zulip Mario Carneiro (May 21 2018 at 16:04):

Lol this is math

view this post on Zulip Mario Carneiro (May 21 2018 at 16:05):

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

view this post on Zulip Patrick Massot (May 21 2018 at 16:06):

What is "r.e. sets"?

view this post on Zulip Mario Carneiro (May 21 2018 at 16:06):

recursively enumerable

view this post on Zulip Mario Carneiro (May 21 2018 at 16:06):

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

view this post on Zulip Mario Carneiro (May 21 2018 at 16:07):

but its complement isn't

view this post on Zulip Sebastian Ullrich (May 21 2018 at 16:08):

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

view this post on Zulip Patrick Massot (May 21 2018 at 16:09):

Thanks

view this post on Zulip 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: .

view this post on Zulip Mario Carneiro (May 21 2018 at 16:10):

I want to finish the MDRP theorem I started last year

view this post on Zulip Patrick Massot (May 21 2018 at 16:35):

Sebastian: do you refer to mathlib here?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 21 2018 at 19:37):

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

view this post on Zulip 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