[m-rev.] for review: fix termination analysis bug

[Zoltan Somogyi]

On 03-Oct-2003, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> Hmm... my intuition is that termination analysis probably ought to take
> the sizes of type_info variables into account, otherwise it won't be
> able to infer termination of any procedure which recursively
> deconstructs types, e.g. io__write_univ.

Knowing the sizes of type_infos is neither necessary nor sufficient
to prove termination of io__write_univ. What *is* both necessary and
sufficient for that is knowing that the deconstruct predicate returns
a list of function symbol argument values that are all individually smaller
than the parent term. Since deconstruct is written outside Mercury,
this requires a programmer annotation.

At the moment, such an annotation would be incorrect, since deconstructing
a typeinfo T1 can yield a list of arguments that includes T1 itself, as well
as terms containing it. As long as this is the case, io__write_univ *won't*
terminate when given a univ containing a type_info, so you don't *want* to
"prove" its termination. Effectively, a typeinfo is a compiler-constructed
circular term.

Zoltan.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------