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 条
  • [11] The Expressive Power of Synchronizations
    Laneve, Cosimo
    Vitale, Antonio
    25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, : 382 - 391
  • [12] Expressive power of SQL
    Libkin, L
    THEORETICAL COMPUTER SCIENCE, 2003, 296 (03) : 379 - 404
  • [13] The Expressive Power of SPARQL
    Angles, Renzo
    Gutierrez, Claudio
    SEMANTIC WEB - ISWC 2008, 2008, 5318 : 114 - 129
  • [14] The expressive power of clocks
    Henzinger, TA
    Kopke, PW
    WongToi, H
    AUTOMATA, LANGUAGES AND PROGRAMMING, 1995, 944 : 417 - 428
  • [15] On the expressive power of OKFDDs
    Becker, B
    Drechsler, R
    Theobald, M
    FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (01) : 5 - 21
  • [16] Expressive power of SQL
    Libkin, L
    DATABASE THEORY - ICDT 2001, PROCEEDINGS, 2001, 1973 : 1 - 21
  • [17] ON THE EXPRESSIVE POWER OF COUNTING
    GRUMBACH, S
    TOLLU, C
    THEORETICAL COMPUTER SCIENCE, 1995, 149 (01) : 67 - 99
  • [18] On the Expressive Power of OKFDDs
    Bernd Becker
    Rolf Drechsler
    Michael Theobald
    Formal Methods in System Design, 1997, 11 : 5 - 21
  • [19] On the expressive power of QLTL
    Wu, Zhilin
    Theoretical Aspects of Computing - ICTAC 2007, Proceedings, 2007, 4711 : 467 - 481
  • [20] Pretty Good Democracy for More Expressive Voting Schemes
    Heather, James
    Ryan, Peter Y. A.
    Teague, Vanessa
    COMPUTER SECURITY-ESORICS 2010, 2010, 6345 : 405 - +
12345