Games and Full Abstraction for a Functional Metalanguage with Recursive Types

این کتاب ویرایش جزئی پایان نامه ارسال شده در آگوست 1996 است. هیچ تغییر عمده ای ایجاد نشده است. با این حال، می‌خواهم از این فرصت استفاده کنم و اشاره کنم که از زمان نگارش پایان نامه، اکتشافاتی انجام شده است که امکان ساده‌سازی و تقویت قابل‌توجه نتایج را در فصل‌های 3 و 6 فراهم می‌کند. به‌ویژه، اکنون امکان مدل‌سازی صحیح مبالغ وجود دارد. در رده I و همچنین در £، به این معنی که نتایج قابل تعریف فصل 6 را می توان در سطح هدف بیان و اثبات کرد، و آنها را ساده تر و از نظر روحی به اثبات های اصلی Abramsky، Jagadeesan، Malacaria، Hyland نزدیکتر می کند. Ong و Nickau [10،61،79]. این نیز کاملاً مستقیم به درک زبانهای فراخوانی به ارزش منجر می شود. جزئیات این بهبودها را می توان در [14،73] یافت. همچنین شایان ذکر است که در برخی از موضوعات پیشنهادی برای تحقیقات آینده در فصل 7 پیشرفت هایی حاصل شده است. به ویژه، مدل های کاملاً انتزاعی برای انواع مختلف زبان ها با متغیرهای محلی پیدا شده است [8،13-16]، و یک مدل بازی کاملاً کامل از زبان چندشکلی System F توسط هیوز ساخته شده است [59]. گای مک کاسکر فوریه 1998 قدردانی ها اول از همه، باید از سرپرستم، سامسون آبرامسکی تشکر کنم. او بود که برای اولین بار مرا با معناشناسی بازی آشنا کرد و راه های تحقیق در این منطقه را پیشنهاد کرد. اگر او نبود این کتاب قطعا وجود نداشت.

This book is a minor revision of the thesis submitted in August 1996; no major changes have been made. However, I would like to take this opportunity to mention that since the thesis was written, discoveries have been made which would allow a substantial simplification and strengthening of the results in Chapters 3 and 6. In particular, it is now possible to model sums correctly in the category I as well as in £, which means that the definability results of Chapter 6 can be stated and proved at the intensional level, making them simpler and much closer in spirit to the original proofs of Abramsky, Jagadeesan, Malacaria, Hyland, Ong and Nickau [10,61,79]. This also leads quite straightforwardly to an understanding of call-by-value languages. Details of these improvements can be found in [14,73]. It is also worth mentioning that progress has been made on some of the topics suggested for future research in Chapter 7. In particular, fully abstract models have been found for various kinds of languages with local variables [8,13-16], and a fully complete games model of the polymorphic language System F has been constructed by Hughes [59]. Guy McCusker February 1998 Acknowledgements First of all, I must thank my supervisor, Samson Abramsky. It was he who first introduced me to game semantics and suggested avenues of research in the area; this book would certainly not exist were it not for him.