NEW BOT Телеграм, страница

Forwarded from a pessimistic researcher (Kc)

"در ابتدا تقارن وجود داشت"
از کتاب جزء و کل به نوشته‌ی آقای Werner Heisenberg.
—————————————

چند روز پیش به یک کتاب Open Source برخورد کردم به نام SYMMETRY که چند نویسنده داره و من یکیشون رو یعنی Ulrik Buchholtz رو می‌شناختم. از اونجایی که ایشون Type theory کار هستند، حس کردم کتاب باید حرف تازه‌ای برای گفتن داشته باشه. وقتی که راجع به باقی نویسنده‌های کتاب سرچ کردم فهمیدم که کتاب رو تعدادی TCS کار نوشتن و همونطور که میشه از بکگراند حضرات حدس زد، کتاب بر پایه‌ی univalent mathematics پیش میره و سعی در تعریف یک Foundation برای پاسخ به سوالات مرتبط با Symmetry داره. کتاب با type theory شروع میشه، از group theory عبور می‌کنه، دستی به Automata Theory میده و به تئوری گالوا میرسه. شاید بد نباشه که کمی شفاف کنم که چرا چنین مبحثی برای شخص خودم اهمیت داره.

بر خلاف خیلی از دوستانی که در ماهای گذشته به جمع ما پیوستن، من رشته‌ام ریاضی نیست. اما خب توی Theoretical of computer science به خطوط Track B کانسپت Symmetry و مشتقاتش خیلی به دادمون میرسه. مثلا ما یک دنیایی داریم توی این track به اسم Abstract Interpretation که PL ای‌ها و Compiler ای‌ها ازش خیلی استفاده می‌کنند. به لطف روپاک و رفقاش، verification ای ها هم از ۲۰۰۰ به اینور ازش استفاده می‌کنند. کانسپت Abstract Interpretation برای اولین بار توسط آقایان Patrick Cousot و Radhia Cousot در دهه ۷۰ میلادی معرفی شد. Semantics فرمالی که این بزرگرواران در دو مقاله‌ی معروف و فوق العاده پیچیده‌شون ارائه دادند بر پایه‌ی Lattice Theory و Galois connections بود. یکی دیگه از کاربردای Symmetry توی Model Checking هستش. خیلی از سیستم‌های Concurrent ای که ما میخوایم verify شون کنیم، تشکیل شده از process هایی هستند که رفتار identical دارند و با تعریف یک symmetry reduction ای که sound باشه میشه فضای حالت سیستم رو به شدت کاهش داد. یک نسخه‌ی Generalized شده‌ی Symmetry به ما در verify کردن parameterized concurrent system ها کمک می‌کنه بدین صورت که اگر اثبات کنیم سیستم به‌ازای تعداد مشخصی process وریفای میشه، میشه نتیجه گرفت که به ازای بینهایت process هم وریفای میشه و به ما در verify کردن infinite state systems ها کمک میکنه.

اینها رو گفتم تا بیشتر دید بدم بهتون ولی خودم دنبال چیز دیگه‌ای از Symmetry هستم. یکی از پروژه‌هایی که روی JMC نعریف کردیم، verify کردن distributed system هایی هستش که با پترن Executors/Futures کار می‌کنند. بدین صورت که شما یک Executor دارید که تشکیل شده از یک Thread Pool و یک Runnable Queue هستش و یک سری Task رو به این Executor سابمیت می‌کنید. وقتی که ما اومدیم این پترن رو به شکل فرمال مدل کردیم و بهش یک semantics مبتنی بر dynamic partial order reduction دادیم، دریافتیم که فضای حالت به شکل سوپرنمایی بزرگ میشه وریفای کردنش خیلی راحت نیست. الان دنبال این هستم که بتونم با توسعه و افزودن یک symmetry reduction به این partial order reduction یک تکنیک sound داشته باشم برای کاهش دادن فضای حالت تا بتونیم یک subclass از این مسائل رو به شکل موثری verify کنیم.

از این جهت این کتاب برام جذاب اومد و گفتم که به شما هم معرفیش کنم. نکته‌ای که هست اینه که این کتاب در درست نگارشه و برخی از فصل‌هاش خصوصا فصول انتهاییش کامل نیست. ولی آخرین ورژن Draft این کتاب رو میتونید از طریق این لینک دسترسی داشته باشید. لینک ریپوی این کتاب هم اینجاست.

عنوان پست، جمله‌ای هست که روی جلد کتاب نوشته شده.

10 views20:24