منطق پویا (منطق وجهی)

منطق پویا (به انگلیسی: Dynamic logic) نوعی گسترش منطق وجهی است. این منطق در اساس برای استنتاج دربارهٔ برنامه‌های رایانه‌ای ساخته شد ولی بعدها به رفتارهای کلی‌تر و پیچیده‌تر در زبان‌شناسی، فلسفه، هوش مصنوعی و دیگر پهنه‌ها اعمال گردید.

زبان

منطق وجهی با عمگرهای وجهی شناخته می‌شود: $\Box p$ (جعبه $p$) ادعا می‌کند که $p$ الزاماً صحیح است، و $\Diamond p$ (لوزی $p$) ادعا می‌کند که $p$ احتمالاً صحیح است. منطق پویا این دو را با ارتباط هر عمل(به انگلیسی: action) که نماد ${\displaystyle a\,\!}$ دارد به عملگرهای وجهی $[a]$ و $\langle a\rangle$ گسترش داده‌است، در نتیجه منطق پویا یک منطق چند-وجهی است. معنی $[a]p$ آن است که «بعد از انجام عمل ${\displaystyle a\,\!}$ لازم است که $p$ برقرار باشد»، یعنی ${\displaystyle a\,\!}$ «باید سبب وقوع» $p$ شود. معنی $\langle a\rangle p$ آن است که «بعد انجام عمل ${\displaystyle a\,\!}$، ممکن است که $p$ برقرار باشد» یعنی «${\displaystyle a\,\!}$ می‌تواند سبب وقوع $p$ شود». این عملگرها توسط این رابطه باهم مرتبط اند: ${\displaystyle [a]p\equiv \neg \langle a\rangle \neg p\,\!}$ و $\langle a\rangle p\equiv \neg [a]\neg p\,\!$. این رابطه مشابه رابطه بین سورهای عمومی (${\displaystyle \forall \,\!}$) و سور وجودی ($\exists \,\!$) است.

منطق پویا این امکان را فراهم می‌کند که «عمل‌های ترکیبی» را از عمل‌های کوچکتر بسازیم. درحالیکه می‌توان از عملگرهای کنترلی اصلی هر زبان برنامه‌نویسی برای این هدف می‌توان استفاده کرد، عبارت باقاعده ی کلینی (Kleene) یک انطباق مناسب به منطق وجهی می‌باشند.

اگر عمل‌های ${\displaystyle a\,\!}$ و ${\displaystyle b\,\!}$ به ما داده شوند:

• عمل ترکیبی ${\displaystyle a\cup b\,\!}$، یا انتخاب، که توسط $a+b\,\!$ یا $a|b\,\!$ نیز نوشته می‌شوند، توسط اجرای یکی از ${\displaystyle a\,\!}$ یا ${\displaystyle b\,\!}$ اجرا می‌گردند.
• عمل ترکیبی ${\displaystyle a{\mathbin {;}}b\,\!}$، یا ترتیب، توسط اجرای اول ${\displaystyle a\,\!}$ و سپس ${\displaystyle b\,\!}$ اجرا می‌گردد.
• عمل ترکیبی ${\displaystyle a{*}\,\!}$، یا تکرار، توسط اجرای ${\displaystyle a\,\!}$ صفر یا بیشتر بار اجرا می‌گردد.
• عمل ثابت ${\displaystyle 0\,\!}$ یا $BLOCK$ هیچ کاری انجام نمی‌دهد و تمام هم نمی‌شود.
• عمل ثابت $1\,\!$ یا SKIP یا NOP، که توسط ${\displaystyle 0{*}\,\!}$ قابل تعریف است، کاری انجام نمی‌دهد، ولی خاتمه یافته‌است.

اصول موضوعی

این عملگرها در منطق پویا به این صورت اصل موضوعی‌بندی می‌گردند. اگر یک اصل‌بندی مناسب برای منطق وجهی به ما داده شده باشد، که شامل این اصول برای عملگرهای وجهی مثل اصل ذکر شده در بالا $[a]p\equiv \neg \langle a\rangle \neg p\,\!$ و دو قاعدهٔ استنتاج وضع مقدم (${\displaystyle \vdash p}$ و ${\displaystyle \vdash p\to q}$ دلالت دارد بر ${\displaystyle \vdash q\,}$) و ضرورت داشتن ($\vdash p$ دلالت دارد بر ${\displaystyle \vdash [a]p\,}$) است، آنوقت:

A1. $[0]p\,\!$

A2. $[1]p\equiv p\,\!$

A3. $[a\cup b]p\equiv [a]p\land [b]p\,\!$

A4. $[a{\mathbin {;}}b]p\equiv [a][b]p\,\!$

A5. $[a*]p\equiv p\land [a][a*]p\,\!$

A6. $p\land [a*](p\to [a]p)\to [a*]p\,\!$

• اصل A1 این قول خالی را می‌دهد که موقعی که BLOCK تمام می‌شود، $p$ برقرار است، حتی اگر $p$ گزارهٔ false باشد. از این رو BLOCK وجود عمل «ابدیت قابل دست یافتن نیست» را انتزاعی می‌کند.
• اصل A2 می‌گوید که NOP به صورت تابع همانی روی گزاره‌ها عمل می‌کند، یعنی این عملگر $p$ را به خودش تبدیل می‌کند.
• اصل A3 می‌گوید اگر انجام یکی از ${\displaystyle a\,\!}$ یا ${\displaystyle b\,\!}$ باید سبب وقوع $p$ شود، آنوقت ${\displaystyle a\,\!}$ باید سبب وقوع $p$ شود و به صورت مشابه برای ${\displaystyle b\,\!}$ و بالعکس.
• اصل A4 می‌گوید اگر انجام ${\displaystyle a\,\!}$ و سپس انجام ${\displaystyle b\,\!}$ باید سبب وقوع $p$ شود، آنوقت ${\displaystyle a\,\!}$ باید سبب وقوع وضعیتی شود که در آن ${\displaystyle b\,\!}$ باید سبب وقوع $p$ شود.
• A5 یک نتیجه آشکار از اعمال A2، A3 و A4 به معادله ${\displaystyle a{*}=1\cup a{\mathbin {;}}a{*}\,\!}$ از جبر کلینی است.
• A6 ادعا می‌کند که اگر $p$ هم‌اکنون برقرار باشد، و مهم نباشد که ما چند بار ${\displaystyle a\,\!}$ را انجام داده‌ایم، آنوقت صحت $p$ بعد از آن اجرا مستلزم صحت آن، بعد از یک اجرای اضافی ${\displaystyle a\,\!}$ است، در این صورت $p$ باید صحیح بماند بدون توجه به اینکه ما چند بار ${\displaystyle a\,\!}$ را اجرا کرده‌ایم. A6 به عنوان استقرای ریاضی شناخته می‌شود، که در آن عمل n := n+1 از افزایش n، توسط عمل اختیاری ${\displaystyle a\,\!}$ تعمیم یافته‌است.