این نسخه‌ی آزمایشی‌ست که روی برد بورد پیاده‌سازی شده (بخاطر همین شلوغ کاری شده) و بعداً هم روی PCB (فایبرگلاس) لحیم‌کاری میشه تا یک مدار یا برد ثابت و خوشگل داشته باشیم... بعداً اگر وقت شد، چندتا ویدیو یا عکس از شکل و نحوه‌ی کارکرد این دستگاه قرار میدم.

امروز می‌خواستم این روز رو به سه دسته از "برنامه‌نویس‌ها" تبریک بگم:
1. اونایی که چند سال اخیر رو فقط با کپی-پیست کردن از LLMها گذروندن و حالا با اعتمادبه‌نفس تمام خودشون رو برنامه‌نویس می‌دونن و خودشون رو مطرح کردن (البته لازم به یادآوری‌ست که کاملا اشتباه هست که این نوع از افراد رو برنامه‌نویس خطاب کنیم)، 2. خود LLMها! بله، هر چی که باشه، از خیلی از دولوپرها بهتر و دقیق‌تر کد می‌زنن و باید ارزش خروجی‌شون رو به خوبی درک کرد، 3. و اما برنامه‌نویس های چپ‌گرای عزیزمون که با کلی کنفرانس، همایش و ایونت، انرژی و وقت گذاشتن، اما تهش ته مسیر هم هیچ‌چیزی نفهمیدیم... نه خودشون می‌دونستن چی می‌خوان، نه ما فهمیدیم هدفشون چی بوده! به هرحال، گویا هرکسی که می‌خواد برنامه‌نویس بشه، از قبل بهش وحی الهی شده و بر این اساس تصمیم داره کل دنیا رو نجات بده:

به‌نظرم، این رابطه رو میشه به صورت یک اپراتور محلی همسایگی روی یک شبکه دوبعدی تفسیر کرد... یعنی در اینجا xᵢ,ⱼ مقدار نقطه (i, j) روی یک شبکه یا ماتریس هست... دو جمع، تمام نقاط موجود در پنجره 3 * 3 پیرامون اون نقطه رو پیمایش میکنن، یعنی
a, b ∈ {-1, 0,1 }
با کم کردن xᵢ,ⱼ خود نقطه حذف میشه و در نتیجه:

پس رابطه در واقع مجموع مقادیر 8 همسایه یک سلول هست و این ساختار هم بیشتر در پردازش تصویر، cellular automata و مدل های شبکه‌ای و محاسبات گسسته کاربرد داره.

پیشنهاد می‌کنم که اگر وقت کردید و تمایل داشتید، مدخل صدق [= Truth] نوشته‌ی Michael Glanzberg، از Stanford Encyclopedia of Philosophy رو مطالعه کنید، چون مفهوم صدق یکی از مسائل بنیادی فلسفه هست و تقریباً با بخش بزرگی از مباحث معرفت‌شناسی، فلسفه زبان و منطق ارتباط داره و مدخلی که آقای Michael Glanzberg نوشته، تلاشی بر ارائه‌ی تصویری منسجم و ساده از مهم‌ترین نظریه‌ها و مسائل معاصر درباره مفهوم حقیقت یا صدق.
در این مدخل، از جمله با این مباحث روبه‌رو می‌شیم:
نظریه‌ی مطابقت [= correspondence theory]
نظریه‌ی انسجام [= coherence theory]
نظریه‌های پراگماتیستی [= pragmatist theories]
نظریه‌ی حقیقت تارسکی [= Tarski’s theory of truth]
رئالیسم و ضدرئالیسم [= realism & anti-realism]
فروکاست‌گرایی درباره حقیقت [Deflationism]
نظریه‌ی افزونگی [= redundancy theory]
نسبت حقیقت با زبان، معنای زبانی و شروط صدق

یکی از بخش های مهم مدخل به نظریه تارسکی اختصاص داره و مفاهیمی مانند Convention T، تعریف بازگشتی حقیقت، ارجاع و ارضا [= satisfaction] رو نیز بررسی می‌کنه. به همین دلیل، این مدخل فقط برای مطالعه‌ی فلسفی مسئله‌ی حقیقت یا صدق نیست یا فقط مختص به دانشجویان فلسفه، بلکه میشه از طریق بقیه‌ی فیلد ها این مداخل رو بررسی یا مطالعه کرد.
نکته‌ی جالب اینکه این مدخل قبلاً به فارسی هم منتشر شده:
دانشنامه فلسفه استنفورد؛ صدق
نویسنده: مایکل گلنزبرگ
مترجم: مهدی محمدی
ناشر: ققنوس
تقریباً ۹۶ صفحه

البته باید توجه داشت که ورژن فارسی کتاب مربوط به انتشار پیشین این مدخل هست و ورژن انگلیسی SEP از زمان انتشار اولیه در 2006 چند بار بازبینی شده و ورژن فعلی اون در 27 ژوئن 2025 بازبینی اساسی شده.

خود مداخل:
https://plato.stanford.edu/archives/fall2025/entries/truth/#NeoClaTheTru

برای خرید نسخه‌ی ترجمه‌شده:
https://www.iranketab.ir/book/142929-truth

Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan, Second Edition, Cambridge University Press, 2004

