Re: interfacing Ocaml with Mathematica

[Elnatan Reisner <elnatan@cs.umd.edu>]

On Sep 7, 2010, at 6:00 AM, caml-list-request@yquem.inria.fr wrote:

> Date: Tue, 7 Sep 2010 06:36:35 +0200
> From: Basile Starynkevitch <basile@starynkevitch.net>
> Subject: Re: [Caml-list] interfacing Ocaml with Mathematica
> To: zaid al-zobaidi <Z.K.Ibrahim@cs.bham.ac.uk>
> Cc: caml-list@yquem.inria.fr
> Message-ID: <20100907063635.f2e4de47.basile@starynkevitch.net>
> Content-Type: text/plain; charset=US-ASCII
>
> On Fri, 03 Sep 2010 16:49:38 +0100
> zaid al-zobaidi <Z.K.Ibrahim@cs.bham.ac.uk> wrote:
>
>> Dear members
>>
>> I am writing an Ocaml code and part of it I need to do the  
>> following job:
>>
>> * I want to find out if two arithmetic or logical expressions  are  
>> equal
>>  like "a + b" and "2 * a + b - a" or "a and b or a" and "a", and  
>> Ocaml
>
> So you want a formal tool working on formal expression trees [you  
> don't want to work on strings]. I believe there are several of these.
>
> And there exist a limitation on them. IIRC, one of Robinson's  
> theorems states that under suitable & reasonable hypothesis the  
> formal equality problem is undecidable (perhaps: equality of  
> functions expressed with an expression made from an unknown x,  
> constants, four usual operations + - * /, square roots,  
> trigonometric, logarithmic, exponential, ... is undecidable)
>
> On the other hand, rewriting such a simplification tool by yourself  
> is a very interesting exercise.
>
>> it is unlikely to achieve my target, therefore I checked the  
>> available
>> packages and tools that can do the job and I found "Mathematica".
>> I would appreciate if someone could guide me on how to interface (if
>> possible)to mathematica from Ocaml programme.
>
> I would choose another tool than Mathematica. I would choose a free  
> (as in speech) software. Very probably, Coq could be used that way  
> (Coq is coded in & interfaced with Ocaml).
> But I don't know it well enough. Coq is a world by itself.

Another possible route, although it might be overkill for your  
specific goal, would be to use an SMT solver.

Two popular ones are Z3 [1] and Yices [2], and both have OCaml APIs.  
CVC3 [3] is another one, this one open-source, with an old OCaml API  
[4], but I have no idea if it works---you'd have to try it or ask the  
author. (Maybe there's a newer OCaml API that I'm unaware of; I just  
found this with a quick Google.)

Elnatan

[1] http://research.microsoft.com/en-us/um/redmond/projects/z3/
[2] http://yices.csl.sri.com/
[3] http://cs.nyu.edu/acsys/cvc3/
[4] https://code.launchpad.net/~cconway/+junk/cvc3-ocaml