Thu Dec 4 20:49:35 EST 2008

Hi,

you can browse my code
here.<http://trac.informatik.uni-bremen.de:8080/hets/browser/trunk/Search/Common>It
has become part of
Hets <http://www.dfki.de/sks/hets> the Heterogeneous Tool Set which is a
parsing, static analysis and proof management tool combining various tools
for different specification languages.
However, let me warn you: the code isn't yet well documented at parts also
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):

\begin{enumeratenumeric}
\item $\forall \varepsilon . \varepsilon > 0 \Rightarrow \exists \delta . \forall x. \forall y. 0 < |x - y| \wedge |x - y| < \delta \Rightarrow | f (x) - f (y) | < \varepsilon$

\item $\forall \varepsilon . \exists \delta . \forall x, y. \varepsilon > 0 \Rightarrow (0 < |x - y| \wedge |x - y| < \delta \Rightarrow | f (x) - f (y) | < \varepsilon)$

\item $\forall e . \exists d . \forall a,b. e > 0 \wedge |a - b| < d \wedge 0 < |a - b| \Rightarrow | f (a) - f (b) | < e$
\end{enumeratenumeric}

Cheers,

Immanuel

2008/12/4 Ganesh Sittampalam <ganesh at earth.li>

> Hi,
>
> That sounds like it might be quite useful. What I'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
>
> \exists p_before . \exists p_after . \exists q_before . \exists q_after .
> \exists as . \exists bs . \exists cs . (length p_before == p_pos && length
> q_before == q_pos && (p_before == as && q_after == cs) && p_before ++ p_new
> ++ p_after == as ++ p_new ++ bs ++ q_old ++ cs && as ++ p_new ++ bs ++ q_old
> ++ cs == q_before ++ q_old ++ q_after)
>
> into
>
> q_pos - (p_pos + length p_new) >= 0
>
> which uses some properties of length as well as some arithmetic. I don't
> expect this all to be done magically for me, but I'd like as much help as
> possible - at the moment I've been growing my own library of predicate
> transformations but it's all a bit ad-hoc.
>
> If I could look at your code I'd be very interested.
>
> Cheers,
>
> Ganesh
>
>
> On Thu, 4 Dec 2008, Immanuel Normann wrote:
>
>  Hi Ganesh,
>>
>> manipulating predicate formulae was a central part of my PhD research. I
>> implemented some normalization and standarcization functions in Haskell -
>> inspired by term rewriting (like normalization to Boolean ring
>> representation) as well as (as far as I know) novell ideas
>> (standardization
>> of quantified formulae w.r.t associativity and commutativity).
>> If you are interested in that stuff I am pleased to provide you with more
>> information. May be you can describe in more detail what you are looking
>> for.
>>
>> Best,
>> Immanuel
>>
>> 2008/11/30 Ganesh Sittampalam <ganesh at earth.li>
>>
>>  Hi,
>>>
>>> Are there any Haskell libraries around for manipulating predicate
>>> formulae?
>>> I had a look on hackage but couldn't spot anything.
>>>
>>> I am generating complex expressions that I'd like some programmatic help
>>> in
>>> simplifying.
>>>
>>> Cheers,
>>>
>>> Ganesh
>>> _______________________________________________