## Stream: general

### Topic: ordinal.out'

#### Violeta Hernández (Jul 14 2022 at 19:13):

I don't remember if I've asked this before, but what's the deal with docs#ordinal.out'? How can it be computable when it depends on quotient.out? Do we really gain any computability out of this?

#### Eric Wieser (Jul 14 2022 at 19:17):

If I remember correctly, terms of type Sort u are always computable

#### Eric Wieser (Jul 14 2022 at 19:18):

Computability is a property of terms t : T where T : Type u

#### Eric Wieser (Jul 14 2022 at 19:18):

Not of T itself

#### Junyan Xu (Jul 14 2022 at 19:21):

Reid Barton said:

I think the rules are simply

1. Types and propositions and proofs are always computable (because they are not actually represented at all at runtime). That is, anything whose type is Sort u for some u. This also extends to Pi-types ending in Sort u.
2. Axioms are not computable (because they have no definition). Normally I think this only applies to choice because the other standard axioms are propositions.
3. Anything that uses something noncomputable is noncomputable, except that rule 1 always takes priority.

#### Kyle Miller (Jul 14 2022 at 19:22):

I don't know anything about the design of ordinal.out', but I think I can explain why it's computable. The fields of docs#Well_order are a Type, a Prop-valued function, and a Prop. Each of these are considered to be computationally irrelevant, so they are erased during VM compilation. So, Well_order is represented by the VM as a nullary constructor with no data whatsoever. The definition of ordinal.out' then reduces to this single nullary constructor during VM compilation, so it's computable in a rather trivial way.

#### Eric Wieser (Jul 14 2022 at 19:25):

I guess the question is whether quotient.out would cause downstream poisoning in places the current out' doesn't

#### Kyle Miller (Jul 14 2022 at 19:25):

The reason quotient.out isn't computable here is that it ends up using the axiom of choice to transform this nullary constructor. It's a no-op in this case, though, so it's noncomputable for a somewhat silly reason.

I wonder whether it would break anything to mark quotient.out to be @[inline]. There's a chance it would make uses of it for ordinals be computable.

#### Eric Wieser (Jul 14 2022 at 19:26):

Is the problem here equivalent to the fact that x : Type matches rule 1 but not x : Type × Type?

#### Eric Wieser (Jul 14 2022 at 19:27):

That is, "is computationally irrelevant" isn't inherited by inspecting fields of structures

#### Kyle Miller (Jul 14 2022 at 19:27):

I think it's just that quotient.out is marked noncomputable, so you can't use it in a computationally relevant way.

#### Kyle Miller (Jul 14 2022 at 19:28):

ordinal.out' is effectively inlining a let that uses quotient.out, pushing it into computationally irrelevant terms.

#### Kyle Miller (Jul 14 2022 at 19:29):

well, also doing the x <-> C x.1 x.2 ... eta conversion for structures and pushing it in even further. (related to what you were saying about x : Type × Type)

#### Eric Wieser (Jul 14 2022 at 19:44):

My suspicion is that the latter is the problem

#### Violeta Hernández (Jul 14 2022 at 22:00):

I've heard about Lean 4 doing eta reduction automatically. Would that turn ordinal.out' noncomputable again?

#### Reid Barton (Jul 14 2022 at 22:34):

A computable pgame is about as useful as a computable real, i.e., not useful. This file would benefit from noncomputable theory.

#### Violeta Hernández (Jul 14 2022 at 22:39):

I do think there's instances where we want computability on games, see the domineering file for instance. But having nim be computable does sound ultimately futile, given the dependence on ordinals.

#### Reid Barton (Jul 14 2022 at 22:42):

It's meaningless though, there is no data in a pgame that you can extract anyways.

How so?

#### Violeta Hernández (Jul 14 2022 at 22:46):

Note that I'm talking about the type of pre-games, not the quotient type of games

#### Violeta Hernández (Jul 14 2022 at 22:47):

You should be able to extract left and right moves out of a pgame

#### Eric Wieser (Jul 14 2022 at 22:48):

But the moves are types, and those have no runtime content

#### Eric Wieser (Jul 14 2022 at 22:49):

If you want to dig into the depths of lean, you could try modifying the noncomputability checker to be aware of this

#### Eric Wieser (Jul 14 2022 at 22:49):

Because the current behavior is certainly misleading, even though as Reid rightly comments it doesn't mean anything

#### Violeta Hernández (Jul 14 2022 at 22:51):

All I know is that the VM can determine whether two small games of domineering are equivalent, and it shouldn't be able to do that if pgame truly held no data

#### Reid Barton (Jul 14 2022 at 22:51):

For example, you can't determine whether the left or right option sets are empty

#### Reid Barton (Jul 14 2022 at 22:51):

pgame really holds no data.

#### Reid Barton (Jul 14 2022 at 22:52):

The data isn't in the pgame, it's in some synthesized decidable instances

I see

#### Violeta Hernández (Jul 14 2022 at 22:53):

So there's really no use in trying to make things computable here

#### Reid Barton (Jul 14 2022 at 22:55):

e.g. for a more familiar example

import data.real.basic

instance x : decidable ((0 : ℝ) < 1) := by { norm_num, apply_instance }

#eval to_bool ((0 : ℝ) < 1)   -- tt


(deleted)

#### Violeta Hernández (Jul 14 2022 at 22:55):

I'm convinced now

#### Violeta Hernández (Jul 14 2022 at 22:55):

#15367 adds noncomputable theory to this file, and removes ordinal.out' in the process

#### Eric Wieser (Jul 14 2022 at 23:49):

Remember the only advantage to noncomputable theory is that it saves a few noncomputable keywords

#### Eric Wieser (Jul 14 2022 at 23:50):

It might be worth leaving in in case we ever fix lean to know automatically that these have no computational content, as they we can see the effect

#### Violeta Hernández (Jul 15 2022 at 00:05):

So, keep the noncomputable keywords but still ditch ordinal.out'?

#### Kyle Miller (Jul 15 2022 at 00:06):

Eric Wieser said:

If you want to dig into the depths of lean, you could try modifying the noncomputability checker to be aware of this

I think this would go beyond the noncomputability checker and would be rather involved. The VM compiler still thinks that there's computational content to the pgame type itself:

inductive pgame : Type (u+1)
| mk : ∀ α β : Type u, (α → pgame) → (β → pgame) → pgame


There are two closures there in its constructor. You'd need to design a pass for the VM compiler that detects this and turns it into a nullary constructor (right now it turns into a 2-argument constructor since the type arguments are irrelevant). This analysis then also needs to go into the noncomputability checker.

Last updated: Aug 03 2023 at 10:10 UTC