A PROOF-THEORETIC TREATMENT OF λ-REDUCTION WITH CUT-ELIMINATION: λ-CALCULUS AS A LOGIC PROGRAMMING LANGUAGE

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).