[Haskell-cafe] manipulating predicate formulae

[Immanuel Normann]

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
>>>
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081205/d1821401/attachment.htm