Here follows some very preliminary view of how the *rules* could be
introduced to Haskell.
I am not so sure about its scientific quality.
The subject needs studying.
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
Equational simplifier proposal for Haskell language
***************************************************
To introduce the constructs
{equations ..}, {defined ..}, {simpStrategy ..}, {termOrdering..}
and the pragma {-# eqScope ..#-}
to be applied as in the following example.
----------------------------------------------------------------------
Example.
{equations
{ map f .map g === map (f.g) }
{x,y,z :: RingWithUnity a => a, (defined x,y,z) ==>
"df" (defined zero, unity, neg x, x*y),
"assoc+" x+(y+z) === (x+y)+z
...
"distr" x*(y+z) === x*y + x*z
}
}
h :: Integer
h = 1 - 1
{-# eqScope
{simpStrategy
{by termOrdering (<')
x =<' y ==> neg x =<' neg y && x+z =<' x+z && x*z =<' y*z
&& x+z <' x*z && x+z <' z*x
... and such
}
}
-- below 0,1,(-) <---> zero, unity, neg
f,f' :: Integer -> Integer
f x = if x==0 then x - x + (x*5 - x*2 - x*3 + 1)
else x - x + (x*5 - x*2 - x*3 + 1)
f' x = x - x + (x*5 - x*2 - x*3 + 1)
}
#-}
----------------------------------------------------------------------
Explanations.
`Equations' are optional
------------------------
Skip `equations', and you never notice the language extension.
{equations ..}
are the bi-directed rewrite rules. They define the equational
calculus with the equivalence relation (===) induced by the given
set of equations.
It depends on the user-defined Strategy, which equations the
simplifier applies first, and whether it applies the equation
from left to right, or from right to left.
Example:
changing the term ordering for `+', `-', `*' would cause the
distributivity equation applied differently, say,
(x+y)*(x-y) --> x*x - y*y or the reverse.
{simpStrategy ..}
is a hint for the simplifier, in what directions to simplify the
expressions.
{termOrdering..}
the part of strategy, often it is the whole strategy.
{defined ..},
(defined e1, e2 ...) means that the values of the listed
expressions are defined. For example, let a = neg a in a+a, 1%0
are not defined.
`defined' is the correctness condition for most of the
simplification rules application.
Return to Example program
-------------------------
The compiler does not apply the equational simplification to the
function h because h is out of eqScope.
For f, the compiler proves that the branches `then ..', `else ..'
operate with the *defined* x value - because the previous operator
succeeded to compare x to 0.
As Integer is an instance of RingWithUnity and as the (defined..)
condition of {equations..} is satisfied in the body of `then..',
`else ..' expressions, they simplify to 1, and the optimization is
f --> fO = if x==0 then 1 else 1
`defined'
---------
Now, it tries to simplify f'. It cannot derive (defined x) in f',
therefore the above equations cannot apply to the body of f'.
For example, replacing f' with f'O = const 1 is incorrect:
(let n = -n in f' n) = undefined,
(let n = -n in f'O n) = 1
But adding `if x==0' the compiler could preserve the program
equivalence and still generate the simplification
fO' x = if x==0 then 1 else 1
This shows that the term rewrite simplifications, like say, x-x -> 0,
are widely applicable. Because the compiler can prove such "defined"
very often. Also the programmer-set properties, like the above
"df" (defined zero, unity, neg x, x*y),
would help the compiler to prove "defined" for other values.
Term rewriting
--------------
The simplification here is the term rewriting by the given equalities:
matching against the successful subterm and substitution.
The ordering, or generally, the strategy, define what subterms are
tried first.
In our particular Example, {simpStrategy..}
puts that the substitutions should make the term smaller in the
described partial ordering (<').
(<') sets, in particular, that the less operation signs (+,*,neg)
contains the term, the less the term is.
Also (<') puts that (+) is smaller than (*).
Under this (<'), the simplifier has a strong reason to apply the
"distr" equation from right to left. Say, x*5 - x*2 --> x*(5-2)
Then, applying the "neg" equation and associativity makes it 1.
Choice of strategy
------------------
In many cases, the notion of optimization is given by some simply
defined ordering <'.
But probably, there has to be possible a direct strategy, say,
"go straight to head normal form". This models the usual programming
language.
Logic language
--------------
The simplifier is actually a program in some logic language,
like, maybe, Maude.
The simplification that the functional programming tool has to perform
at the compile-time, it is done by the Logical language at the
run-time.
Notion of simplification computing
----------------------------------
"Find possibly small expression equal to the given one".
"Equal" means - in the relation (===) defined by equalities.
"Small" means - in the sense of the given ordering (strategy?).
The reduction is not necessary confluent. For example,
2*x + 3*x - 5*x --> (5-5)*x
--> 5*x - 5*x
are both the correct results. It depends on the ordering, which is
better.
Though the confluent systems are of particular interest.
And there exists the Knuth-Bendix completion procedure that sometimes
produces the confluent equality system equivalent to the given
non-confluent system.
Methods
-------
Term rewriting technique. Completion procedure. AC-unification ...
Inductive prover.
In principle, the simplifier could handle the optimizations like
map not (map not xs) --> xs
sum [n..(n+100)] :: Integer --> ((2*n+100)*101)/2
Not only algebra
----------------
All the functional programs can be simplified by this method,
not only "algebraic".
Because the "usual" programs still satisfy some algebraic laws, and
the compiler can exploit these laws.
Type system
-----------
The term rewriting technique i am familiar with, ignores the types.
I hope, the types would not change the theory essentially.
(?)
Say, when the substitution is searched to unify the subexpressions
e1, e2, the unifier may exist only if e1, e2 are of the same type
...
Sources
-------
This proposal is inspired by
[Bu,Lo] Buchberger B., Loos R. Algebraic Simplification.
In "Computer Algebra. Symbolic and Algebraic Computation",
edited by B.Buchberger et al., Springer Verlag, 1982,1983
[Hs] Jieh Hsiang.
Refutational theorem proving using term rewriting systems.
Artificial Intelligence, 1985, vol.25, pp.255-300.
Maude project. http://maude.csl.sri.com Jose Meseguer's group.
I only had once attended to the message in which Maude was mentioned.
Studying the materials from http://maude.csl.sri.com,
its philosophy, will lead to more definite notion of simplification
than written here above.
And maybe, to different notion.
I am not so sure that my recent idea on Maude is correct.
