[racket] Symbolic expression, reduction, equivalence, ....

Redex should work well if you're experimenting with not too large
formulas. If you need to reduce huge formulas, you will probably be
better off prototyping in Redex and then porting to Racket itself,
using a datastructure that helps you efficiently manipulate the
formulas.

Robby

On Thu, Jan 19, 2012 at 8:28 AM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> Have you looked at Redex? -- Matthias
>
>
>
> On Jan 19, 2012, at 9:06 AM, David Delfieu wrote:
>
>> Hello
>>
>> I am defining a new algebra with internal compositional laws over symbolic elements.
>>
>> After the definition of the properties of the operators, I would to express well formed formula (wff) in that algebra, which are symbolic expression :
>> (e1 \oplus e2) \perp e3   : for example.
>>
>> I would like to apply theorem reductions on theses wff, pattern matching, and prove that reduced expressions are equivalent.
>>
>> Could you suggest a package which could bring me some interesting functions ?
>>
>> What type of structure could you suggest me to store a wff :
>> mlist, vector, sets, ...
>>
>> Best regards, David.
>>
>> *******************************************************
>> David Delfieu, tel : 02 40 90 50 45
>> EC à Polytech'Nantes - Département Génie Électrique
>> Site de Gavy, 44603 Saint Nazaire Cedex
>> Chercheur à L'IRCCyN
>> *******************************************************
>>
>>
>> ____________________
>>  Racket Users list:
>>  http://lists.racket-lang.org/users
>
>
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users