A Simplified Application of Howard's Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems

摘要

There have been some important methods of combining a recursive path ordering and Tait-Girard's computability argument to provide an ordering for termination proofs of higher-order rewrite systems. The higher-order recursive path ordering HORPO by Jouannaud and Rubio and the computability path ordering CPO by Blanqui, Jouannaud and Rubio are examples of such an ordering. In this paper, we give a case study of yet another direction of such extension of recursive path ordering, avoiding Tait-Girard's computability method plugged in the above mentioned works. This motivation comes from Levy's question in the RTA open problem 19, which asks for a reasonably straightforward interpretation of simply typed λ-calculus λ_→ in a certain well founded ordering. As in the cases of HORPO and CPO, the addition of λ-abstraction and application into path orderings might be considered as one solution, but the following question still remains; can the termination of λ_→ be proved by an interpretation in a first-order well founded ordering in the sense that λ-abstraction/application are not directly built in the ordering? Reconsidering one of Howard's works on proof-theoretic studies, we introduce the path ordering with Howard algebra as a case study towards further studies on Levy's question.