Open AccessTermination of dependently typed rewrite rules
Author(s) -
Jean-Pierre Jouannaud,
Jianqi Li
Publication year - 2015
Publication title -
hal (le centre pour la communication scientifique directe)
Language(s) - English
Resource type - Conference proceedings
DOI - 10.4230/lipics.tlca.2015.x
Subject(s) - mathematical proof , dependent type , computer science , programming language , computability , modulo , type (biology) , type theory , base (topology) , order (exchange) , path (computing) , extension (predicate logic) , transformation (genetics) , automated theorem proving , discrete mathematics , theoretical computer science , algebra over a field , mathematics , lambda calculus , pure mathematics , ecology , mathematical analysis , biochemistry , chemistry , geometry , finance , gene , economics , biology
International audienceOur interest is in automated termination proofs of higher-order rewrite rules in presence of dependent types modulo a theory T on base types. We first describe an original transformation to a type discipline without type dependencies which preserves non-termination. Since the user must reason on expressions of the transformed language, we then introduce an extension of the computability path ordering CPO for comparing dependently typed expressions named DCPO. Using the previous result, we show that DCPO is a well-founded order, behaving well in practice