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 条
  • [21] On the Expressive Power of String Constraints
    Day, Joel D.
    Ganesh, Vijay
    Grewal, Nathan
    Manea, Florin
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (POPL):
  • [22] EXPRESSIVE POWER OF RELATIONAL ALGEBRA
    PAREDAENS, J
    INFORMATION PROCESSING LETTERS, 1978, 7 (02) : 107 - 111
  • [23] On the Expressive Power of Priorities in CHR
    Gabbrielli, Maurizio
    Mauro, Jacopo
    Meo, Maria Chiara
    PPDP'09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2009, : 267 - 275
  • [24] Expressive power, mood, and actuality
    French, Rohan
    SYNTHESE, 2013, 190 (09) : 1689 - 1699
  • [25] The expressive power of voting rules
    Bourgeois-Gironde, Sacha
    Ferreira, Joao V.
    SOCIAL CHOICE AND WELFARE, 2024, 62 (02) : 233 - 273
  • [26] Expressive power and abstraction in ESSENCE
    Mitchell, David G.
    Ternovska, Eugenia
    CONSTRAINTS, 2008, 13 (03) : 343 - 384
  • [27] On the expressive power of canonical abstraction
    Sagiv, M
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2004, 2937 : 58 - 58
  • [28] Expressive Power of "Now" and "Then" Operators
    Yanovich, Igor
    JOURNAL OF LOGIC LANGUAGE AND INFORMATION, 2015, 24 (01) : 65 - 93
  • [29] THE EXPRESSIVE POWER OF VOTING POLYNOMIALS
    ASPNES, J
    BEIGEL, R
    FURST, M
    RUDICH, S
    COMBINATORICA, 1994, 14 (02) : 135 - 148
  • [30] On the Expressive Power of Homomorphism Counts
    Atserias, Albert
    Kolaitis, Phokion G.
    Wu, Wei-Lin
    2021 36TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2021,
12345