# Zulip Chat Archive

## Stream: new members

### Topic: What is a deterministic timeout

#### Lars Ericson (Dec 09 2020 at 06:09):

The following

```
import measure_theory.lebesgue_measure
#reduce measure_theory.real.measure_space
```

causes Lean to print the error message

```
(deterministic) timeout
```

Why is that?

#### Bryan Gin-ge Chen (Dec 09 2020 at 06:18):

`(deterministic) timeout`

means that Lean was trying to do a computation which exceeded the time limit allowed by the `--timeout`

/ `-T`

option. If you run `lean --help`

you'll see that it says:

```
--timeout=num -T maximum number of memory allocations per task
this is a deterministic way of interrupting long running tasks
```

In this case, you are trying to reduce an enormous term in the Lean kernel which is going to take a lot of time and memory.

#### Bryan Gin-ge Chen (Dec 09 2020 at 06:21):

I'm not sure the result of this (some extremely long, unreadable expression) would be very enlightening.

#### Lars Ericson (Dec 09 2020 at 13:22):

Thank you. I am trying to understand whether it is a finitely long expression that it is trying to print or recursively defined and infinitely long. I will up the memory parameter to 64GB and see if it prints.

#### Lars Ericson (Dec 09 2020 at 13:24):

How do I up the memory parameter in general for VS Code? I am just running `code`

and I don't know how that connects to `lean`

.

#### Lars Ericson (Dec 09 2020 at 13:30):

I've made a file `foo.lean`

with the above contents and run `lean foo.lean`

. It's not using any memory at all, it's just sitting there keeping one core hot at 100%. Screenshot-from-2020-12-09-08-28-48.png

#### Reid Barton (Dec 09 2020 at 13:30):

it's finite

#### Lars Ericson (Dec 09 2020 at 13:31):

Thank you, what is it busy doing? You can see from the picture it is using constant memory and all of one CPU.

#### Reid Barton (Dec 09 2020 at 13:32):

probably working out the expression, I imagine

#### Reid Barton (Dec 09 2020 at 13:32):

I don't think this is a productive line of inquiry

#### Alex J. Best (Dec 09 2020 at 13:33):

What are you hoping for reduce to tell you about this definition?

#### Lars Ericson (Dec 09 2020 at 13:37):

I am trying to work out the 3 questions in this thread. This was question 3, which is the easiest to state in 2 lines. It's still working out that expression as I type, on a core i9 CPU. The stack of definitions is not that long, so I guess there is some way to make a combinatorial explosion in term expansion. Which is not what I am trying to understand, but it would be interesting to demonstrate, in a few lines without imports, how to produce a type expression of say `k`

terms which Lean will expand into `2^2^k`

terms, if that's what's going on here, which I also kind of doubt because I'm still not using any memory. So it may not be particularly productive but in some ways, still interesting on its own.

#### Lars Ericson (Dec 09 2020 at 13:39):

Unless this is a case where unification is intractable, which may also be an unproductive thing to think about, but still.

#### Reid Barton (Dec 09 2020 at 13:40):

well for example `#reduce (2^2^10)`

will already result in a term of size 2^2^10

#### Lars Ericson (Dec 09 2020 at 13:40):

Good example, case closed....if the definition of the real numbers contains something like that. Where is it?

#### Lars Ericson (Dec 09 2020 at 13:41):

And also, it's using **no additional memory**, so...probably not.

#### Kevin Buzzard (Dec 09 2020 at 13:41):

Type `#print notation ℝ`

to discover that `ℝ`

is notation for `real`

, and then `#check real`

and right click to go to the definition of `real`

.

#### Kevin Buzzard (Dec 09 2020 at 13:42):

Then you can right click more at your leisure to explore the term without ever explicitly unfolding it.

#### Lars Ericson (Dec 09 2020 at 13:43):

Thank you Kevin, that is helpful. I am trying to climb into definitions, so that is all I really need to know.

#### Lars Ericson (Dec 09 2020 at 13:44):

But...in this case I am trying to climb into `measure_theory.real.measure_space`

as a constructed object. I can read the code but I don't have Lean in my head so it's not a perfect replacement for `#reduce`

.

#### Reid Barton (Dec 09 2020 at 13:45):

If you're interested in such questions, why not start with something a **lot** smaller than `measure_theory.real.measure_space`

#### Lars Ericson (Dec 09 2020 at 13:45):

Yes, please suggest an example. I looked for other fully instantiated `measure_space`

examples in `mathlib`

but didn't see one.

#### Reid Barton (Dec 09 2020 at 13:46):

