Termination and Reduction Checking in the Logical Framework

The logical framework LF [HHP93] offers concise encodings of deductive systems and their meta-theory. Twelf [SP98] is a realization of LF. It provides a higher-order logic programming language for the implementation of deductive systems as well as a higher-order inductive theorem prover to automatically prove properties about these systems. The inductive theorem prover has been used successfully to prove several challenging theorems like cut-admissibility of intuitionistic logic and the Church-Rosser theorem. Under the proofs-as-programs paradigm the application of the induction hypothesis (IH) in a proof corresponds to the recursive call in a program. To check that the IH application is valid, we need to show that the induction hypothesis is smaller than the induction conclusion according to a well-founded order. This corresponds to proving that the arguments in the recursive call decrease according to a well-founded order, i.e., a program terminates. Twelf uses a termination checker based on structural ordering [RP96] to check termination of programs and to generate valid induction hypotheses according to a given order.