Souběžné programování logiky omezení - Concurrent constraint logic programming

Souběžné omezení logického programování je verze omezujícího logického programování zaměřené primárně na programování souběžných procesů spíše než (nebo navíc) k řešení problémů s uspokojením omezení . Cíle v logickém programování omezení jsou vyhodnocovány souběžně; souběžný proces je proto programován jako vyhodnocení cíle tlumočníkem .

Syntakticky jsou logické programy souběžných omezení podobné programům nesouběžným, jedinou výjimkou je, že klauzule obsahují stráže , což jsou omezení, která mohou za určitých podmínek blokovat použitelnost klauzule. Sémanticky se souběžné logické programování omezení liší od jeho nesouběžných verzí, protože vyhodnocení cíle je zamýšleno spíše k realizaci souběžného procesu než k nalezení řešení problému. Nejvýznamnější je, že tento rozdíl ovlivňuje, jak se chová tlumočník, když je použitelná více než jedna klauzule: nekonkurentní logické programování omezení rekurzivně zkouší všechny klauzule; souběžné omezení logické programování vybere pouze jeden. Toto je nejzřetelnější účinek zamýšlené směrovosti tlumočníka, který nikdy nezmění volbu, kterou dříve přijal. Dalšími důsledky jsou sémantická možnost mít cíl, který nelze prokázat, zatímco celé hodnocení nezklame, a konkrétní způsob, jak srovnávat cíl a hlavu klauze.

Pravidla manipulace s omezeními lze považovat za formu souběžného logického programování omezení, ale používají se spíše k programování omezovače omezení nebo řešitele než k souběžným procesům.

Popis

V logickém programování omezení jsou cíle v aktuálním cíli vyhodnocovány postupně, obvykle probíhají v pořadí LIFO , ve kterém jsou nejprve hodnoceny novější cíle. Souběžná verze logického programování umožňuje paralelní hodnocení cílů : každý cíl je vyhodnocen procesem a procesy běží souběžně. Tyto procesy interagují prostřednictvím úložiště omezení: proces může přidat omezení do úložiště omezení, zatímco jiný kontroluje, zda je omezení způsobeno úložištěm.

Přidání omezení do úložiště se provádí jako v běžném logickém programování omezení. Kontrola vyplývání z omezení se provádí přes stráže doložek. Stráže vyžadují syntaktické rozšíření: klauzule souběžného programování logiky omezení je psána jako H :- G | Bkde Gje omezení nazývané strážce klauze. Zhruba řečeno, novou variantu této klauzule lze použít k nahrazení literálu v cíli pouze v případě, že stráž je vyvolána úložištěm omezení po přidání rovnice literálu a hlavy klauze. Přesná definice tohoto pravidla je složitější a je uvedena níže.

Hlavní rozdíl mezi logickým programováním bez souběžného a souběžného omezení je v tom, že první je zaměřen na vyhledávání, zatímco druhý je zaměřen na implementaci souběžných procesů. Tento rozdíl ovlivňuje, zda lze volby vrátit zpět, zda je povoleno, aby procesy nebyly ukončeny, a jak jsou cíle a klauzule hlav vyrovnány.

První sémantický rozdíl mezi regulárním a souběžným logickým programováním omezení je o stavu, kdy lze k prokázání cíle použít více než jednu klauzuli. Nesouběžné logické programování zkouší při přepisování cíle všechny možné klauze: pokud nelze cíl prokázat při jeho nahrazení tělem nové varianty klauzule, je prokázána jiná klauzule, pokud existuje. Je to proto, že cílem je prokázat cíl: jsou vyzkoušeny všechny možné způsoby, jak prokázat cíl. Na druhé straně je cílem souběžného logického programování omezení programování paralelních procesů. Obecně souběžné programování, pokud proces provede volbu, tuto volbu nelze vrátit zpět. Souběžná verze logického programování s omezeními implementuje procesy tak, že jim umožňuje přijímat volby, ale po jejich převzetí se k nim zaváže. Technicky vzato, pokud lze k přepsání literálu v cíli použít více než jednu klauzuli, pokusí se nekonkurenční verze postupně všechny klauzule, zatímco souběžná verze zvolí jednu libovolnou klauzuli: na rozdíl od nekonkurenční verze ostatní klauzule nikdy nebude souzen. Tyto dva různé způsoby řešení více možností se často nazývají „neznají nedeterminismus“ a „nezajímají se nedeterminismus“.

Při přepisování literálu v cíli jsou považovány pouze klauzule, jejichž stráž je spojena spojením úložiště omezení a rovnicí literálu s hlavou klauzule. Stráže poskytují způsob, jak zjistit, které klauzule nemají být vůbec brány v úvahu. To je zvláště důležité vzhledem k závazku k jediné klauzuli souběžného omezování logického programování: jakmile bude klauzule zvolena, tato volba nebude nikdy znovu zvážena. Bez stráže by si tlumočník mohl zvolit „nesprávnou“ klauzuli k přepsání doslovného slova, zatímco existují další „dobré“ klauzule. V nesouběžném programování je to méně důležité, protože tlumočník vždy zkouší všechny možnosti. Při souběžném programování se tlumočník zaváže k jediné možnosti, aniž by vyzkoušel jiné.

