What is a deterministic timeout

Stream: new members

[Lars Ericson]

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]

(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]

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

[Lars Ericson]

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]

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]

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]

it's finite

[Lars Ericson]

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]

probably working out the expression, I imagine

[Reid Barton]

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

[Alex J. Best]

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

[Lars Ericson]

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]

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

[Reid Barton]

well for example #reduce (2^2^10) will already result in a term of size 2^2^10

[Lars Ericson]

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

[Lars Ericson]

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

[Kevin Buzzard]

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]

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

[Lars Ericson]

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

[Lars Ericson]

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]

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

[Lars Ericson]

Yes, please suggest an example. I looked for other fully instantiated measure_space examples in mathlib but didn't see one.

[Reid Barton]

maybe nat.mul or something

[Reid Barton]

or heck, real.mul

[Lars Ericson]

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]

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]

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]

The phenomenon that terms get really big when you #reduce them is not specific to measure spaces.

[Lars Ericson]

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]

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

[Lars Ericson]

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]

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]

why are you trying to break Lean

[Bryan Gin-ge Chen]

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]

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

[Lars Ericson]

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]

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]

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]

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]

Would it be sensible to have a #reduce' that only reduces types and not proofs?

[Mario Carneiro]

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]

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]

There's no real purpose in reducing proofs in the first place though, or using #reduce at all really.

[Mario Carneiro]

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.