The converse principal type-scheme theorem in lambda calculus
Studia Logica 51 (1):83 - 95 (1992)
| Abstract | 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 | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,705 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesNick 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).
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.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads2 ( #232,628 of 549,514 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