Druhým účinkem rozdílu mezi nekonkurenční a souběžnou verzí je, že souběžné programování logiky omezení je speciálně navrženo tak, aby umožňovalo spuštění procesů bez ukončení. Nekončující procesy jsou obecně běžné při souběžném zpracování; souběžná verze logického programování s omezeními je implementuje tím, že nepoužívá podmínku selhání: pokud není pro přepsání cíle použitelná žádná klauzule, proces hodnocení tohoto cíle se zastaví místo toho, aby selhalo celé hodnocení, jako v nekonkurenčním logickém programování s omezením. V důsledku toho může být proces vyhodnocování cíle zastaven, protože není k dispozici žádná klauzule, ale ostatní procesy současně běží.

Synchronizace mezi procesy, které řeší různé cíle, je dosaženo použitím stráží. Pokud cíl nelze přepsat, protože všechny klauze, které lze použít, mají ochranný kryt, který není uložen v úložišti omezení, proces řešení tohoto cíle je blokován, dokud ostatní procesy nepřidají omezení, která jsou nezbytná k zajištění ochrany alespoň jednoho příslušných ustanovení. Tato synchronizace podléhá zablokování : pokud jsou blokovány všechny cíle, nebudou přidána žádná nová omezení, a proto nebude nikdy odblokován žádný cíl.

Třetím účinkem rozdílu mezi souběžným a nesouběžným logickým programováním je způsob, jakým je cíl přirovnáván k hlavě nové varianty klauzule. Operačně se to provádí kontrolou, zda proměnné v hlavě lze přirovnat k pojmům takovým způsobem, že hlava se rovná cíli. Toto pravidlo se liší od odpovídajícího pravidla pro logické programování omezení v tom, že umožňuje přidávat omezení pouze ve tvaru variable = term, kde je proměnná jednou z hlav. Toto omezení lze chápat jako formu směrovosti v tom, že s cílem a hlavou klauze se zachází odlišně.

Pravidlo, které říká, zda H:-G|Blze k přepsání cíle použít novou variantu klauze, Aje následující. Nejprve se zkontroluje, zda Aa Hmají stejný predikát. Zadruhé se zkontroluje, zda existuje způsob, jak se vyrovnat s daným aktuálním úložištěm omezení; na rozdíl od běžného logického programování se to děje pod jednostranným sjednocením , které umožňuje, aby se proměnná hlavy rovnala členu. Za třetí, u strážce je zkontrolováno, zda nedošlo k zachycení z úložiště omezení a rovnice vygenerované ve druhém kroku; stráž může obsahovat proměnné, které nejsou uvedeny v hlavičce klauzule: tyto proměnné jsou interpretovány existenciálně. Tuto metodu pro rozhodování o použitelnosti nové varianty klauzule pro nahrazení cíle lze kompaktně vyjádřit takto: aktuální úložiště omezení znamená, že existuje vyhodnocení proměnných hlavy a stráže tak, aby se hlava rovnala branka a strážce jsou spojeny. V praxi lze uvíznutí zkontrolovat pomocí neúplné metody. ${\ displaystyle A}$${\ displaystyle H}$

Rozšíření syntaxe a sémantiky souběžného logického programování je atomic tell . Když tlumočník používá klauzuli, přidá se její ochranný kód do úložiště omezení. Přidána jsou však také omezení těla. Kvůli závazku k této klauzuli tlumočník neprovádí ústup, pokud jsou omezení těla v rozporu s úložištěm. Této podmínce se lze vyhnout použitím atomic tell, což je varianta, ve které klauzule obsahuje jakýsi „druhý strážný“, u kterého se kontroluje pouze konzistence. Taková doložka je napsána H :- G:D|B. Tato klauzule se používá k přepsání literálu pouze v případě, že Gje uložena v úložišti omezení a Dje s ním v souladu. V tomto případě jsou oba Ga Djsou přidány do úložiště omezení.

Dějiny

Studium souběžného logického programování omezení začalo na konci 80. let, kdy Michael J. Maher integroval některé principy souběžného logického programování do logického programování omezení . Teoretické vlastnosti souběžného logického programování omezení byly později studovány různými autory, například Vijayem A. Saraswatem .

Viz také

• Curry , logický funkční programovací jazyk, který umožňuje programování souběžných systémů [1] .
• ToonTalk
• Janus
• Alice

Reference

• Marriott, Kim; Peter J. Stuckey (1998). Programování s omezeními: Úvod . MIT Stiskněte. ISBN  0-262-13341-5
• Frühwirth, Thom; Slim Abdennadher (2003). Základy programování omezení . Springer.ISBN  3-540-67623-6
• Jaffar, Joxan; Michael J. Maher (1994). "Logické programování omezení: průzkum". Časopis logického programování . 19/20: 503–581. doi : 10.1016 / 0743-1066 (94) 90033-7 .

Charakteristický