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
W. W. Tait (2003). The Completeness of Heyting First-Order Logic. Journal of Symbolic Logic 68 (3):751-763.
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.
Twan Laan & Rob Nederpelt (1996). A Modern Elaboration of the Ramified Theory of Types. Studia Logica 57 (2-3):243 - 278.
Harold Simmons (2000). Derivation and Computation: Taking the Curry-Howard Correspondence Seriously. Cambridge University Press.
William W. Tait (2006). Proof-Theoretic Semantics for Classical Mathematics. Synthese 148 (3):603 - 622.
Chris Hankin (1994). Lambda Calculi: A Guide for the Perplexed. Oxford University Press.
Aarne Ranta (1998). Syntactic Calculus with Dependent Types. Journal of Logic, Language and Information 7 (4):413-431.
Added to index2009-01-28
Total downloads10 ( #165,277 of 1,410,090 )
Recent downloads (6 months)4 ( #57,890 of 1,410,090 )
How can I increase my downloads?