دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
دسته بندی: منطق ویرایش: 1 نویسندگان: J. Roger Hindley سری: Cambridge Tracts in Theoretical Computer Science 42 ISBN (شابک) : 0521054222, 0521465184 ناشر: Cambridge University Press سال نشر: 2008 تعداد صفحات: 199 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 2 مگابایت
در صورت تبدیل فایل کتاب Basic Simple Type Theory به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب تئوری نوع ساده ساده نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
تئوری نوع یکی از مهمترین ابزارها در طراحی زبان های برنامه نویسی سطح بالاتر مانند ML است. این کتاب با تمرکز بر یک سیستم خاص و مطالعه دقیق آن، تکنیک های آن را معرفی و آموزش می دهد. نویسنده با تمرکز بر اصولی که باعث میشود نظریه در عمل عمل کند، تمام ایدههای کلیدی را بدون درگیر شدن در پیچیدگیهای سیستمهای پیشرفتهتر پوشش میدهد. این کتاب یک رویکرد تخصیص نوع به نظریه نوع دارد و سیستم در نظر گرفته شده سادهترین چند شکلی است. نویسنده تمام ایدههای اساسی، از جمله رابطه سیستم با منطق گزارهای را پوشش میدهد و الگوریتم بررسی نوع را که در قلب هر سیستمی قرار دارد، به دقت بررسی میکند. همچنین دو الگوریتم جالب دیگر که تا کنون در ادبیات فنی غیرقابل دسترس مدفون شده اند نیز به نمایش گذاشته شده است. ارائه ریاضی دقیق اما واضح است، و آن را به اولین کتاب در این سطح تبدیل می کند که می تواند به عنوان مقدمه ای برای تئوری تایپ برای دانشمندان کامپیوتر استفاده شود.
Type theory is one of the most important tools in the design of higher-level programming languages, such as ML. This book introduces and teaches its techniques by focusing on one particularly neat system and studying it in detail. By concentrating on the principles that make the theory work in practice, the author covers all the key ideas without getting involved in the complications of more advanced systems. This book takes a type-assignment approach to type theory, and the system considered is the simplest polymorphic one. The author covers all the basic ideas, including the system's relation to propositional logic, and gives a careful treatment of the type-checking algorithm that lies at the heart of every such system. Also featured are two other interesting algorithms that until now have been buried in inaccessible technical literature. The mathematical presentation is rigorous but clear, making it the first book at this level that can be used as an introduction to type theory for computer scientists.
Contents......Page 8 Introduction......Page 10 A. λ-terms and their structure......Page 14 B. β-reduction and β-normal forms......Page 17 C. η- and βη-reductions......Page 20 D. Restricted λ-terms......Page 23 A. The system TA_λ......Page 25 B. The subject-construction theorem......Page 33 C. Subject reduction and expansion......Page 37 D. The typable terms......Page 40 3. The principal-type algorithm......Page 43 A. Principal types and their history......Page 44 B. Type-substitutions......Page 47 C. Motivating the PT algorithm......Page 51 D. Unification......Page 53 E. The PT algorithm......Page 57 A. The equality rule......Page 65 B. Semantics and completeness......Page 70 A. Typed terms......Page 76 B. Reducing typed terms......Page 80 C. Normalization theorems......Page 84 A. Intuitionist implicational logic......Page 87 B. The Curry-Howard isomorphism......Page 92 C. Some weaker logics......Page 98 D. Axiom-based versions......Page 101 A. The converse PT theorems......Page 106 B. Identifications......Page 108 C. The converse PT proof......Page 109 D. Condensed detachment......Page 115 A. Inhabitants......Page 121 B. Examples of the search strategy......Page 127 C. The search algorithm......Page 131 D. The counting algorithm......Page 137 E. The structure of a nf scheme......Page 140 F. Stretching, shrinking and completeness......Page 145 A. The structure of a term......Page 153 B. Residuals......Page 157 C. The structure of a TA_λ-deduction......Page 161 D. The structure of a type......Page 164 E. The condensed structure of a type......Page 166 F. Imitating combinatory logic in λ-calculus......Page 170 Answers to starred exercises......Page 174 Bibliography......Page 182 Table of principal types......Page 190 Index......Page 192