skaller at users.sourceforge.net
Fri Mar 30 21:38:40 EDT 2007
On Fri, 2007-03-30 at 13:04 -0700, Tim Chevalier wrote:
> On 3/30/07, skaller <skaller at users.sourceforge.net> wrote:
> > I'm curious when and how GHC applies rewrite rules,
> > and how expensive it is.
> Have you seen the "Playing By Rules" paper?
> If you still have questions after reading it, you can always ask here.
Thanks for that reference!
FYI, the authors comment that the possibility exists for
feeding reduction rules into a theorem prover but it has
not been explored.
This IS indeed being done right now by Felix. Felix
supports axioms, lemmas, and reduction rules. Lemmas
are theorems which are simple enough to be proven with
an automatic theorem prover.
A couple of days ago my first test case lemma was
proven by Ergo and Simplify. (roughly I proved
that given x + y = y + x and x + 0 = x, that
0 + x = x .. not exactly rocket science :)
Felix emits all the
axioms and lemmas in Why notation, which allows
a large class of theorem provers to have a go at
proving them, since Why translates them.
Reductions aren't handled yet because doing this raised
a simple syntactic problem: I have no way to distinguish
whether a reduction is an axiom or a lemma.
I would note also that default definitions of typeclass
functions are also axioms.
What would be REALLY cool is to prove that typeclass
instances conform to the specified semantics. That,
however, is much harder, especially in Felix (which
is an imperative language ;(
IMHO: connecting a programming language to a theorem prover
is probably mandatory for optimisation. Obvious goals
other than reduction rules are elimination of pre-condition
checks for partial functions. However doing this is hard
because theorem provers can be slow, so generally have
to be run offline. Thus some way of caching the results
for a subsequent recompilation is required.
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
More information about the Glasgow-haskell-users