On the expressive power of schemes
Copyright policy )On the expressive power of schemes
We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike $λ$-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 $λ$-calculi.
- INRIA - Centre Sophia-Antipolis France
- Inria Saclay - Île-de-France Research Centre France
- Chinese Academy of Sciences China (People's Republic of)
- INRIA - (INRIA SIEGE) France
- Chinese Academy of Sciences (CAS) China (People's Republic of)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Natural deduction, bound variable, Structure of proofs, proof normalization, Bound variable, Theoretical Computer Science, Computer Science Applications, Logic in Computer Science (cs.LO), Proof normalization, Computational Theory and Mathematics, Combinatory logic and lambda calculus, Cut-elimination and normal-form theorems, natural deduction, Information Systems
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Natural deduction, bound variable, Structure of proofs, proof normalization, Bound variable, Theoretical Computer Science, Computer Science Applications, Logic in Computer Science (cs.LO), Proof normalization, Computational Theory and Mathematics, Combinatory logic and lambda calculus, Cut-elimination and normal-form theorems, natural deduction, Information Systems
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).2 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!