instance inference

[Johannes Waldmann]

> | As a termination test, how about no restrictions on context and head
> | except:
> | 
> |    Each assertion in the context must satisfy
> |     * the variables of the assertion are a sub-multiset of those of
> the
> |       head (though they may be the same), and
> |     * the assertion has fewer type constructors and variables (taken
> |       together and counting repetitions) than the head.

it seems you just re-discovered termination proofs by linear
interpretations :-) of course that's just the tip of the iceberg,
see e.g. http://www.cs.tau.ac.il/%7Enachumd/papers/printemp-print.pdf

best regards,
--
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------