برنامه‌نویسی منطقی

برنامه‌نویسی منطقی (به انگلیسی: Logic Programming) یک پارادایم برنامه‌نویسی است که بیشتر آن مبتنی بر منطق صوری است. هر برنامه نوشته‌شده به یک زبان برنامه‌نویسی منطقی مجموعه‌ای از جمله‌ها است که حالت منطقی دارند، که آن جمله‌ها بیانگر «واقعیت» و «قاعده» دربارهٔ یک دامنه مسئله هستند. خانواده‌های زبان برنامه‌نویسی منطقی اصلی شامل پرولوگ، برنامه‌نویسی مجموعه جواب (ASP) و دیتالاگ است. در همه این زبان‌ها، «قاعده‌ها» به حالت «بند» نوشته می‌شوند:

H :- B₁, …, B_n.

که به صورت اعلانی به صورت پیامد منطقی خوانده می‌شود:

H if B₁ and … and B_n.

به H «راس» یا «سر» قاعده گفته می‌شود، و به B₁, … , B_n «بدنه» گفته می‌شود. «واقعیت» قاعده‌ای است که بدنه ندارد، و به صورت ساده‌شده زیر نوشته می‌شود:

H.

در ساده‌ترین حالت که H, B₁, … , B_n همه شان فرمول اتمی هستند، به این بندها بند معین یا بند هورن گفته می‌شود. با این حال گسترش‌های زیادی برای این حالت ساده وجود دارد، که مهمترین گسترش حالتی است که شرط‌های موجود در بدنه بند، توانمندی "نقیض فرمول اتمی بودن" را نیز دارند. زبان‌های برنامه‌نویسی منطقی که شامل این گسترش هستند، توانمندی‌های نمایش دانش را برای منطق غیریکنواخت دارند.

در ASP و Dataloog، برنامه‌های منطقی را فقط به صورت اعلانی می‌توان خواند، و اجرایشان توسط فرایند اثبات، یا مولد مدل انجام می‌شود، که این رفتار در آن‌ها توسط برنامه‌نویس قابل کنترل نیست. با این حال در خانواده پرولوگ از زبان‌ها، برنامه‌های منطقی یک تفسیر رویه‌ای هم وجود دارد، که به صورت «رویه‌های کاهش هدف» است:

to solve H, solve B₁, and … and solve B_n.

بند زیر را به عنوان یک مثال در نظر بگیرید:

fallible(X) :- human(X).

که بر اساس مثالی از آقای تری وینوگراد است، و هدفش توضیح زبان برنامه‌نویسی پلانر است. به عنوان یک بند در برنامه منطقی، از آن هم به عنوان «یک روند برای آزمون آنکه آیا X خطاپذیر است، توسط آزمون آنکه X انسان است استفاده می‌شود»، و هم به صورت «رویه یافتن یک X که خطاپذیر است، از طریق یافتن یک X که انسان است» به کار می‌رود. حتی واقعیت‌ها هم تفسیر رویه‌ای دارند. برای مثال، بند:

human(socrates).

هم قابلیت استفاده به صورت رویه‌ای برای نشان دادن آنکه سقراط انسان است، و هم به صورت رویه‌ای برای یافتن یک X که انسان است، با «انتساب» سقراط به X به کار می‌رود.

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

تاریخچه

استفاده از منطق ریاضی برای نمایش و اجرای برنامه‌های رایانه‌ای اولین بار در دهه ۱۹۳۰ توسط آلونزو چرچ صورت گرفت.

مفاهیم

منطق و کنترل

برنامه‌نویسی منطقی را می‌توان به صورت «استنتاج کنترل‌شده» نگریست. یک مفهوم مهم در برنامه‌نویسی منطقی، جداسازی برنامه‌ها به «مولفهٔ منطقی» و «مولفهٔ کنترلی» است. در زبان‌های برنامه‌نویسی منطقی محض، «فقط» مولفه منطقی جواب‌های تولید شده را تعیین می‌کند. اما مولفه کنترلی برای ایجاد روش‌های متمایز اجرای یک برنامه منطقی قابل تغییر است. این مفهوم توسط این شعار قابل بیان است:

الگوریتم = منطق + کنترل

که در آن «منطق» نمایش‌دهنده یک برنامه منطقی است، و «کنترل» نمایش‌دهنده راهکارهای اثبات قضیه مختلف است.

اثبات مسئله

