ordinal.out'

Stream: general

[Violeta Hernández]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Not of T itself

[Junyan Xu]

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]

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]

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

[Kyle Miller]

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]

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

[Eric Wieser]

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

[Kyle Miller]

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

[Kyle Miller]

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

[Kyle Miller]

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]

My suspicion is that the latter is the problem

[Violeta Hernández]

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

[Reid Barton]

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]

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]

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

[Violeta Hernández]

How so?

[Violeta Hernández]

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

[Violeta Hernández]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Violeta Hernández]

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]

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

[Reid Barton]

pgame really holds no data.

[Reid Barton]

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

[Violeta Hernández]

I see

[Violeta Hernández]

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

[Reid Barton]

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

[Victor Maia]

(deleted)

[Violeta Hernández]

I'm convinced now

[Violeta Hernández]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Kyle Miller]

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.