The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

> what does take so many nodes?
> 256×256=65.536 which is 15 times smaller than 1million+,
> so you have more than 15 nodes for a branch!

That's not really surprising. The definition of the function itself is
66k, which corresponds to roughly one node per leaf of the matching
tree (true or false) + extra nodes for each nested match. But the
proof contains a small proof term at each leaf, and each branch
abstracts on the hypothesis [char_eqb c c' = true] when destructing on
[c] or [c'], so 15 nodes per path seem OK. Note that the proof as a
whole contains 65250 discrimination proofs (which I cut in a lemma,
otherwise the proof is even larger -- 1.8M).
Anyway, the time it takes to typechecks confirms it's way bigger than 66k.

S.

>> 2011/3/3 AUGER Cedric 
>>Â <Cedric.Auger AT lri.fr>:
>> > Le Thu, 3 Mar 2011 09:39:02 +0100,
>> > Stéphane Lescuyer 
>>Â >Â <stephane.lescuyer AT inria.fr>
>> >  a écrit :
>> >
>> > And as the first function to define would be equality, ie.
>> >
>> > match x, y with
>> > | TAB, TAB => true
>> > | CR, CR => true
>> > …
>> > | _, _ => false
>> > end.
>> >
>> > By diagonalizing, you'll need to have a 256×256 system.
>> >
>> >> Indeed, you are right, so in a way the situation isn't too bad.
>> >> Another matching pattern which looks simple but would be quadratic
>> >> is the following:
>> >>
>> >> match c1, c2 with
>> >> | TAB, _ => true
>> >> | _, CR => true
>> >> | _, _ => false
>> >> end
>> >>
>> >> I guess that's up to people to avoid stuff like that, except for
>> >> some basic necessary functions (equality test and maybe
>> >> comparison).
>> >>
>> >> Even with 'only' 512 cases or so, what bothers me is that because
>> >> underscore patterns are only syntactic, the right-hand side
>> >> expression will end up being duplicated and typechecked 500+ times
>> >> in the term.
>> >>
>> >> S.
>> >>
>> >> On Wed, Mar 2, 2011 at 11:55 PM, Brandon Moore
>>Â >>Â <brandon_m_moore AT yahoo.com>
>> >>  wrote:
>> >> >
>> >> >
>> >> >> From: Stéphane Lescuyer 
>>Â >>Â >>Â <stephane.lescuyer AT inria.fr>
>> >> >
>> >> >>
>> >> >> ...
>> >> >>
>> >> >> The other thing I would be worried about is '_' patterns,  where
>> >> >> writing something like:
>> >> >>
>> >> >> match c1, c2 with
>> >> >> | TAB, CR =>  true
>> >> >> | _, _ => false
>> >> >> end
>> >> >>
>> >> >> would look harmless while actually  expanding to a 256*256
>> >> >> matching tree.
>> >> >
>> >> > A minor point, but I think that expands to a 256+256 matching
>> >> > tree. I would expect all but the TAB branch of the outer match
>> >> > to not decompose the second argument. It seems that's how it
>> >> > actually works, at least with a smaller example. Perhaps
>> >> > something with dependent types might see the pathological case.
>> >> >
>> >> > Example:
>> >> >
>> >> > Inductive foo : Set := A | B | C | D | E .
>> >> >
>> >> > Definition bar : foo -> foo -> bool := fun x y =>
>> >> >  match x, y with
>> >> >  | A, B => true
>> >> >  | _, _ => false
>> >> >  end.
>> >> >
>> >> > Print bar.
>> >> >
>> >> > produces
>> >> >
>> >> > bar =
>> >> > fun x y : foo =>
>> >> > match x with
>> >> > | A =>
>> >> >    match y with
>> >> >    | A => false
>> >> >    | B => true
>> >> >    | C => false
>> >> >    | D => false
>> >> >    | E => false
>> >> >    end
>> >> > | B => false
>> >> > | C => false
>> >> > | D => false
>> >> > | E => false
>> >> > end
>> >> >     : foo -> foo -> bool
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >>
>> >>
>> >>
>> >
>> >
>>
>>
>>
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06