Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!zaphod.mps.ohio-state.edu!cis.ohio-state.edu!pacific.mps.ohio-state.edu!linac!midway!msuinfo!rang
From: rang@cs.wisc.edu (Anton Rang)
Newsgroups: comp.lang.misc
Subject: Re: Halting Problem Solved! Film at 11! (Was Re: definitions)
Message-ID: <RANG.91May11192903@nexus.cs.wisc.edu>
Date: 11 May 91 23:29:03 GMT
References: <30040@dime.cs.umass.edu> <1991May4.192440.5527@sctc.com>
	<30095@dime.cs.umass.edu> <1991May6.021753.4373@agate.berkeley.edu>
	<30227@dime.cs.umass.edu>
Sender: news@msuinfo.cl.msu.edu
Organization: UW-Madison CS department
Lines: 55
In-Reply-To: yodaiken@chelm.cs.umass.edu's message of 8 May 91 14:50:33 GMT

In article <30227@dime.cs.umass.edu> yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:

>Thus, if our compiler provides a sorting algorithm, and we attempt to
>compile a program which applies the sorting operator to a sequence
>that cannot be sorted on our machine, then it would be both useful
>and theoretically possible to have the compiler find and report the
>error.

  Right.  We have ways of doing this in a suboptimal way (e.g. assume
that all branches are taken), but they're not as useful as we'd like,
since obviously real programs don't always do that.  For instance, the
program (in pseudo-code):

	list := []
	if A == B then
	  list := append(list, 3)
	else
	  list := append(list, 'x')
	fi
	if A == B then
	  list := append(list, 4)
	else
	  list := append(list, 'y')
	fi
	sort(list)

  It's pretty obvious that the list at this point will contain either
only integers, or only characters, so that we should be able to sort
it.  However, a compiler may not be able to figure this out, at least
in the general case.

>Maybe we can even do better than that, and have an algorithm that
>will compute TypeSafe(Prog,Bound) so that any machine M that fits
>within the Bound is typesafe. If our compiler could test
>TypeSafe(Prog,Anything-with-at-least-2^32-addressable-words) this
>would would be quite useful.

  It's possible, but it's unlikely that you can write a compiler which
will check this *within* the bounds of the machine, or which can do it
in a reasonable amount of time, etc.  It's conceivable, but how about
this example....

	list := ['a']
	for i in (some finite stream of even numbers)
	  if (we cannot find two prime numbers which add up to i) then
	    list := append(list, i)
	  fi
	rof

  Now, in the general case, the list will be safe iff Goldbach's
conjecture holds.  If we can figure out what numbers are generated in
the stream (perhaps bound them by some maximum integer), we can
obviously test whether this will hold, but it's not really feasible.

	Anton
   
+---------------------------+------------------+-------------+----------------+
| Anton Rang (grad student) | rang@cs.wisc.edu | UW--Madison | "VMS Forever!" |
+---------------------------+------------------+-------------+----------------+