Ganesh Sittampalam ganesh at earth.li
Thu Dec 4 17:00:18 EST 2008

```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
>> _______________________________________________