Lambda the Ultimate

Thanks Vesa. I wonder if this is a worthwhile book to purchase and read? If anyone has comments on it, or other suggestions for a good textbook on term rewriting, please throw them at me. Thanks!

The book Term Rewriting and All That might be relevant to your question.

I can confirm that this is a good book, and I would recommend it to anyone who wants to think deep thoughts about term-rewriting, lambda calculus and computation.

I don't know if it will help with the originally-posted problem in immediate practical terms, but if anyone wants to think hard about the question, it is probably a good book to absorb as background.

Hi Roly, thanks for the link.

"asking whether equational conditions like associativity, left-idempotence, commutativity, etc., are true about program phrases is undecidable"

Yes, this is fairly obviously true. However decidability is not a deterrent: we can still search for proofs of certain properties of functions within the infinite space created by rewrite rules. Whatever properties we discover proofs of, we get to use.

So to give an example, consider the following rewriting rules:

rule { $a $b f } => { $a $b g }
rule { $a $b g } => { $b $a f }

We can follow these rules and find something useful, we just aren't always guaranteed to find something useful, and to get to the end of the search.

It just like ordinary optimization: finding the fastest program is undecidable, but we can still look for faster programs.

I believe I found the Pettorossi paper, thanks Gavin.

Automatic Derivation of Logic Programs by Transformation (2000) Alberto Pettorossi, Maurizio Proietti

Abstract: We present the program transformation methodology for the automatic development of logic programs based on the rules + strategies approach. We consider both definite programs and normal programs and we present the basic transformation rules and strategies which are described in the literature. To illustrate the power of the program transformation approach we also give some examples of program development. Finally, we show how to use program transformations for proving properties of predicates...

I will look closely at this, it seems to be exactly what I am suggesting.

"providing the compiler with a proof is possible to do in an elegant way in a system with dependent types. You just have a proof term for the commutativity of your function that the compiler can check and use."

This is a good point. Thank you for sharing it.

"it is clear that deciding if a function is commutative is too hard"

I am convinced that it is in fact not too hard to be useful. Why do you say that? I suspect you are referring to the general case, which as I mentioned earlier is not neccessary to try and solve. I am not trying to prove that all functions are commutative or not, just trying to find as many commutative functions as possible.

While I appreciate the links for using lemmas as rewrite rules, I should point out that I am proposing the opposite: using rewriting rules as axioms (or lemmas). I am trying to figure out whether such research has some novelty.

Of course I do not dispute the fact that inference of properties is useful, I'm quite happy when people design programs to do work humans would have to do otherwise (isn't that the whole point?). People have already provided links on distillation and rewriting-based techniques for proving equations. There is also the rippling technique which might be of interest: a kind of mix between heuristics and rewriting for automated deduction.

This ripppling technique is very interesting, I was not aware of it, thank you very much Matthieu.

This is a good reference for rippling. Although it's a bit old now, and doesn't cover some recent developments (dynamic rippling, relational rippling etc.)

There's also, in addition to the rippling book, a chapter in the Handbook of Automated Reasoning (Chapter 7, pgs 876 onwards) that covers some material on rippling.

Thank you very much for the links Bryan!