> | 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/ ------- _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users