در حالت ساده و گزاره‌ای، که در آن برنامه منطقی و هدف اتمی سطح بالا، هیچ متغیری ندارند، استدلال پس‌گرد تعیین‌کننده یک درخت and-or است، که یک فضای جستجو را برای حل هدف می‌سازد. هدف سطح بالا همان ریشه درخت است. برای هر گره از درخت و هر بند که سر آن با آن گره منطبق است، یک مجموعه از گره‌های فرزند وجود دارد که متناظر با زیر هدف‌های موجود در بدنه بند هستند. این گره‌های فرزند توسط یک «and» با هم گروهبندی می‌شوند. مجموعه‌های جایگزین از فرزندان که متناظر با راه‌های جایگزین برای آن حل گره‌اند، توسط یک «or» با هم گروهبندی می‌شوند.

از هر راهکار جستجو ای برای جستجوی این فضا می‌توان استفاده کرد. پرولوگ از راهکار پس‌گرد، ورودی آخر-خروجی اول و ترتیبی استفاده می‌کند، که در آن در هر لحظه فقط یک جایگزین و یک زیر هدف در هر زمان درنظر گرفته می‌شود. در دیگر راهکارهای جستجو، مثل جستجوی موازی، پس‌گرد هوشمند، یا جستجوی بهترین-اول برای یافتن یک جواب بهینه، هم ممکن هستند.

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

نقیض به عنوان شکست

برای بیشتر کاربردهای عملی، مثل کاربردهایی که نیاز به استدلال غیریکنواخت در هوش مصنوعی دارند، برنامه‌های منطقی بند هورن را باید به برنامه‌های منطقی نرمال گسترش داد، که در آن شرایط منفی وجود دارد. یک بند در برنامه منطقی نرمال این فرم را دارد:

H :- A₁, …, A_n, not B₁, …, not B_n.

و به صورت اعلانی به صورت یک پیامد منطقی خوانده می‌شود:

H if A₁ and … and A_n and not B₁ and … and not B_n.

که در آن H و همه A_i‌ها و B_i‌ها فرمول اتمی هستند. نقیض موجود در لیترال‌های منفی not B_i به صورت معمول به صورت «نقیض به عنوان شکست (به انگلیسی: negation as failure)» گفته می‌شود، زیرا در بیشتر پیاده‌سازی‌ها یک شرط منفی not B_i را با نشان دادن آنکه شرط مثبت B_i شکست می‌خورد نشان می‌دهند. برای مثال:

canfly(X) :- bird(X), not abnormal(X).
abnormal(X) :- wounded(X).
bird(john).
bird(mary).
wounded(john).

و با هدف معین یافتن چیزی که بتواند پرواز کند:

:- canfly(X).

دو جواب نامزد وجود دارد که زیر هدف اول یعنی bird(X) را حل می‌کند، که X = john و X = mary هستند. دومین زیر هدف not abnormal(john) از راه‌حل نامزد اول شکست می‌خورد، زیرا wounded(john) پیروز می‌شود، و از این رو abnormal(john) پیروز می‌شود. با این حال، زیر هدف دومی not abnormal(mary) از راه‌حل نامزد دومی پیروز می‌شود، زیرا wounded(mary) شکست می‌خورد، و از این رو abnormal(mary) شکست می‌خورد. از این رو، X = mary تنها جواب برای هدف است.

زبان میکروپلنر، یک ساختار به نام "thnot" دارد، که موقعی که به یک عبارت اعمال شود، مقدار درست را فقط (و فقط) وقتی برمی‌گرداند که ارزیابی عبارت شکست بخورد. یک عملگر معادل معمولاً در پیاده‌سازی‌های مدرن پرولوگ وجود دارد. این عملگر معمولاً به صورت not(Goal) یا \+ Goalنوشته می‌شود، که در آن Goal یک هدف (گزاره) است که باید توسط برنامه اثبات شود. این عملگر با نقیض در منطق مرتبه اول متفاوت است: یک نقیض مثل \+ X == 1 موقعی که متغیر X به اتم 1 انتساب یافته باشد، شکست می‌خورد، اما در همه حالت‌های دیگر پیروز می‌شود، که این شامل حالتی است که X انتسابی نداشته باشد. این موضوع استدلال پرولوگ را غیریکنواخت می‌کند: X = 1, \+ X == 1 همیشه شکست می‌خورد اما، عبارت \+ X == 1, X = 1 می‌تواند پیروز شود، اگر X را به 1 انتساب دهیم، بسته به آنکه آیا X از اول انتسابی داشته‌است یا نه (توجه کنید که پرولوگ استاندارد هدف‌ها را به ترتیب چپ-به-راست اجرا می‌کند).

