David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
The reduction of the lambda calculus to the theory of combinators in [Sch¨ onfinkel, 1924] applies to positive implicational logic, i.e. to the typed lambda calculus, where the types are built up from atomic types by means of the operation A −→ B, to show that the lambda operator can be eliminated in favor of combinators K and S of each type A −→ (B −→ A) and (A −→ (B −→ C)) −→ ((A −→ B) −→ (A −→ C)), respectively.1 I will extend that result to the case in which the types are built up by means of the general function type ∀x : A.B(x) as well as the disjoint union type ∃x : A.B(x)– essentially to the theory of [Howard, 1980]. To extend the treatment of −→ to ∀ we shall need a generalized form of the combinators K and S, and to deal with ∃ we will need to introduce a new form of the combinator S..
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Aarne Ranta (1998). Syntactic Calculus with Dependent Types. Journal of Logic, Language and Information 7 (4):413-431.
Chris Hankin (1994). Lambda Calculi: A Guide for the Perplexed. Oxford University Press.
William W. Tait (2006). Proof-Theoretic Semantics for Classical Mathematics. Synthese 148 (3):603 - 622.
Harold Simmons (2000). Derivation and Computation: Taking the Curry-Howard Correspondence Seriously. Cambridge University Press.
Twan Laan & Rob Nederpelt (1996). A Modern Elaboration of the Ramified Theory of Types. Studia Logica 57 (2-3):243 - 278.
Anna Szabolcsi (2003). Binding On the Fly: Cross-Sentential Anaphora in Variable— Free Semantics. In R. Oehrle & J. Kruijff (eds.), Resource Sensitivity, Binding, and Anaphora. Kluwer 215--227.
W. W. Tait (2003). The Completeness of Heyting First-Order Logic. Journal of Symbolic Logic 68 (3):751-763.
Added to index2009-01-28
Total downloads13 ( #179,414 of 1,700,303 )
Recent downloads (6 months)5 ( #128,702 of 1,700,303 )
How can I increase my downloads?