این کتاب به‌نظرم یکی از نمونه های خیلی خوب از پیوند بین منطق و علم کامپیوتر هست (یعنی کتابی میان‌رشته‌ای‌ست)، یعنی منطق رو صرفاً به عنوان یک موضوع ریاضی مستقل بررسی نمی‌کنه، بلکه از ابتدا دنبال اینکه با استفاده از منطق، سیستم های کامپیوتری و نرم‌افزار رو مدل کنیم و درباره‌ی درستی رفتار اون‌ها به‌صورت صوری استدلال کنیم... ایده‌ی مرکزی کتاب دقیقاً همین هست که برای یک سیستم M و یک specification یا formula مثل φ، بتونیم به صورت دقیق بررسی کنیم که آیا M ⊨ φ برقرار هست یا نه و حتی در بسیاری از موارد این رابطه رو به‌صورت الگوریتمی محاسبه کنیم.
کتاب از Propositional Logic شروع می‌کنه... جایی که علاوه بر formal language و semantics، مباحثی مثل natural deduction, soundness, completeness, normal forms, satisfiability, validity و SAT solving و... رو پوشش میده... حتی صرفاً به تعریف SAT بسنده نمی‌کنه و وارد طراحی و تحلیل solver ها، از یک linear solver تا روش های با پیچیدگی بالاتر، میشه.
بعد وارد Predicate Logic میشه و از syntax, terms, formulas, free و bound variables و substitution می‌گذره و به proof theory, models, semantic entailment, undecidability و expressiveness و... می‌رسه. در ویرایش دوم هم مباحثی از model theory مثل Compactness Theorem و Löwenheim–Skolem Theorem هم اضافه شده و حتی ارتباط منطق با ابزارهایی مثل Alloy برای مدل‌سازی و exploration سیستم‌های under-specified بررسی میشه.
از اینجا به بعد، به‌نظرم کتاب واقعاً وارد وهله یا قلمرو جذاب خودش میشه، یعنی Verification by Model Checking... در این بخش Linear-Time Temporal Logic (LTL) و Computational Tree Logic (CTL), specification patterns, model checking, fairness و الگوریتم های model checking بررسی میشن و در کنار توضیح نظری، ابزار NuSMV هم به‌صورت عملی وارد بحث میشه... بعد هم fixed-point characterization of CTL و مباحث مربوط به monotone functions و correctness الگوریتم ها مطرح میشه.
فصل بعدی کتاب هم میره سراغ Program Verification، یعنی specification و verification کد، Hoare Logic یا Hoare triples, partial و total correctness, proof calculus, proof tableaux و در نهایت programming by contract. اینجا منطق دیگه صرفاً برای اثبات قضایای انتزاعی نیست و مستقیماً به این سوال وصل میشه که چطور می‌تونیم به‌صورت منطقی– ریاضی نشون بدیم یک برنامه واقعاً property موردنظرش رو حفظ می‌کنه.
در ادامه هم Modal Logics and Agents، منطق دانش در multi-agent systems، و در پایان Binary Decision Diagrams (BDDs)، الگوریتم های reduced OBDDs و symbolic model checking بررسی میشن. یعنی مسیر کتاب از منطق گزاره‌ای شروع میشه و قدم‌به‌قدم به جایی می‌رسه که منطق تبدیل به ابزار مدل‌سازی، verification و automated reasoning درباره‌ی سیستم های واقعی کامپیوتری میشه.
به‌طور خلاصه، این کتاب برای کسانی‌ست که می‌خوان بفهمن منطق دقیقاً کجای علم کامپیوتر وارد عمل میشه و از syntax و semantics و proof شروع می‌کنه، به model و temporal logic می‌رسه و بعد اون‌ها رو به model checking, program verification, SAT solving و symbolic reasoning وصل می‌کنه... به همین دلیل هم برای دانشجوی علم کامپیوتر که به logic, formal methods, verification و theoretical computer science علاقه داره، یک منبع خیلی ارزشمند و نسبتاً عمیق محسوب میشه. خود نویسندگان هم در مقدمه تأکید می‌کنن که برای این مسیر، آشنایی با arithmetic مقدماتی و naive set theory کفایت می‌کنه.

درود و وقت بخیر
با شروع نیم‌سال تحصیلی دانشگاه، دوباره مشغله‌های من افزایش یافته هست... علاوه بر فعالیت‌های دانشگاهی، تمرکز اصلی من در ماه‌های آتی بر تکمیل ترجمه‌ی برخی آثار مهم (که ناتمام هستند) و همچنین ضبط یک دوره‌ی آموزشی درباره نظریه‌ی محاسبات، خواهد بود؛ به همین دلیل، احتمالاً مدتی در تلگرام حضور کمتری خواهم داشت.
در این میان، از علاقه‌مندان و متخصصان حوزه های فلسفه، علوم کامپیوتر، آنالیز ریاضی و ریاضیات گسسته دعوت می‌کنم تا در فرآیند نقد متون با من همکاری کنند. اگرچه آثار ترجمه‌شده در نهایت زیر نظر اساتید و متخصصان شناخته‌شده بازبینی نهایی خواهند شد، اما بسیار ارزشمند هست که از دیدگاه مخاطبان دقیق و منتقدان، نظرات و پیشنهادات خود رو جهت بهبود کیفیت کار ارائه بدید. البته بابت این کمک‌ها، بعداً از شما تقدیر و تشکر خواهد شد.
در آخر، اگر مایل بودید، میتونید به آیدی زیر پیام بدید:
@dnyalnr

+ همچنین، اگر تمایل دارید متن‌ها رو از منظر ادبی و نگارشی (شامل بررسی گرامر، انتخاب واژگان و ساختار جملات و...) نقد کنید، خوشحال میشم با من در میان بذارید.