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)|
References found in this work BETA
A result for combinators, BCK logics and BCK algebras.M. W. Bunder - 1985 - Logique Et Analyse 28 (9):33.
Citations of this work BETA
No citations found.
Similar books and articles
What is the Type-1/Type-2 Distinction?Nick Chater - 1997 - Behavioral and Brain Sciences 20 (1):68-69.
New Directions in Type-Theoretic Grammars.Reinhard Muskens - 2010 - Journal of Logic, Language and Information 19 (2):129-136.
DFC-Algorithms for Suszko Logic and One-to-One Gentzen Type Formalizations.Anita Wasilewska - 1984 - Studia Logica 43 (4):395 - 404.
Storage Operators and Directed Lambda-Calculus.René David & Karim Nour - 1995 - Journal of Symbolic Logic 60 (4):1054-1086.
Resolution Calculus for the First Order Linear Logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
On Proof Terms and Embeddings of Classical Substructural Logics.Ken-etsu Fujita - 1998 - Studia Logica 61 (2):199-221.
A Lambda Proof of the P-W Theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
Added to index2009-01-28
Total downloads11 ( #400,781 of 2,164,542 )
Recent downloads (6 months)1 ( #347,995 of 2,164,542 )
How can I increase my downloads?