Open AccessTermination Casts: A Flexible Approach to Termination with General Recursion
Author(s) -
Aaron Stump,
Vilhelm Sjöberg,
Stephanie Weirich
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
SCImago Journal Rank - 0.21
H-Index - 7
ISSN - 2398-7340
DOI - 10.29007/3w36
Subject(s) - normalization property , recursion (computer science) , type theory , double recursion , property (philosophy) , term (time) , computer science , typed lambda calculus , simply typed lambda calculus , lambda calculus , type (biology) , primitive recursive function , dependent type , translation (biology) , discrete mathematics , calculus (dental) , algebra over a field , mathematics , programming language , algorithm , pure mathematics , philosophy , dentistry , ecology , chemistry , biology , biochemistry , epistemology , quantum mechanics , medicine , physics , messenger rna , gene
This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form ``Terminates t'', expressing that term t is terminating; and then allow terms t to be coerced from possibly diverging to total, using a proof of Terminates t. We call such coercions termination casts, and show how to implement terminating recursion using them. For the meta-theory of the system, we describe a translation from Teqt to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of Teqt is translated to a theorem expressing the appropriate termination property of the computational part of the Teqt term.