Graduate studies at Western
|Abstract||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)|
No categories specified
(categorize this paper)
|Through your library||Only published papers are available at libraries|
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.
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 downloads5 ( #170,177 of 739,345 )
Recent downloads (6 months)1 ( #61,538 of 739,345 )
How can I increase my downloads?