Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them. Key words: higher order rewriting, termination, dependency pairs, modularity

• Type: Journal
• Year: 2011
• Where: FROCOS
• Authors: Carsten Fuhs, Cynthia Kop
• Keywords: Control Systems, Dependency Pairs, FROCOS 2011, Rewrite System, Rewrite Systems