The M-computations induced by accessibility relations in nonstandard models M of Hoare logic

doi:10.1007/s11704-015-4024-2

	The M-computations induced by accessibility relations in nonstandard models M of Hoare logic
	Cao, Cungen 1; Sui, Yuefei 1; Zhang, Zaiyue 2
	2016-08-01
发表期刊	FRONTIERS OF COMPUTER SCIENCE
ISSN	2095-2228
卷号	10 期号:4 页码:717-725
摘要	Hoare logic [1] is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure [2]. In a model M of Hoare logic, each program alpha induces an M-computable function f (alpha) (M) on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions f (alpha) (M) induced by programs is equal to the class of all the M-recursive functions. Moreover, each M-recursive function is -definable in M, where the universal quantifier is a number quantifier ranging over the standard part of a nonstandard model M.
关键词	Hoare logic recursive function computable function nonstandard model of Peano arithmetic
DOI	10.1007/s11704-015-4024-2
收录类别	SCI
语种	英语
资助项目	National Natural Science Foundation of China[91224006] ; National Natural Science Foundation of China[61035004] ; National Natural Science Foundation of China[61173063] ; National Natural Science Foundation of China[61203284]
WOS研究方向	Computer Science
WOS类目	Computer Science, Information Systems ; Computer Science, Software Engineering ; Computer Science, Theory & Methods
WOS记录号	WOS:000379533100011
出版者	HIGHER EDUCATION PRESS
引用统计
文献类型	期刊论文
条目标识符	http://119.78.100.204/handle/2XEOYT63/8277
专题	中国科学院计算技术研究所期刊论文_英文
通讯作者	Cao, Cungen
作者单位	1.Chinese Acad Sci, Inst Comp Technol, Key Lab Intelligent Informat Proc, Beijing 100190, Peoples R China 2.Jiangsu Univ Sci & Technol, Dept Comp Sci, Zhenjiang 212003, Peoples R China
推荐引用方式 GB/T 7714	Cao, Cungen,Sui, Yuefei,Zhang, Zaiyue. The M-computations induced by accessibility relations in nonstandard models M of Hoare logic[J]. FRONTIERS OF COMPUTER SCIENCE,2016,10(4):717-725.
APA	Cao, Cungen,Sui, Yuefei,&Zhang, Zaiyue.(2016).The M-computations induced by accessibility relations in nonstandard models M of Hoare logic.FRONTIERS OF COMPUTER SCIENCE,10(4),717-725.
MLA	Cao, Cungen,et al."The M-computations induced by accessibility relations in nonstandard models M of Hoare logic".FRONTIERS OF COMPUTER SCIENCE 10.4(2016):717-725.