The work is on theoretical aspects motivated from computer science like term rewriting and its termination, decomposition systems arising from orders on signatures, labels, \(\lambda\)-calculus etc.
Kruskal’s theorem asserts that tree embedding extension of a well order on labels is also a well order. The author’s attempt to extend the scope of the recursive path ordering (RPO) techniques to higher-order calculi like \(\lambda\)-calculus led to the axiomatic proof of a generalization of Kruskal’s theorem to binary relations.
It is a simple but fruitful observation of the author that the complement of the reverse of a well order is a noetherian order at the level of binary relations. This complement of reverse is a duality which translates the presented binary relational version of Kruskal’s theorem to special decomposition systems and noetherian orders (so-called dual Kruskal theorem).
It is shown that this dual Kruskal theorem is an instance of the Fereira-Zantema theorem on term lifting and Dershowitz’s theorem on RPOs.
A similar duality arose in the theory of Galois-Tukey connections on binary relations and was used to translate theorems, e.g., between measure and category [see the reviewer, “Generalized Galois-Tukey-connections between explicit relations on classical objects of real analysis”, Isr. Math. Conf. Proc. 6, 619-643 (1993; Zbl 0829.03027) and “A lattice of binary relations with polarity”, Tatra Mt. Math. Publ. 5, 143-150 (1995; Zbl 0853.06003)].
For the entire collection see [Zbl 0893.00039].