🧠 کتاب The Formal Semantics of Programming Languages تکنیک‌های پایه ریاضی موردنیاز برای شروع مطالعه معناشناسی و منطق زبان‌های برنامه‌نویسی رو آموزش میده. این تکنیک‌ها به دانشجوها کمک میکنن قواعدی رو ابداع، صورت‌بندی و اثبات کنن که با استفاده از اون‌ها میشه درباره زبان‌های برنامه‌نویسی مختلف استدلال کرد.

🔬 با اینکه مطالب کتاب از سطح مقدماتی شروع میشن، چند موضوع اون از پژوهش‌های جدید گرفته شده‌اند؛ از جمله حوزه مهم هم‌زمانی. کتاب تمرین‌های زیادی داره که از سؤال‌های ساده تا پروژه‌های کوچک رو شامل میشن.

📐 کتاب با نظریه مقدماتی مجموعه‌ها شروع میشه و بعد معناشناسی عملیاتی ساختاریافته رو به‌عنوان روشی برای تعریف معنای زبان‌های برنامه‌نویسی معرفی میکنه. تکنیک‌های اثبات مرتبط با این رویکرد هم در ادامه توضیح داده میشن.

🧩 معناشناسی دلالتی و اصل‌موضوعی با استفاده از یک زبان ساده شامل برنامه‌های while بررسی میشن. کتاب اثبات‌های کاملی از هم‌ارزی معناشناسی عملیاتی و دلالتی، همین‌طور درستی و کامل بودن نسبی معناشناسی اصل‌موضوعی ارائه میده.

📜 اثباتی از قضیه ناتمامیت گودل هم در کتاب قرار داره که نشون میده دستیابی به یک معناشناسی اصل‌موضوعی کاملاً کامل امکان‌پذیر نیست. یک پیوست هم برای پشتیبانی از این بخش ارائه شده که مقدمه‌ای بر نظریه محاسبه‌پذیری بر پایه برنامه‌های while داره.

🌐 بعد از معرفی نظریه دامنه، معناشناسی و روش‌های اثبات برای چند زبان تابعی بررسی میشن. ساده‌ترین زبان مطرح‌شده، زبان معادلات بازگشتیه که هر دو روش ارزیابی Call-by-Value و Call-by-Name رو پوشش میده.

🔄 این بحث بعدتر به زبان‌هایی با نوع‌های مرتبه‌بالا و بازگشتی گسترش پیدا میکنه و حساب لامبدای Eager و Lazy رو هم شامل میشه. در سراسر کتاب، رابطه بین معناشناسی دلالتی و عملیاتی اهمیت زیادی داره و اثبات‌های مربوط به تطابق این دو نوع معناشناسی ارائه میشن.

🧠 بررسی نوع‌های بازگشتی که یکی از بخش‌های پیشرفته‌تر کتابه، بر استفاده از سیستم‌های اطلاعاتی برای نمایش دامنه‌ها تکیه داره.

⚙️ کتاب در پایان به زبان‌های برنامه‌نویسی موازی میپردازه و روش‌های مشخص‌سازی و اعتبارسنجی برنامه‌های غیرقطعی و موازی رو بررسی میکنه.

📖 فهرست مطالب

فصل ۱. نظریه مقدماتی مجموعه‌ها

فصل ۲. مقدمه‌ای بر معناشناسی عملیاتی

فصل ۳. برخی اصول استقرا

فصل ۴. تعریف‌های استقرایی

فصل ۵. معناشناسی دلالتی IMP

فصل ۶. معناشناسی اصل‌موضوعی IMP

فصل ۷. کامل بودن قواعد Hoare

فصل ۸. مقدمه‌ای بر نظریه دامنه

فصل ۹. معادلات بازگشتی

فصل ۱۰. تکنیک‌های بازگشت

فصل ۱۱. زبان‌هایی با نوع‌های مرتبه‌بالا

فصل ۱۲. سیستم‌های اطلاعاتی

فصل ۱۳. نوع‌های بازگشتی

فصل ۱۴. عدم قطعیت و موازی‌سازی

👤 درباره نویسنده

👨‍🏫 گلین وینسکل استاد علوم کامپیوتر در University of Aarhus دانمارک است.

The Formal Semantics of Programming Languages provides the basic mathematical techniques necessary for those who are beginning a study of the semantics and logics of programming languages. These techniques will allow students to invent, formalize, and justify rules with which to reason about a variety of programming languages. Although the treatment is elementary, several of the topics covered are drawn from recent research, including the vital area of concurency. The book contains many exercises ranging from simple to miniprojects.Starting with basic set theory, structural operational semantics is introduced as a way to define the meaning of programming languages along with associated proof techniques. Denotational and axiomatic semantics are illustrated on a simple language of while-programs, and fall proofs are given of the equivalence of the operational and denotational semantics and soundness and relative completeness of the axiomatic semantics. A proof of Godel's incompleteness theorem, which emphasizes the impossibility of achieving a fully complete axiomatic semantics, is included. It is supported by an appendix providing an introduction to the theory of computability based on while-programs. Following a presentation of domain theory, the semantics and methods of proof for several functional languages are treated. The simplest language is that of recursion equations with both call-by-value and call-by-name evaluation. This work is extended to lan guages with higher and recursive types, including a treatment of the eager and lazy lambda-calculi. Throughout, the relationship between denotational and operational semantics is stressed, and the proofs of the correspondence between the operation and denotational semantics are provided. The treatment of recursive types - one of the more advanced parts of the book - relies on the use of information systems to represent domains. The book concludes with a chapter on parallel programming languages, accompanied by a discussion of methods for specifying and verifying nondeterministic and parallel programs.

Table of Contents

1 Basic set theory

2 Introduction to operational semantics

3 Some principles of induction

4 Inductive definitions

5 The denotational semantics of IMP

6 The axiomatic semantics of IMP

7 Completeness of the Hoare rules

8 Introduction to domain theory

9 Recursion equations

10 Techniques for recursion

11 Languages with higher types

12 Information systems

13 Recursive types

14 Nondeterminism and parallelism

About the Author

Glynn Winskel is Professor of Computer Science at the University of Aarhus, Denmark.