Languages that optimise using logic programming

Question

Are there any languages that perform compile-time optimisation using arbitrary logic programming?

I'm looking for an example of a language that will enable you to do something like:

• Define an arbitrary predicate, e.g. is-idempotent?
• Tell the compiler that f(f(x)) is equal to f(x) if the is-idempotent? function is true for f
• Specify is-idempotent? for various functions (possibly indirectly, e.g. implied by other logic statements)
• Have the compiler perform optimisations based on the predicates / optimisations that it is aware of

Answer 1

I think what you want is a program transformation system.

These can let you define rules to apply to source code, e.g., algrebraic laws to optimize code.

What you will discover is that there is a variety of problems. The first is handling scoping rules and side effects in langauges. The second is sequencing of the transformations; the order in which they are applied often produces radically different results.