On the expressive power of schemes

被引：0
|
作者：
Dowek, Gilles [1 ]
Jiang, Ying [2 ]
机构：
[1] INRIA, F-75214 Paris 13, France
[2] Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing 100190, Peoples R China
来源：
INFORMATION AND COMPUTATION | 2011年 / 209卷 / 09期
关键词：
Natural deduction; Proof normalization; Bound variable; MODULO; PROOFS;
D O I：
10.1016/j.ic.2011.06.003
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike lambda-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names are introduced for the hypotheses. We show that despite its non-determinism, some typed scheme-calculi have the same expressivity as the corresponding typed lambda-calculi. (C) 2011 Elsevier Inc. All rights reserved.
引用
收藏
页码：1231 / 1245
页数：15
相关论文
共 50 条
12345