Higher-order dependency pairs. F. Blanqui. WST'06, 5 pages.

Arts and Giesl proved that the termination of a first-order rewrite system can be reduced to the study of its ``dependency pairs''. We extend these results to rewrite systems on simply typed lambda-terms by using Tait's computability technique.

Erratum:

• Page 4, the assertion before Theorem 4 holds only if, for all l→r ∈ DP(R), FV(r)⊆FV(l), a condition used in Theorem 4 too.