timeout why?

Stream: general

[Thorsten Altenkirch]

timeout.lean
I get a timeout for this toy compiler on a small expression? Why?

[Gabriel Ebner]

Please paste your example in a code block.

[Johan Commelin]

or a github gist... if it's too long

[Thorsten Altenkirch]

inductive Expr : Type
| const : ℕ → Expr
| var : string → Expr
| plus : Expr → Expr → Expr
| times : Expr → Expr → Expr

open Expr

inductive Instr : Type
| pushC : ℕ → Instr
| pushV : string → Instr
| add : Instr
| mult : Instr

open Instr

def Code : Type
  := list Instr

def Stack : Type
  := list ℕ

def comp_aux : Expr → Code → Code
| (const n) c := pushC n :: c
| (var x) c := pushV x :: c
| (plus l r) c := comp_aux l (comp_aux r (add :: c))
| (times l r) c := comp_aux l (comp_aux r (mult :: c))

def comp (e :Expr) : Code
  := comp_aux e []

def e1 : Expr
  := times (var "x") (plus (var "y") (const 2))

#reduce (comp e1)

[Kenny Lau]

maybe it's the string bug

[Kenny Lau]

I remember there was a bug with evaluating strings because of some "undefined" string

[Gabriel Ebner]

You should use #eval instead of #reduce.

[Rob Lewis]

It is related to strings, but it's not a bug. This comes up pretty often. https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/deep.20recursion.20error.20reducing.20strings

[Rob Lewis]

We need to work on SEO for the Zulip archive. It's too bad that googling "lean prover string reduce" doesn't turn up one of the relevant threads.

[Thorsten Altenkirch]

Gabriel Ebner said:

You should use #eval instead of #reduce.

I see but then I have a different problem:

35:1: result type does not have an instance of type class 'has_repr', dumping internal representation

[Johan Commelin]

So I guess you need to provide an

instance : has_repr Code :=
...

[Johan Commelin]

Are there derive handlers for has_repr? If so you can put @[derive has_repr] before most of your defs.

[Gabriel Ebner]

Unfortunately not. But they would be pretty useful.

[Gabriel Ebner]

https://github.com/gebner/mathlib/blob/e66976e99d5e1b7811e80bb7ca41421a5e31a322/src/tactic/derive_to_string.lean

[Gabriel Ebner]

