A predicative analysis of structural recursion Export

@article{citeulike:5251872, abstract = {We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation (foetus) of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of terms considered. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. To this end, we define a semantics on all types and a structural ordering on the values in this semantics and prove that all values are accessible with regard to this ordering. Finally, we point out how to do this proof predicatively using set based operators.}, address = {New York, NY, USA}, author = {Abel, Andreas and Altenkirch, Thorsten}, citeulike-article-id = {5251872}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=968426}, citeulike-linkout-1 = {http://dx.doi.org/10.1017/S0956796801004191}, comment = {* Concert Reading Group: 08/11/2009}, doi = {10.1017/S0956796801004191}, issn = {0956-7968}, journal = {J. Funct. Program.}, keywords = {program-analysis, recursion, rg-2009, termination}, number = {1}, pages = {1--41}, posted-at = {2009-08-18 07:43:56}, priority = {2}, publisher = {Cambridge University Press}, title = {A predicative analysis of structural recursion}, url = {http://dx.doi.org/10.1017/S0956796801004191}, volume = {12}, year = {2002} }

TY - JOUR ID - citeulike:5251872 L3 - citeulike-article-id:5251872 N2 - We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation (foetus) of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of terms considered. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. To this end, we define a semantics on all types and a structural ordering on the values in this semantics and prove that all values are accessible with regard to this ordering. Finally, we point out how to do this proof predicatively using set based operators. IS - 1 JF - J. Funct. Program. SN - 0956-7968 AD - New York, NY, USA EP - 41 TI - A predicative analysis of structural recursion PB - Cambridge University Press VL - 12 SP - 1 KW - program-analysis KW - recursion KW - rg-2009 KW - termination N1 - * Concert Reading Group: 08/11/2009 AU - Abel, Andreas AU - Altenkirch, Thorsten PY - 2002/// UR - http://dx.doi.org/10.1017/S0956796801004191 ER -