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 |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=63280098&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 63280098 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00224812 3TY jtl: Journal of Symbolic Logic issn: 00224812 maglogo: N pubinfo: dt: Jun2011 vid: 76 iid: 2 pid: 15979 pub: Cambridge University Press artinfo: ui: 63280098 10.2178/jsl/1305810770 ppf: 673 ppct: 27 formats: tig: atl: A PROOF-THEORETIC TREATMENT OF λ-REDUCTION WITH CUT-ELIMINATION: λ-CALCULUS AS A LOGIC PROGRAMMING LANGUAGE. aug: au: GABBAY, MICHAEL affil: Department of Philosophy, Kings College London, Strand, WC2R 2LS, UK su: Logic Mathematics Mathematical logic Calculus Mathematical analysis sug: subj: Logic Mathematics Mathematical logic Calculus Mathematical analysis keyword: cut-elimination lambda-calculus logic programming term-sequent ab: 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). pubtype: Academic Journal doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2011 holdings: @attributes: islocal: N |
|---|