LOPSTR 2014: 24th International Symposium on Logic-Based Program Synthesis and Transformation

2014-08-29-LOPSTR

af Henning Christiansen
Prof. Henning Christiansen, CBIT, forskningsgruppe PLIS, deltager i konferencen LOBSTR 2014, med præsentation af en artikel skrevet sammen med ph.d.-studerende Maja Kirkeby fra samme forskningsgruppe. Titlen er »Confluence Modulo Equivalence in Constraint Handling Rules«. Konferencen finder sted i Canterbury, UK, 9.-11. september 2014.

Området er fundamentale studier indenfor teknologi til programmering. Constraint Handling Rules (CHR) er et programmeringssprog baseret på genskrivningsregler. Hvor traditionelle programmeringssprog beskriver en specifik beregningsrækkefølge, er CHR et nondeterministisk sprog, hvis programmer består af en mængde af regler af formen »hvis …. så ….«. Sådanne programmeringssprog er specielt egnede til vidensrepræsentation og ræsonnering, f.eks. anvendt i operationsanalyse, planlægning og kunstig intelligens.

Konfluente programmer – rækkefølgen er ligegyldig
Artiklen her handler om begrebet konfluens: Et program er konfluent såfremt man får samme resultat, uanset hvilken rækkefølge, dets regler bliver anvendt i. Og hvad sjovt er der så ved det? Jo, eksempelvis betyder det, at man kan optimere et program ved at finde den mest effektive rækkefølge at anvende reglerne – man ved så, at det stadigvæk er korrekt. Eller man kan udføre reglerne i parallel og stadigvæk få det rigtige resultat. Det har man kendt til længe sammen med en grundlæggende teori og metoder til at bevise konfluens (hvis det altså holder for det program, man kigger på).

Vores bidrag er at åbne op for, at man kan definere og bevise konfluens, når man tillader visse variationer i slutresultatet. Som et minimalistisk eksempel kan man forestille sig et program, som opsamler en liste af navne på personer, som opfylder visse betingelser; her kan programmøren have besluttet, at rækkefølgen er ligegyldig, dvs. at resultatet [Peter, Jens, Marie] er akkurat lige så godt som [Marie, Jens, Peter]. Dvs. programmøren specificerer de »tilladte variationer« som en ækvivalensrelation (»equivalence« i titlen), og vi tilbyder en teoretisk ramme for at gøre det og metoder til at vise konfluens. På denne måde gør vi begrebet konfluens anvendeligt på en langt større mængde og mere realistisk klasse af programmer.

Ny semantisk definition for CHR
Nu vi var i gang, forbedrede vi også tidligere resultater med en ny semantisk definition for CHR, som er en hel del enklere, end hvad man har brugt tidligere, og som samtidigt dækker en væsentlig større mængde af realistiske programmer (hvor man tidligere holdt sig indenfor en idealiseret delmængde).

Artiklen udgives i første omgang i en lokal publikation, og efter endnu en revision vil den udkomme i Lecture Notes in Computer Science en gang inden jul.

Hvad har det så med design at gøre? Tjah, godt digital design kræver gode IT-implementationer, og går vi et niveau længere ned, for at en udvikler kan designe gode programmer, er det en fordel med gode sprog og værktøjer til formulere og analysere programmer. Og det er her nede, vi kommer ind i billedet.

Læs mere om konferencen LOBSTR 2014 på deres hjemmeside her

Leave a Reply

Your email address will not be published. Required fields are marked *