19 Dec
2005
19 Dec
'05
5:56 a.m.
| 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/ -------