maybe `nat.mul`

or something

#### Reid Barton (Dec 09 2020 at 13:46):

or heck, `real.mul`

#### Lars Ericson (Dec 09 2020 at 13:50):

I only see one fully instantiated `measure_space`

in `mathlib`

, and one measure-space-producing function instance:

```
$ grep measure_space */*.lean */*/*.lean | grep instance
measure_theory/lebesgue_measure.lean:instance real.measure_space : measure_space ℝ :=
measure_theory/prod.lean:instance prod.measure_space {α β} [measure_space α] [measure_space β] : measure_space (α × β) :=
```

#### Alex J. Best (Dec 09 2020 at 13:54):

Well a measure space is a measurable space + a choice of measure and there are other examples of measures in mathlib (e.g. the Haar measure), so these can be used to define other measure spaces

#### Alex J. Best (Dec 09 2020 at 13:56):

They just might not be an instance as some choice is involved (picking a compact open) so there isn't going to be a unique such choice for any topological group

#### Reid Barton (Dec 09 2020 at 13:58):

The phenomenon that terms get really big when you `#reduce`

them is not specific to measure spaces.

#### Lars Ericson (Dec 09 2020 at 14:13):

Is there a way to trace the rewriting steps of a `#reduce`

? I recall there is a way to trace proofs, not sure about `#reduce`

.

Also in the end, in terms of picking things apart, the major question I have at the moment in terms of how the language works is why I can't extract the value of `m_Union`

in a fully constructed measure.

#### Eric Wieser (Dec 09 2020 at 14:38):

What do you mean by "can't extract the value"?

#### Lars Ericson (Dec 09 2020 at 14:47):

In the last line of this code:

```
import measure_theory.measurable_space
def X : Type := fin 3
def A1 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
def M1 : measurable_space X := {
is_measurable' := A1,
is_measurable_empty := by {rw A1, finish},
is_measurable_compl := assume a h, by {rw A1 at *, finish},
is_measurable_Union := assume f hf, by {rw A1 at *, simp },
}
#check M1
instance XFT : fintype X := fin.fintype _
noncomputable instance amy (s : set X) : fintype s := by classical; apply_instance
noncomputable def μ_M1 : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable _ M1
(λ s _, finset.card s.to_finset)
(by simp)
(λ x h a, begin simp, sorry end)
#check μ_M1 -- μ_M1 : measure_theory.measure X
#check μ_M1.m_Union -- ERROR
```

where it says ERROR in the comment, I get

```
invalid field notation, type is not of the form (C ...) where C is a constant
μ_M1
has type
⁇
```

where `m_Union`

is defined as:

```
(m_Union ⦃f : ℕ → set α⦄ :
(∀i, is_measurable (f i)) → pairwise (disjoint on f) →
measure_of (⋃i, f i) = (∑'i, measure_of (f i)))
```

#### Lars Ericson (Dec 09 2020 at 23:36):

It's not necessary to go to the reals to get `#reduce`

to time out, reducing the type of finite sets with 1 element will also work:

```
import data.fintype.basic
#reduce fin.fintype 1
```

#### Kenny Lau (Dec 09 2020 at 23:41):

why are you trying to break Lean

#### Bryan Gin-ge Chen (Dec 09 2020 at 23:57):

Sure, here's an easier example. These numbers might be specific to my computer / Lean settings but you get the point:

```
#reduce 25781 -- slow, but returns 25781
#reduce 25782 -- deep recursion detected
```

#### Bryan Gin-ge Chen (Dec 09 2020 at 23:59):

We try not to make the Lean kernel reduce big terms. (This is why Kenny is always saying "never unfold definitions!")

#### Lars Ericson (Dec 10 2020 at 00:13):

The set `{0}`

is not as big as the von Neumann ordinal representation of 25782. Something in `#reduce fin.fintype 1`

is intractable, but not because of arithmetic with large von Neumann ordinals. Insight would be gained by finding exactly what in the relatively small (compared to ℝ) set of rules governing `fintype`

is triggering an intractable computation. The question is then whether it is

- Some phrasing in the rules which could be changed to make this example run faster, or
- Lean is triggering an unavoidable instance of an intractable unification problem.

There are lots of intractable unification situations, for example

- https://academic.oup.com/logcom/article/10/1/105/1078476
- https://link.springer.com/chapter/10.1007/3-540-62950-5_78
- https://www.sciencedirect.com/science/article/pii/S0747717103001445
- https://dl.acm.org/doi/abs/10.5555/647196.720997

If there is an option for `#reduce`

