Formalizing non-termination of recursive programs

被引：2
作者：
Kahle, R
Studer, T
机构：
[1] Univ Tubingen, WSI, D-72076 Tubingen, Germany
[2] Univ Bern, Inst Informat & Angew Math, CH-3012 Bern, Switzerland
来源：
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING | 2001年 / 49卷 / 1-2期
关键词：
applicative theories; least fixed point operator; non-termination;
D O I：
10.1016/S1567-8326(01)00006-6
中图分类号：
学科分类号：
摘要：
In applicative theories the recursion theorem provides a term rec which solves recursive equations. However, it is not provable that a solution obtained by rec is minimal. In the present paper we introduce an applicative theory in which it is possible to define a least fixed point operator. Still, our theory has a standard recursion theoretic interpretation. (C) 2001 Elsevier Science Inc. All rights reserved.
引用
收藏
页码：1 / 14
页数：14
相关论文
共 35 条
[1]  
Amadio Roberto M, 1998, Domains and lambda calculi
[2]  
[Anonymous], LOGIC C
[3]  
BARENDREGT H, 1984, LAMBDA CALCULUS
[4]  
Beeson M.J., 1985, Foundations of Constructive Mathematics
[5]  
Curry H., 1972, Combinatory Logic, V2
[6]  
Feferman, 1975, LECT NOTES MATH, P87, DOI DOI 10.1007/BFB0062852
[7]   SYSTEMS OF EXPLICIT MATHEMATICS WITH NONCONSTRUCTIVE MU-OPERATOR .1 [J].
FEFERMAN, S ;
JAGER, G .
ANNALS OF PURE AND APPLIED LOGIC, 1993, 65 (03) :243-263
[8]  
FEFERMAN S, 1992, LECT NOTES COMPUT SC, V626, P79, DOI 10.1007/BFb0023759
[9]  
FEFERMAN S, 1992, PROOF THEORY, P195
[10]  
FEFERMAN S, 1991, MSRI PUBLICATIONS, V21, P95
1234