[Haskell-cafe] manipulating predicate formulae

[Ganesh Sittampalam]

Thanks - I'll take a look. One pre-emptive question: if I want to use it, 
it'd be more convenient, though not insurmountable, if that code was 
BSD3-licenced, since it will fit in better with the licence for camp 
<http://projects.haskell.org/camp>, which I might eventually want to 
integrate my code into. (the predicates I described are intended to be the 
commutation conditions for patches). Is that likely to be possible?

Cheers,

Ganesh

On Fri, 5 Dec 2008, Immanuel Normann wrote:

> 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
> ad hoc. Don't know whether it can help to solve your tasks.
> 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
>>>> _______________________________________________
>>>> Haskell-Cafe mailing list
>>>> Haskell-Cafe at haskell.org
>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>>
>>>>
>>>
>