توضیحاتی در مورد کتاب :
در دهه 1930، منطقدانان ریاضی مفهوم «توانایی محاسباتی مؤثر» را با استفاده از مفاهیمی مانند توابع بازگشتی، حساب A و ماشینهای تورینگ مطالعه کردند. دهه 1940 شاهد ساخت اولین رایانه های الکترونیکی بود و 20 سال بعد شاهد تکامل زبان های برنامه نویسی سطح بالاتری بودیم که در آن برنامه ها می توانستند به شیوه ای راحت و مستقل (به لطف کامپایلرها و مفسرها) از معماری هر ماشین خاصی نوشته شوند. . توسعه چنین زبان هایی به نوبه خود منجر به تجزیه و تحلیل کلی سؤالات نحو، ساختار رشته های نمادها که می توانند به عنوان برنامه های قانونی به حساب آیند، و معناشناسی، تعیین "معنا" یک برنامه، به عنوان مثال، به عنوان تابعی که در تبدیل محاسبه می کند، انجام شد. داده های ورودی به نتایج خروجی یک رویکرد مهم به معناشناسی، که توسط فلوید، هور، و ویرث پیشگام شد، معناشناسی ادعا نامیده میشود: با توجه به مشخصاتی که در آن ادعاها (پیششرطها) در دادههای ورودی باید تضمین کنند که نتایج، ادعاهای مورد نظر (شرایط پس از آن) در دادههای خروجی را برآورده میکنند، به دنبال دلیل منطقی این است که برنامه با مشخصات آن مطابقت دارد. یک رویکرد جایگزین، که توسط اسکات و استراچی پیشگام شد، معناشناسی دلالتی نامیده میشود: این روش تکنیکهای جبری را برای مشخص کردن نشانههای یک برنامه (یعنی تابع محاسبهشده توسط) ارائه میکند - سپس ویژگیهای برنامه را میتوان با مقایسه مستقیم دلالت بررسی کرد. با مشخصات این کتاب مقدمه ای بر معناشناسی دلالتی است. به طور خاص تر، ما خواننده را با دو رویکرد به معنای شناسی دلالتی آشنا می کنیم: معناشناسی نظم اسکات و استراچی و معناشناسی جزئی افزودنی خودمان.
فهرست مطالب :
Front Matter....Pages i-xi
Front Matter....Pages 1-1
An Introduction to Denotational Semantics....Pages 3-37
An Introduction to Category Theory....Pages 38-70
Partially Additive Semantics....Pages 71-97
Assertion Semantics....Pages 98-115
Front Matter....Pages 117-117
Recursive Specifications....Pages 119-145
Order Semantics of Recursion....Pages 146-175
Canonical Fixed Points....Pages 176-179
Partially Additive Semantics of Recursion....Pages 180-209
Fixed Points in Metric Spaces....Pages 210-231
Front Matter....Pages 233-233
Functors....Pages 235-257
Recursive Specification of Data Types....Pages 258-278
Parametric Specification....Pages 279-292
Order Semantics of Data Types....Pages 293-317
Equational Specification....Pages 318-340
Back Matter....Pages 341-353
توضیحاتی در مورد کتاب به زبان اصلی :
In the 1930s, mathematical logicians studied the notion of "effective comput ability" using such notions as recursive functions, A-calculus, and Turing machines. The 1940s saw the construction of the first electronic computers, and the next 20 years saw the evolution of higher-level programming languages in which programs could be written in a convenient fashion independent (thanks to compilers and interpreters) of the architecture of any specific machine. The development of such languages led in turn to the general analysis of questions of syntax, structuring strings of symbols which could count as legal programs, and semantics, determining the "meaning" of a program, for example, as the function it computes in transforming input data to output results. An important approach to semantics, pioneered by Floyd, Hoare, and Wirth, is called assertion semantics: given a specification of which assertions (preconditions) on input data should guarantee that the results satisfy desired assertions (postconditions) on output data, one seeks a logical proof that the program satisfies its specification. An alternative approach, pioneered by Scott and Strachey, is called denotational semantics: it offers algebraic techniques for characterizing the denotation of (i. e. , the function computed by) a program-the properties of the program can then be checked by direct comparison of the denotation with the specification. This book is an introduction to denotational semantics. More specifically, we introduce the reader to two approaches to denotational semantics: the order semantics of Scott and Strachey and our own partially additive semantics