But the automatically generated instances are not particularly nice. (It's hard to know if you should parenthesize or not. That is, var 5 or var (5).)

[Thorsten Altenkirch]

I am not sure what is going on. Surely lean knows how to evaluate this expression? Or not? And it should also know how to print a list. And Instr which is just a sum???

[Johan Commelin]

It doesn't unfold Code when trying to figure out how to print things, afaik.

[Johan Commelin]

You can write @[derive has_repr] above def Code, but apparently for Instr you will have to write the instance by hand.

[Thorsten Altenkirch]

Johan Commelin said:

It doesn't unfold Code when trying to figure out how to print things, afaik.

It's not this - I tried substitute Code by list Instr.

[Johan Commelin]

I guess it got stuck on Instr at that point

[Thorsten Altenkirch]

Actually I also have a related problem. How do I use ++ on Code (which is defined as list Instr)?

[Thorsten Altenkirch]

Is there a way to just have a type synonym, without indroducing a new type?

[Gabriel Ebner]

You could use @[reducible] def instead.

[Gabriel Ebner]

Or you could use @[deriv has_append, deriv has_repr] def to copy the instances explicitly.

[Gabriel Ebner]

Type-class inference can see through reducible definitions, so you get all instances from list automatically.

[Thorsten Altenkirch]

Gabriel Ebner said:

You could use @[reducible] def instead.

Thank you - this does the trick.

[Thorsten Altenkirch]

I still don't understand why #reduce hangs. Btw all I wanted is a nice example for the code without having to create it by hand... :-(

[Gabriel Ebner]

Please read the link that Rob posted earlier, it explains the issue.

[Thorsten Altenkirch]

Ah I sort of ignored this because I couldn't imagine it had anything to do with strings. I see. Weird.

[Rob Lewis]

Gabriel Ebner said:

But the automatically generated instances are not particularly nice. (It's hard to know if you should parenthesize or not. That is, var 5 or var (5).)

Is the heuristic "does the argument contain a space" good enough?

[Rob Lewis]

It will still use unnecessary parens, but not all the time

[Rob Lewis]

(I think we should add this derive handler, I've missed it before too)

[Gabriel Ebner]

Rob Lewis said:

Gabriel Ebner said:

But the automatically generated instances are not particularly nice. (It's hard to know if you should parenthesize or not. That is, var 5 or var (5).)

Is the heuristic "does the argument contain a space" good enough?

That seems slow. I would rather go for a typeclass/attribute class does_not_require_parens (α : Sort*) : Prop. The proper way is of course to add four classes has_to_{repr,string,format,tactic_format}_parens which return tuples consisting of (left-binding power, string, right-binding power).

[Rob Lewis]

That still seems trickier than I care to waste my time on. What if we just add the dumb version? People can still implement their own has_reprs if they don't like the ugly derived one.

[Gabriel Ebner]

I won't complain about a "bad" version. I think any derive handler is better than none, and we can improve it afterwards.

[Alexandre Rademaker]

Most of the discussion so far seems to blame string, right? I have a similar problem using nat. Following the idea from https://github.com/leanprover/lean/blob/72a965986fa5aeae54062e98efb3140b2c4e79fd/tests/lean/run/soundness.lean, we are defining atomic symbols in our logic with nat. Everything looks fine until we need to implement a function to convert between representations.

[Mario Carneiro]

Do you have a #mwe? nat should be fine for small numbers

[Mario Carneiro]

num may perform better if you have larger numbers and still need kernel computation

[Alexandre Rademaker]

Sorry, yes, I didn't complete my post. The relevant part is https://github.com/arademaker/alc-lean/blob/atomics/src/alc.lean#L21-L39. and https://github.com/arademaker/alc-lean/blob/atomics/src/sequent.lean#L7-L40. Line 40 is the problem... reduce produces a timeout.

[Alexandre Rademaker]

The function sigma' is a recursive function to transform the lconcept (labeled concepts) into regular concepts of the logic. The idea is that labeled concepts are concepts were the quantifier prefix were separated into a list. The reduce is to test if the function definition is right, I can't understand why it doesn't work.

[Alexandre Rademaker]

The reduction of lconcept and concept terms works. The non-standard facts about sigma' is the pattern match over the structure and the way the recursion calls are constructed. the recursive call is done inside the term being produced.

[Mario Carneiro]

The issue is that sigma' is written in a way that is not straightforwardly structural recursive, so lean is falling back on well founded recursion and this performs poorly in the kernel. There is an easy fix:

def sigma'_aux : list Label → Concept → Concept
| [] c := c
| (Forall r :: ls) c := Every r (sigma'_aux ls c)
| (Exists r :: ls) c := Some r (sigma'_aux ls c)

def sigma' : LConcept → Concept
| ⟨roles, c⟩ := sigma'_aux roles c

[Alexandre Rademaker]

Hi @mario, indeed, I ended up with the same approach that I was about to post. Thank you...

[Alexandre Rademaker]

def aux : list Label -> Concept -> Concept
 | [] c := c
 | ((Forall r) :: ls) c := Every r (aux ls c)
 | ((Exists r) :: ls) c := Some r (aux ls c)

def sigma2 (lc : LConcept) : Concept := aux lc.roles lc.concept

#reduce sigma2 (LConcept.mk [Forall R#0, Exists R#1] (Concept.Bot))

Can we see this as a Lean bug? So maybe we can expect better behaviour in Lean 4?

[Mario Carneiro]

What would the bug be exactly? This is an interaction of components that are all working as designed

[Mario Carneiro]

Also, I think the days of hoping that everything will magically be better in lean 4 are over, because the real thing is out. Many things are better, many other things can be made better in user space, and some things aren't any different. Right now I think well founded recursion isn't completely supported yet but I don't think the overall structure of how the equation compiler picks a compilation strategy will change much if at all

[Alexandre Rademaker]

well, the pattern matching was used as expected. The syntax for the definition is right. So why the reduction is not working? You said that it is not straightforwardly structural recursive but it is a recursive definition. Can we provide any hint to Lean? Maybe?!

[Alexandre Rademaker]

I see.

[Mario Carneiro]

Structural recursion means it has to be written in a certain form. You pattern match on an inductive type and call the function on subterms

[Mario Carneiro]

sigma' isn't written like that because (LConcept.mk ls c) is not a subterm of { LConcept . roles := (Forall r :: ls) , concept := c}

[Mario Carneiro]

I'm not saying it can't be better, I'm saying there is a nontrivial design question that has to be resolved to improve the situation

[Mario Carneiro]

well founded recursion is much more flexible, you can call the function on anything with a smaller "size", where size is a natural number defined automatically on inductive types. sizeof (LConcept.mk ls c) < sizeof { LConcept . roles := (Forall r :: ls) , concept := c} which is why the wf recursion compilation strategy succeeds

[Alexandre Rademaker]

I see, thank you for the explanation.

[Mario Carneiro]

However, the issue with well founded recursion is that it requires unfolding proofs in order for the definition to definitionally reduce in the kernel (which is what #reduce does), and lean / mathlib generally make no effort to write proofs that can be computed well (indeed, most proofs use axioms and those block computation entirely)

[Mario Carneiro]

The real answer is "don't use #reduce" though

[Mario Carneiro]

It is slow and mostly useless

[Mario Carneiro]

#eval works fine on the wf definition

[Alexandre Rademaker]

But for using eval I will need to understand how to provide the has_repr instance to may structures and inductive types..

[Mario Carneiro]

@Alexandre Rademaker If the only reason you aren't using #eval is because #reduce gets better printing, here's a life hack for you

meta def print {α} [has_reflect α] (e : α) : tactic unit :=
tactic.pp (reflect e) >>= tactic.trace

#eval print $ sigma' (LConcept.mk [Forall R#0, Exists R#1] (Concept.Bot))
-- Ax R#0:Ex R#1:Bot

That way you just need @[derive has_reflect] on all your inductive types, and you get the same printing as lean will normally do, meaning that notations and things work as normal

[Alexandre Rademaker]

Thank you, I should have missed someting, I spread the @[derive has_reflect] all over the places but now eval does not produce anything

https://github.com/arademaker/alc-lean/blob/atomics/src/sequent.lean

[Alexandre Rademaker]

Oh, no. Sorry. It is working, the Emacs mode is not showing it with the C-c C-b (Toogle message boxes).

[Mario Carneiro]

you might also try using run_cmd instead of #eval; it should look the same but maybe emacs shows it differently