PROGRAMARE PRIN RESCRIERE

Cartea conține o prezentare riguros matematică a unor teme importante din teoria specificațiilor algebrice, aceasta incluzând și aspectul lor computațional, adică rescrierea algebrică de termeni. Acest din urmă aspect duce specificațiile algebrice pe tărâmul programării. Mai mult, acestea sunt extinse și către paradigma programării logice, prezentându-se, astfel, o abordare mai puțin convențională a programării logice ca prelungire a teoriei specificațiilor algebrice.
Cadrul algebric fundamental este cel clasic al algebrelor multi-sortate. În primul capitol sunt prezentate definițiile importante și sunt dezvoltate în cadrul multi-sortat rezultatele fundamentale din teoria algebrelor universale. Acestea includ conceptele de morfism de algebre, subalgebre, congruențe și algebre factor, algebre libere. Rezultatul principal al acestui capitol este cel legat de semantica algebrei inițiale în cadrul mai general al algebrelor libere pentru teorii Horn educaționale. Conceptele și rezultatele sunt ilustrate cu exemple concrete de specificații formale a unor studii de caz de informatică.
Capitolul doi este dedicat aspectelor computaționale ale specificațiilor prin algebre muti-sortate. Tema principală este rescrierea de termeni, introdusă ca sistem deductiv. Sunt tratate riguros matematic aspecte importante clasice din teoria rescrierilor de termeni cum ar fi: terminarea, confluența, rescrierea modulo teorii, rescrierea condiționată, perechi critice etc. Tot în acest capitol este discutat și algoritmul de unificare, cu toate că această secțiune ar aparține de fapt următorului capitol.
Următorul capitol abordează tema programării logice dintr-o perspectivă mai puțin convențională, și anume aceea a specificațiilor algebrice educaționale. Dar această abordare este cea care se încadrează în contextul general al logicii educaționale în care este scrisă cartea. În acest context paradigma programării logice este dezvoltată din nou riguros matematic pe două paliere: cel al semanticii denotaționale și cel al semanticii operaționale. Prima înseamnă teoremele lui Herbrand, iar a doua, tehnici de paramodulație și narrowing.
Capitolele patru și cinci reprezintă altceva decât primele trei capitole, deoarece se referă la tehnici de modularizare pentru specificații algebrice, și există un anumit grad de deconectare de primele trei capitole. Din punct de vedere matematic sunt introduse elementele necesare de teoria categoriilor și de teoria instituțiilor. Apoi se dezvoltă semantica binecunoscută a modularizării bazate pe instituții. Caracterul riguros matematic se menține și în aceste capitole.

Răzvan Diaconescu este cercetător științific 1 la Institutul de Matematică al Academiei Române.

 7,648 total views,  8 views today