From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id AFD52BC57 for ; Tue, 7 Sep 2010 15:51:41 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArsDACLghUyACH+RhWdsb2JhbACTSI0/AQEBCgsKBRMith6Ha4U9BA X-IronPort-AV: E=Sophos;i="4.56,328,1280700000"; d="scan'208";a="69009837" Received: from router-304.cs.umd.edu (HELO bacon.cs.umd.edu) ([128.8.127.145]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 07 Sep 2010 15:51:37 +0200 X-CSD-MailScanner-Watermark: 1284472277.48149@Kyrpp503EUcUDeHV9fa06Q Received: from anatase.cs.umd.edu (anatase.cs.umd.edu [172.16.0.207]) (authenticated bits=0) by bacon.cs.umd.edu (8.13.1/8.14.1) with ESMTP id o87DpGlp005560 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NO); Tue, 7 Sep 2010 09:51:17 -0400 Cc: Z.K.Ibrahim@cs.bham.ac.uk Message-Id: From: Elnatan Reisner To: caml-list@yquem.inria.fr In-Reply-To: <20100907100003.A4D67BC57@yquem.inria.fr> Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v936) Subject: Re: interfacing Ocaml with Mathematica Date: Tue, 7 Sep 2010 09:51:16 -0400 References: <20100907100003.A4D67BC57@yquem.inria.fr> X-Mailer: Apple Mail (2.936) X-Greylist: Sender succeeded SMTP AUTH, not delayed by milter-greylist-4.0 (bacon.cs.umd.edu [172.24.3.34]); Tue, 07 Sep 2010 09:51:17 -0400 (EDT) X-CSD-Milter-Status: Skipped o87DpGlp005560 on bacon (user authenticated to SMTP server) X-CSD-MailScanner-Information: Please email staff@cs.umd.edu for more information X-MailScanner-ID: o87DpGlp005560 X-CSD-MailScanner: Found to be clean X-CSD-MailScanner-SpamCheck: not spam, SpamAssassin (not cached, score=-50, required 5, autolearn=not spam, ALL_TRUSTED -50.00) X-CSD-MailScanner-From: elnatan@cs.umd.edu X-Spam: no; 0.00; interfacing:01 ocaml:01 basile:01 basile:01 interfacing:01 ocaml:01 iirc:01 theorems:01 undecidable:01 logarithmic:01 undecidable:01 rewriting:01 coq:01 coq:01 overkill:01 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 > Subject: Re: [Caml-list] interfacing Ocaml with Mathematica > To: zaid al-zobaidi > 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 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