[Haskell-cafe] manipulating predicate formulae
ganesh at earth.li
Fri Dec 5 01:33:44 EST 2008
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?
On Fri, 5 Dec 2008, Immanuel Normann wrote:
> you can browse my code
> 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
> \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 >
> \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$
> 2008/12/4 Ganesh Sittampalam <ganesh at earth.li>
>> 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)
>> 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.
>> 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
>>> 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
>>> 2008/11/30 Ganesh Sittampalam <ganesh at earth.li>
>>>> Are there any Haskell libraries around for manipulating predicate
>>>> I had a look on hackage but couldn't spot anything.
>>>> I am generating complex expressions that I'd like some programmatic help
>>>> Haskell-Cafe mailing list
>>>> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe