Zulip Chat Archive

Stream: general

Topic: make onote.repr computable again


view this post on Zulip Kenny Lau (Apr 20 2018 at 09:33):

/-- The ordinal denoted by a notation -/
@[simp] noncomputable def repr : onote  ordinal.{0}
| 0 := 0
| (oadd e n a) := ω ^ repr e * n + repr a

This is in set_theory/ordinal_notation.lean. This definition is currently noncomputable. Should I start working on it to make it computable? (I believe I know how to make it computable, my only worry is that my PR will be rejected)

view this post on Zulip Kenny Lau (Apr 20 2018 at 09:33):

(cc @Mario Carneiro)

view this post on Zulip Kenny Lau (Apr 20 2018 at 09:36):

(cc @Johannes Hölzl )

view this post on Zulip Kenny Lau (Apr 20 2018 at 09:53):

maybe I'll do some analysis to show that I know how to make it computable

view this post on Zulip Kenny Lau (Apr 20 2018 at 09:55):

ω depends on nat.lt.is_well_order, which depends on has_lt.lt.is_strict_total_order', which depends on lt_trichotomy, which depends on lt_or_eq_of_le, which uses classical.by_cases, so we only need to change one of them

view this post on Zulip Gabriel Ebner (Apr 20 2018 at 09:56):

classical.by_cases is in Prop, so it has zero effect on noncomputability.

view this post on Zulip Kenny Lau (Apr 20 2018 at 10:00):

you're right. I need to redo my analysis.

view this post on Zulip Kenny Lau (Apr 20 2018 at 10:02):

@Gabriel Ebner do you have any idea which part is noncomputable?

view this post on Zulip Gabriel Ebner (Apr 20 2018 at 10:09):

ord.has_pow is noncomputable because it 1) has an if-then-else on a=0, and 2) uses limit_rec_on

view this post on Zulip Gabriel Ebner (Apr 20 2018 at 10:11):

I wonder if there is a cheap trick where you "eta-expand" an arbitrary ordinal to make it computable. All components of ordinals are props or types after all.

view this post on Zulip Mario Carneiro (Apr 20 2018 at 22:44):

Ordinals are a noncomputable theory, so there isn't much point. Furthermore, as Gabriel observes, ordinals are "cheaply noncomputable" since they contain only erasable data, so the VM never computes with them anyway. I think a future version of lean may mark this function computable simply because it doesn't compute anything.

view this post on Zulip Mario Carneiro (Apr 20 2018 at 22:48):

You may wonder why so many things are noncomputable, when the choice usage is only in things like ord; the reason is because there is a lot of use of "unique choice", which is okay in ZF but not in lean. For example, can you even decide a = 0? This is easy in ZF, where everything is decidable by unique choice, but to do in lean you would have to decide if an arbitrary type is empty, for example plift p where p is a nondecidable proposition.

view this post on Zulip Mario Carneiro (Apr 20 2018 at 22:50):

My question to you: why do you care that repr is noncomputable? If the goal is to compute with ordinals, that's the whole reason I wrote the ordinal_notation file - it gives computational analogues of the ordinal functions. You will note that onote.add and such are all computable. repr is only there to make it possible to state correctness results, assuming full choice.


Last updated: May 16 2021 at 21:11 UTC