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 λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-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...
| Publicado en: | Journal of Symbolic Logic Vol. 76; no. 2; pp. 673 - 700 |
|---|---|
| Autor principal: | |
| Formato: | Artículo |
| Publicado: |
Cambridge University Press
Jun2011
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| Sumario: | We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-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 λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen). |
|---|