From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,39579ad87542da0e X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.66.121.4 with SMTP id lg4mr7325573pab.41.1368746446321; Thu, 16 May 2013 16:20:46 -0700 (PDT) Path: ln4ni2577pbb.0!nntp.google.com!news.glorb.com!border3.nntp.dca.giganews.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Thu, 16 May 2013 18:20:45 -0500 Newsgroups: comp.lang.ada Date: Thu, 16 May 2013 19:20:43 -0400 From: "Peter C. Chapin" X-X-Sender: peter@whirlwind Subject: Re: Seeking for papers about tagged types vs access to subprograms In-Reply-To: Message-ID: References: <1oy5rmprgawqs.1jz36okze0xju$.dlg@40tude.net> <1q2ql1e4rcgko.diszzq1mhaq8$.dlg@40tude.net> <518dedd4$0$6581$9b4e6d93@newsspool3.arcor-online.net> <1um7tijeo609b$.1gtdijp0acfmn$.dlg@40tude.net> <1nkyb845dehcu.1sd90udwsrpdu.dlg@40tude.net> <1mg9eepp12ood$.14lj7s8a7eygd$.dlg@40tude.net> <1cj8b5amtua30.1foe0rdpldt2.dlg@40tude.net> <5195144f$0$6558$9b4e6d93@newsspool4.arcor-online.net> User-Agent: Alpine 2.02 (DEB 1266 2009-07-14) MIME-Version: 1.0 X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-lGXMKs7mkx0n9Liq1SQgb++CviZxghHm9y790FnrCZ28dXFGDMF5tyg8EcD/NsfzaJanKvhnsKTtmjv!n9HxZY+0VVe6Ccvr7ZZ9cx6KdTlFOPenLCMekPbGCnPZNz7GX09FF5yaNyRS76px/7Ss1UvrTw== X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 4592 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Date: 2013-05-16T19:20:43-04:00 List-Id: On Fri, 17 May 2013, Niklas Holsti wrote: > A proof seems simple enough, assuming that the set of inputs is infinite > and enumerable: if you want to decide whether f1 and f2 are equivalent, > make a program P that iteratively generates (enumerates) all possible > inputs x; computes f1(x) and f2(x); and stops if f1(x) /= f2(x). This > program P halts if and only if f1 /= f2. Since halting is undecidable, > so therefore is function equality. You've shown that the method of enumerating all possible argument values and testing f1(x) = f2(x) doesn't work. But perhaps there is some clever way to statically analyze the code of f1 and f2 to decide their equivalence without having to actually evaluate the functions for all possible inputs. I did a quick Google search on this out of curiosity and it turns out there is a body of work in this area related to optimization. That makes sense. Optimizers would like to make transformations on a given function that generate provably equivalent functions (that are faster or smaller, etc). It's easy to see why people into optimization would care about this. I could imagine some sort of conversation that takes a function to a kind of canonical form... maybe repeated applications of certain primitive transformations on the code... and then showing equivalence would be a matter of comparing the text of the canonical forms of the two functions. I doubt it can be done (in general), but it's not immediately obvious to me that it can't. On the other hand, to prove undecidability one could use a reduction approach. Assume I had a Turing machine program that could take as input two functions (expressed also as Turing machine programs) and , and accept that input if the two functions are equivalent, rejecting it otherwise. Now show how one could transform an arbitrary instance of some known undecidable problem, using a Turing machine and in finite time, to an instance of the equivalence checking problem. If such a transformation could be found, the equivalence checking problem would also be undecidable since a solver for it would imply a solver for the original undecidable problem. Niklas, your approach actually does the reduction in the wrong direction. You showed how one can transform an instance of the equivalence checking problem into an instance of the halting problem. However, that doesn't allow you to conclude equivalence checking is undecidable. Maybe that's just the wrong way to do it. Peter