Martin Sulzmann wrote,
By possible you mean this extension won't break any of the existing ATS inference results? You have to be very careful otherwise you'll loose decidability.
Can someone explain to me why decidability is of any practical interest at all? What's the (practical) difference between a decision procedure which might never terminate and one which might take 1,000,000 years to terminate? Actually, why push it out to 1,000,000 years: in the context of a compiler for a practical programming language, a decision procedure which might take an hour to terminate might as well be undecidable ... surely all we really need is that the decision procedure _typically_ terminates quickly, and that where it doesn't we have the means of giving it hints which ensure that it will. There's a very nice paper by George Boolos on this[1]: he gives an example of an inference which is (and is intuitively) valid in second- order logic, and which can be first-orderized ... but the proof of the first-order equivalent is completely unfeasible. [1] Boolos, G., A Curious Inference, Journal of Philosophical Logic, 16, 1987. Also in Boolos, Logic, Logic and Logic, 1998. Useful citation here, http://www.nottingham.ac.uk/journals/analysis/preprints/KETLAND.pdf Cheers, Miles