[isabelle-dev] case syntax
krauss at in.tum.de
Sun Jan 15 23:50:27 CET 2012
On 01/12/2012 03:43 PM, Stefan Berghofer wrote:
> Quoting Makarius <makarius at sketis.net>:
>> Just to illuminate the general situation a bit, can you point to
>> relevant parts of your thesis, also the one of Konrad Slind for the
>> old version? Stefan had mentioned that at some point "as everybody
>> knows, Konrad used to do it like that" without giving a reference.
> you can find Konrad's thesis on the web at
> The pattern matching algorithm is described in Section 3.3 (p. 62 - 71)
> The steps of the algorithm are summarized in Figure 3.4.
Here is the younger history:
Konrad's algorithm sometimes leads to a blowup in the number of cases,
which was always seen as problematic. In 2006, I thought I had found an
algorithm that actually produces the minimal number of cases, but I
didn't try to prove it. It was completely wrong of course, as I
discovered later. The current "pattern_split.ML" is based on these ideas.
In 2007/8, I worked out how to actually optimize the number of cases,
but the results are not practical: You get a relatively complex
optimization problem (worse than NP-hard), and it is hard to predict the
results, which makes it unsuitable for use in a package. Furthermore, it
does not actually solve the underlying problem: even when minimizing,
the number of cases is large (it can be exponential). But the theory is
nice and interesting (ch. 4 of my thesis has all the details).
So, in short, it seems that Konrad's algorithm is basically the most
appropriate we can get. When Stefan adapted it to the syntax
translations, he also thought about adding some heuristics that improve
it (by trying to guess the right variable to split on, instead of just
picking the first), but I don't think that any such modifications went in.
More information about the isabelle-dev