Re: [Haskell-cafe] manipulating predicate formulae
I have no idea if it is relevant, but I wrote a tiny proof assistant for a hilbert style first order logic the other day. http://repetae.net/Hilbert.hs set hasUnicode to False at the top if your terminal doesn't support unicode. fun what one can do in a few hundred lines of haskell.. :) heres the cheat sheet: stack operations 0 duplicate top of lemma stack 1-9 move the specified formula to the top of the stack shift A-Z copy the specified formula from the theorem list to the top of the stack - delete top of lemma stack p promote the top of the lemma stack to a theorem rules of inference d (degeneralize) replace a quantifier with an unbound term g (generalize) universally quantify all unbound terms m use modus pones to apply the top of the stack to the second item in the stack utilities h show this help u undo last operation ! quit John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] manipulating predicate formulae
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 [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] manipulating predicate formulae
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 [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] manipulating predicate formulae
Hi,
you can browse my code
here.http://trac.informatik.uni-bremen.de:8080/hets/browser/trunk/Search/CommonIt
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 [EMAIL PROTECTED]
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 [EMAIL PROTECTED]
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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] manipulating predicate formulae
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/CommonIt
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 [EMAIL PROTECTED]
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 [EMAIL PROTECTED]
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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] manipulating predicate formulae
On Sun, 30 Nov 2008, Neil Mitchell wrote: http://www.cs.york.ac.uk/fp/darcs/proposition/ Unreleased, but might be of interest. It simplifies propositional formulae, and can do so using algebraic laws, custom simplifications or BDDs. I don't really use this library, so if it is of interest to you, its all yours :-) Thanks, but I don't think a propositional library is a good starting point for a predicate library - the problems are too different. Sadly my predicates are over infinite domains, otherwise BDDs would have been really nice :-( Cheers, Ganesh ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] manipulating predicate formulae
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] manipulating predicate formulae
Hi Ganesh, Are there any Haskell libraries around for manipulating predicate formulae? I had a look on hackage but couldn't spot anything. http://www.cs.york.ac.uk/fp/darcs/proposition/ Unreleased, but might be of interest. It simplifies propositional formulae, and can do so using algebraic laws, custom simplifications or BDDs. I don't really use this library, so if it is of interest to you, its all yours :-) Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
