* Re: interfacing Ocaml with Mathematica
[not found] <20100907100003.A4D67BC57@yquem.inria.fr>
@ 2010-09-07 13:51 ` Elnatan Reisner
0 siblings, 0 replies; 2+ messages in thread
From: Elnatan Reisner @ 2010-09-07 13:51 UTC (permalink / raw)
To: caml-list; +Cc: Z.K.Ibrahim
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
^ permalink raw reply [flat|nested] 2+ messages in thread
* interfacing Ocaml with Mathematica
@ 2010-09-03 15:49 zaid al-zobaidi
0 siblings, 0 replies; 2+ messages in thread
From: zaid al-zobaidi @ 2010-09-03 15:49 UTC (permalink / raw)
To: caml-list
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
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.
Note: I have to compare the expression and get the result of the
checking back to my Ocaml programme as I want to do the following
comparison that depends on the previous one.
Your help is much appreciated
Cheers,
Zaid
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2010-09-07 13:51 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
[not found] <20100907100003.A4D67BC57@yquem.inria.fr>
2010-09-07 13:51 ` interfacing Ocaml with Mathematica Elnatan Reisner
2010-09-03 15:49 zaid al-zobaidi
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox