Hi,<br><br>you can browse my code <a href="http://trac.informatik.uni-bremen.de:8080/hets/browser/trunk/Search/Common">here.</a> It has become part of&nbsp;<a href="http://www.dfki.de/sks/hets">Hets</a> the Heterogeneous Tool Set which is a parsing, static analysis and proof management tool combining various tools for different specification languages.<br>
However, let me warn you: the code isn&#39;t yet well documented at parts also ad hoc. Don&#39;t know whether it can help to solve your tasks.<br>The goal of my normalization code is to bring formulae via equivalence transformations and alpha-renaming into a standard or normal form such that for instance the following three formulae become syntactically identical (i.e. not just modulo alpha equivalence or modulo associativity and commutativity):<br>
<br>\begin{enumeratenumeric}<br>&nbsp; \item $\forall \varepsilon . \varepsilon &gt; 0 \Rightarrow \exists \delta .<br>&nbsp; \forall x. \forall y. 0 &lt; |x - y| \wedge |x - y| &lt; \delta \Rightarrow | f<br>&nbsp; (x) - f (y) | &lt; \varepsilon$<br>
&nbsp; <br>&nbsp; \item $\forall \varepsilon . \exists \delta . \forall x, y. \varepsilon &gt; 0<br>&nbsp; \Rightarrow (0 &lt; |x - y| \wedge |x - y| &lt; \delta \Rightarrow | f (x) - f (y)&nbsp; | &lt; \varepsilon)$<br>&nbsp; <br>&nbsp; \item $\forall e . \exists d . \forall a,b. e &gt; 0<br>
&nbsp; \wedge |a - b| &lt; d \wedge 0 &lt; |a - b| \Rightarrow | f (a) - f (b) | &lt; e$<br>\end{enumeratenumeric}<br><br>Cheers,<br><br>Immanuel<br><br><br><br><div class="gmail_quote">2008/12/4 Ganesh Sittampalam <span dir="ltr">&lt;<a href="mailto:ganesh@earth.li">ganesh@earth.li</a>&gt;</span><br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Hi,<br>
<br>
That sounds like it might be quite useful. What I&#39;m doing is generating some predicates that involve addition/subtraction/comparison of integers and concatenation/comparison of lists of some abstract thing, and then trying to simplify them. An example would be simplifying<br>

<br>
\exists p_before . \exists p_after . \exists q_before . \exists q_after . \exists as . \exists bs . \exists cs . (length p_before == p_pos &amp;&amp; length q_before == q_pos &amp;&amp; (p_before == as &amp;&amp; q_after == cs) &amp;&amp; p_before ++ p_new ++ p_after == as ++ p_new ++ bs ++ q_old ++ cs &amp;&amp; as ++ p_new ++ bs ++ q_old ++ cs == q_before ++ q_old ++ q_after)<br>

<br>
into<br>
<br>
q_pos - (p_pos + length p_new) &gt;= 0<br>
<br>
which uses some properties of length as well as some arithmetic. I don&#39;t expect this all to be done magically for me, but I&#39;d like as much help as possible - at the moment I&#39;ve been growing my own library of predicate transformations but it&#39;s all a bit ad-hoc.<br>

<br>
If I could look at your code I&#39;d be very interested.<br>
<br>
Cheers,<br><font color="#888888">
<br>
Ganesh</font><div><div></div><div class="Wj3C7c"><br>
<br>
On Thu, 4 Dec 2008, Immanuel Normann wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Hi Ganesh,<br>
<br>
manipulating predicate formulae was a central part of my PhD research. I<br>
implemented some normalization and standarcization functions in Haskell -<br>
inspired by term rewriting (like normalization to Boolean ring<br>
representation) as well as (as far as I know) novell ideas (standardization<br>
of quantified formulae w.r.t associativity and commutativity).<br>
If you are interested in that stuff I am pleased to provide you with more<br>
information. May be you can describe in more detail what you are looking<br>
for.<br>
<br>
Best,<br>
Immanuel<br>
<br>
2008/11/30 Ganesh Sittampalam &lt;<a href="mailto:ganesh@earth.li" target="_blank">ganesh@earth.li</a>&gt;<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Hi,<br>
<br>
Are there any Haskell libraries around for manipulating predicate formulae?<br>
I had a look on hackage but couldn&#39;t spot anything.<br>
<br>
I am generating complex expressions that I&#39;d like some programmatic help in<br>
simplifying.<br>
<br>
Cheers,<br>
<br>
Ganesh<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br>
</blockquote>
<br>
</blockquote>
</div></div></blockquote></div><br>