Zulip Chat Archive

Stream: new members

Topic: What is a deterministic timeout


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 09 2020 at 13:30):

it's finite

view this post on Zulip 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.

view this post on Zulip Reid Barton (Dec 09 2020 at 13:32):

probably working out the expression, I imagine

view this post on Zulip Reid Barton (Dec 09 2020 at 13:32):

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

view this post on Zulip Alex J. Best (Dec 09 2020 at 13:33):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Lars Ericson (Dec 09 2020 at 13:41):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Dec 09 2020 at 13:46):

maybe nat.mul or something

view this post on Zulip Reid Barton (Dec 09 2020 at 13:46):

or heck, real.mul

view this post on Zulip 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 (α × β) :=

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 09 2020 at 14:38):

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

view this post on Zulip 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)))

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 09 2020 at 23:41):

why are you trying to break Lean

view this post on Zulip 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

view this post on Zulip 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!")

view this post on Zulip 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

If there is an option for #reduce that causes it to print each rewrite then I could drill down on it more.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 10 2020 at 08:27):

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

view this post on Zulip 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 _

view this post on Zulip 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:

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.

view this post on Zulip 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.

view this post on Zulip 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: May 13 2021 at 18:26 UTC