interfacing Ocaml with Mathematica

interfacing Ocaml with Mathematica

[zaid al-zobaidi]

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

Re: [Caml-list] interfacing Ocaml with Mathematica

[Basile Starynkevitch]

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.

Cheers

-- 
Basile Starynkevitch <basile@starynkevitch.net>

Re: [Caml-list] interfacing Ocaml with Mathematica

[Florent Ouchet]

Hello,

You might be interested in the evaluation core of VSyml [1], which is  
not Mathematica-based.

The module DesignEval rewrites and evaluates function trees whose  
types are defined in the module DesignTypes. However, this project  
aims at symbolically simulate VHDL code, (by mixing immediate values  
and variables - denoted at symbols - in expression trees) and  
therefore it might be a little bit oversized for your needs. The  
boolean rewrite rules are quite efficient although the arithmetic  
rewriting rules might need some rework for corner cases.

Here is an example of how to invoke the evaluator:

(* make all && cd build/byte && ocaml *)
#load "nums.cma";;
#load "Resources.cmo";;
#load "OCamlUtils.cmo";;
#load "DesignTypes.cmo";;
#load "DesignStandardTypes.cmo";;
#load "DesignUtils.cmo";;
#load "DesignAttributes.cmo";;
#load "DesignLogic.cmo";;
#load "DesignSolver.cmo";;
#load "DesignEval.cmo";;

open DesignStandardTypes;; (* for boolean type definition *)
open DesignTypes;; (* for formula types *)
open DesignEval;; (* for evaluator definitions *)

let a_symbol = FormulaSymbol {symboltype=vhdl_boolean_type;symbolname="a"};;
let b_symbol = FormulaSymbol {symboltype=vhdl_boolean_type;symbolname="b"};;

let or_formula = FormulaAssociativeOperator (OperatorAssociativeOr,  
[a_symbol;b_symbol]);;
let formula = FormulaAssociativeOperator  
(OperatorAssociativeAnd,[a_symbol;or_formula]);;

designeval_formula formula default_struct_context default_eval_context;;
--> returns a_symbol

The syntax is /a little bit/ verbose, but that's required to evaluate  
complex VHDL expression. It supports associative and/unary  
and/or/nand/nor/xor/xnor/unary -/-/+/*/// and many others...

Best Regards,

- Florent Ouchet

[1] http://users-tima.imag.fr/vds/ouchet/vsyml.html

-- 
Florent Ouchet
PhD Student, CIS/VDS Groups
TIMA Laboratory, Grenoble, France

Re: [Caml-list] interfacing Ocaml with Mathematica

[Frederic Chyzak]

Hi,

On Fri, 2010-09-03 at 16:49 +0100, zaid al-zobaidi wrote:
> 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 not clear to me what power of symbolic computation you really
need.

If you really need to be able to interface a computer-algebra system
with ocaml (whether Mathematica or Maple or ...), you might be
interested to hear that we are developing a tool [1] named DynaMoW
(for Dynamic Mathematics on the Web) for this purpose.  (Well, beyond
this, our purpose is to generate web pages with dynamic mathematical
content).  We cannot unfortunately point you to a public release as we
expect our first release only later this fall.

Concerning the test you were asking for, it could be coded as follows
using DynaMoW's quotations and antiquotations, and Mathematica's
syntax:

  let s1 = <:symb< a + b >> and s1 = <:symb< 2 * a + b - a >> in
  let b = <:bool< If[ $(symb:s1) == $(symb:s2), True, False, False ] >>
in
  if b then "equal" else "different" ;;

If this really is the route you have to go, we are ready to discuss it
further.

Best regards,
Frédéric Chyzak and Alexis Darrasse


[1] http://ddmf.msr-inria.inria.fr/DynaMoW/

Re: interfacing Ocaml with Mathematica

[Elnatan Reisner]

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