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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id A7182BC57 for ; Tue, 7 Sep 2010 06:36:38 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmIBAA5ehUw+BBBlkWdsb2JhbAChBwEBAQEJCwoHEQMfvhYNhTAElQg X-IronPort-AV: E=Sophos;i="4.56,327,1280700000"; d="scan'208";a="67032045" Received: from smtp-101-monday.nerim.net (HELO kraid.nerim.net) ([62.4.16.101]) by mail1-smtp-roc.national.inria.fr with ESMTP; 07 Sep 2010 06:36:38 +0200 Received: from hector.lesours (ours.starynkevitch.net [213.41.244.95]) by kraid.nerim.net (Postfix) with ESMTP id EFD64CF262; Tue, 7 Sep 2010 06:36:37 +0200 (CEST) Received: from glinka.lesours ([192.168.0.1] helo=glinka) by hector.lesours with smtp (Exim 4.72) (envelope-from ) id 1OspvB-0001en-MZ; Tue, 07 Sep 2010 06:36:37 +0200 Date: Tue, 7 Sep 2010 06:36:35 +0200 From: Basile Starynkevitch To: zaid al-zobaidi Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] interfacing Ocaml with Mathematica Message-Id: <20100907063635.f2e4de47.basile@starynkevitch.net> In-Reply-To: <4C811912.8000106@cs.bham.ac.uk> References: <4C811912.8000106@cs.bham.ac.uk> X-Mailer: Sylpheed 3.1.0beta2 (GTK+ 2.21.7; x86_64-pc-linux-gnu) Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; basile:01 basile:01 interfacing:01 ocaml:01 ocaml:01 iirc:01 theorems:01 undecidable:01 logarithmic:01 undecidable:01 rewriting:01 coq:01 coq:01 cheers:01 equality:01 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. Cheers -- Basile Starynkevitch