A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language. (English) Zbl 1223.03038

Summary: We build on an existing a term-sequent logic for the \(\lambda \)-calculus. We formulate a general sequent system that fully integrates \(\alpha \beta \eta \)-reductions between untyped \(\lambda \)-terms into first-order logic.
We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for \(\lambda \)-terms. We suggest how this allows us to view the calculus of untyped \(\alpha \beta \)-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).


03F05 Cut-elimination and normal-form theorems
03B40 Combinatory logic and lambda calculus
68N17 Logic programming
68N18 Functional programming and lambda calculus
Full Text: DOI


[1] DOI: 10.1007/978-3-540-32033-3_31
[2] Elements of intuitionism (1977) · Zbl 0358.02032
[3] Second international joint conference on automated reasoning (IJCAR 2004) 3097 pp 460– (2004)
[4] Term rewriting and all that (1998)
[5] DOI: 10.1016/S0304-3975(02)00038-5 · Zbl 1070.68022
[6] DOI: 10.2307/421090 · Zbl 0930.03095
[7] Uniform proofs as a foundation for logic programming (1991) · Zbl 0721.03037
[8] DOI: 10.1093/logcom/1.4.497 · Zbl 0738.68016
[9] Electronic notes in theoretical computer science 4 (2000)
[10] Computer science logic, CSL 2007 4646 pp 451– (2007)
[11] Conditional term rewriting systems 308 (1988) · Zbl 0666.68092
[12] DOI: 10.2307/2025471 · Zbl 0418.03001
[13] Lambda-calculus and combinators, an introduction (2008) · Zbl 1149.03016
[14] Proceedings of the 16th international workshop on functional and (constraint) logic programming (WFLP 2007) pp 47– (2007)
[15] DOI: 10.1007/978-3-642-17511-4_14 · Zbl 1253.03058
[16] Proceedings of the 17th international workshop on functional and (constraint) logic programming (WFLP 2008) 246 pp 87– (2009)
[17] AISC and Calculemos joint international conferences 2385 pp 4– (2002)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.