David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 51 (1):83 - 95 (1992)
A principal type-scheme of a -term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969) 29–60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term.This paper shows a simple proof for the theorem in -calculus, by constructing an algorithm which transforms a type assignment to a -term into a principal type assignment to another -term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW--terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general -terms and BCIW--terms.
|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
M. W. Bunder (1985). A result for combinators, BCK logics and BCK algebras. Logique Et Analyse 28 (9):33.
Citations of this work BETA
No citations found.
Similar books and articles
Nick Chater (1997). What is the Type-1/Type-2 Distinction? Behavioral and Brain Sciences 20 (1):68-69.
Reinhard Muskens (2010). New Directions in Type-Theoretic Grammars. Journal of Logic, Language and Information 19 (2):129-136.
Anita Wasilewska (1984). DFC-Algorithms for Suszko Logic and One-to-One Gentzen Type Formalizations. Studia Logica 43 (4):395 - 404.
René David & Karim Nour (1995). Storage Operators and Directed Lambda-Calculus. Journal of Symbolic Logic 60 (4):1054-1086.
Sachio Hirokawa (1996). The Proofs of Α→Α in P - W. Journal of Symbolic Logic 61 (1):195-211.
Grigori Mints (1993). Resolution Calculus for the First Order Linear Logic. Journal of Logic, Language and Information 2 (1):59-83.
Ken-etsu Fujita (1998). On Proof Terms and Embeddings of Classical Substructural Logics. Studia Logica 61 (2):199-221.
Sachio Hirokawa, Yuichi Komori & Misao Nagayama (2000). A Lambda Proof of the P-W Theorem. Journal of Symbolic Logic 65 (4):1841-1849.
Sabine Broda & Luís Damas (1997). Compact Bracket Abstraction in Combinatory Logic. Journal of Symbolic Logic 62 (3):729-740.
Added to index2009-01-28
Total downloads11 ( #312,527 of 1,906,985 )
Recent downloads (6 months)1 ( #468,221 of 1,906,985 )
How can I increase my downloads?