that causes it to print each rewrite then I could drill down on it more.

#### Lars Ericson (Dec 10 2020 at 00:17):

And to be clear, this is an intractable **time** problem, not an intractable **space** problem, because my memory usage is constant during the run.

#### Lars Ericson (Dec 10 2020 at 00:42):

But anyway, I don't really care about the intractability of unification, do you? The real reason I was obsessing over this was because I was having a very very hard time figuring out how to rewrite `(λ s _, finset.card s.to_finset)`

as a standalone function. It took me several days of spare time to come up with this (note, `def`

doesn't work):

```
noncomputable abbreviation qlbrdl (s: set (fin 1)) (z: @is_measurable (fin 1) M s) : ennreal :=
finset.card s.to_finset
```

It's done, though, so I can move on.

#### Mario Carneiro (Dec 10 2020 at 08:22):

The problem with reducing `fin.fintype 1`

is that using `#reduce`

means it also has to reduce the *proofs*, which is not something you normally have to worry about in unification problems / proof by `rfl`

. `fintype`

contains several proofs, proved using some recursions that were not size optimized, so it's not particularly surprising to me that this fails. Really, `#reduce`

is useless on almost everything beyond the basics

#### Eric Wieser (Dec 10 2020 at 08:27):

Would it be sensible to have a `#reduce'`

that only reduces types and not proofs?

#### Mario Carneiro (Dec 10 2020 at 09:03):

You can use `whnf`

to incrementally drill down into a term, unfolding only what you need to.

```
import data.fintype.basic
set_option pp.proofs true
-- #reduce (fin.fintype 1) -- timeout
run_cmd tactic.whnf `(fin.fintype 1) >>= tactic.trace
-- {elems := finset.fin_range 1, complete := finset.mem_fin_range 1}
-- #reduce finset.fin_range 1 -- timeout
run_cmd tactic.whnf `(finset.fin_range 1) >>= tactic.trace
-- {val := ↑(list.fin_range 1), nodup := list.nodup_fin_range 1}
#reduce (↑(list.fin_range 1) : multiset (fin 1))
-- quot.mk list.perm [⟨0, _⟩]
set_option pp.proofs true
#reduce (↑(list.fin_range 1) : multiset (fin 1))
-- quot.mk list.perm [⟨0, <1310 lines of proof>⟩]
set_option pp.proofs false
run_cmd tactic.whnf `(↑(list.fin_range 1) : multiset (fin 1)) >>= tactic.trace
-- quot.mk setoid.r (list.fin_range 1)
#reduce list.fin_range 1
-- [⟨0, _⟩]
run_cmd tactic.whnf `(list.fin_range 1) >>= tactic.trace
-- fin.mk 0 _ :: list.pmap fin.mk list.nil _
```

#### Lars Ericson (Dec 10 2020 at 13:19):

Thank you, having a technique for stepping through term-mode proofs is extremely useful.

So the root cause in this case is an unoptimized recursion in the proof.

This introduces a new field of study: **The computational complexity of Lean proofs about P m. ** If there are

`m`

variables in a statement about `P m1 ... mN`

, it would be reasonable to write papers of the form "We can prove `P m1 .. mN`

in Lean in O(N^2) time thus improving on the prior proof in O(2^N)" or in a sad case of form "Any proof of `P m1..mN`

in Lean requires O(2^2^n) time".You can see something along these lines in a different paradigm (decidable sublanguages of set theory) here:

- Decision procedures for elementary sublanguages of set theory. I. Multi‐level syllogistic and some extensions
- Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
- ...
- Decision procedures for elementary sublanguages of set theory XV. Multilevel syllogistic extended by the predicate finite and the operators singleton and pred

The only downside is that a lot of these results are of form "this is hyperexponential in `N`

" . This creates a market for quantum computing. It can also lead to some discouragement in the absence of a quantum computer.

#### Reid Barton (Dec 10 2020 at 13:25):

There's no real purpose in reducing proofs in the first place though, or using `#reduce`

at all really.

#### Mario Carneiro (Dec 10 2020 at 13:47):

The size of a fully expanded proof is basically the same thing as proving a theorem only using the axioms. There is a close connection to cut-free proofs, and the computational bounds on those are usually in the range `2^^n`

where `^^`

is the iterated exponential (power tower), so quite bad. However, we need not dismay, because all this means is that *lemmas are important*. We can still prove and efficiently typecheck a proof without ever inlining all the lemmas, which is what `#reduce`

amounts to.

Last updated: Dec 20 2023 at 11:08 UTC