on termination

[Peter Gammie]

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.).

cheers
peter