on termination

Peter Gammie peteg@cse.unsw.EDU.AU
Fri, 9 May 2003 12:45:18 +1000 (EST)

On Fri, 9 May 2003, Andrew J Bromage wrote:

> On Thu, May 08, 2003 at 08:15:11PM +1000, Peter Gammie wrote:
> > Utility? Absolutely none. ;-)
> Not true.  The Mercury group did this analysis for a reason, namely,
> that the transformation:
> 	p :- q, r.
> 	becomes
> 	p :- r, q.
> preserves static semantics in a declarative logic language, however
> it does not preserve operational semantics unless r always terminates.

argh! having a language that satisfies my constraints is pretty useless;
in practice I'd expect you're better off going for Turing completeness +
analysis (ala Mercury, incomplete) or Turing incompleteness + trivial
termination predicate (ala traditional Type Theory - not to belittle the
efforts that go into termination/totality proofs, or expressing programs
in their languages.).