The Coq mailing list

[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
> >
> >
> >
> >
> >
> 
> 
>