وضعیت منطقی نقیض به صورت شکست تا زمان کیث کلارک (۱۹۷۸) حل نشده بود، که او نشان داد که تحت شرایط طبیعی معین، یک پیاده‌سازی درست (و گاهی کامل) از نقیض کلاسیک، در رابطه با کامل بودن برنامه، است. کامل بودن تقریباً به درنظر گرفتن مجموعه همه بندهای برنامه با یک گزاره مشابه در سمت چپ می‌رسد، اگر بگوییم:

H :- Body₁.

…

H :- Body_k.

به عنوان تعریفی از گزاره‌ی:

H iff (Body₁ or … or Body_k)

که در آن "iff" یعنی "اگر و فقط اگر". نوشتن کامل‌بودن نیاز به استفاده صریح از گزاره تساوی و نیز شمول یک مجموعه از اتم‌های مناسب برای تساوی دارد. با این حال، پیاده‌سازی "نقیض به عنوان شکست" تنها نیاز به نیمه‌های-if از تعاریف، بدون اتم‌های تساوی دارد.

برای مثال مکمل برنامه بالا به این صورت است:

canfly(X) iff bird(X), not abnormal(X).

abnormal(X) iff wounded(X).

bird(X) iff X = john or X = mary.

X = X.

not john = mary.

not mary = john.

مفهوم کامل بودن در بالا، به معناشناسی انحصار مک‌کارتی برای استدلال پیش‌فرض، و نیز به فرض جهانی بسته، بسیار مرتبط است.

به عنوان یک جایگزین برای معناشناسی کامل‌بودن، «نقیض به عنوان شکست» را می‌توان به صورت معرفتی تفسیر کرد، که این موضوع در معناشناسی مدل ثابت برای برنامه‌نویسی مجموعه جواب وجود دارد. در این تفسیر، عبارت not(B_i) به صورت لیترالی، یعنی که B_i را نمی‌دانیم یا به آن عقیده نداریم. «تفسیر معرفتی» این مزیت را دارد که توانایی ترکیب بسیار ساده با نقیض کلاسیک را دارد، این موضوع در «برنامه‌نویسی منطقی گسترش‌یافته» برای صوری‌سازی عباراتی مثل «ضد را نمی‌توان نشان دارد» وجود دارد، که در آن «ضد» همان نقیض کلاسیک، و «را نمی‌توان نشان داد» تفسیر معرفتی از نقیض به صورت شکست است.

نمایش دانش

این واقعیت که «می‌توان به بندهای هورن یک تفسیر رویه‌ای داد»، و برعکس این موضوع که «رویه‌های کاهش هدف را می‌توان به صورت بند هورن + استدلال پس‌گرد شناخت»، یعنی برنامه‌های منطقی نمایش‌های رویه‌ای و اعلانی از دانش را ترکیب کرده‌اند. شمول «نقیض به عنوان شکست» یعنی برنامه‌نویسی منطقی نوعی منطق غیریکنواخت است.

علیرغم سادگی، در مقایسه با منطق کلاسیک، این موضوع ثابت شده‌است که این ترکیب بند هورن با «نقیض به صورت شکست» به طرز شگفت‌آوری گویا و رسا است. برای مثال، یک نمایش طبیعی برای قوانین، حس عام «دلیل» و «تأثیر» ایجاد می‌کند، که هم به صورت حساب وضعیت و هم به صورت حساب واقعه صوری‌سازی شده‌است. نشان داده شده‌است که به صورت کاملاً طبیعی با زبان نیمه صوری قانون‌گذاری متناظر است. به‌خصوص پراکن و سارتور نمایش British Nationality Act را به صورت یک برنامه منطقی اعتبار دادند، که در آن «نفوذ بزرگی برای توسعه نمایش‌های محاسباتی قانون‌گذاری بود، که نشان می‌داد که چگونه برنامه‌نویسی منطقی امکان ایجاد نمایش‌های جذاب بصری را می‌داد، که برای ایجاد استدلال‌های خودکار قابل استقرار مستقیم بود».

جستارهای وابسته

• عبارت هورن
• برنامه‌نویسی تابعی

منابع

مشارکت‌کنندگان ویکی‌پدیا. «Logic programming». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۲۷ مهٔ ۲۰۲۱.