|
Limbajul
ELF este folosit pentru formularea si verificarea meta-teoremelor despre
sistemele deductive. Poate verifica multe teoreme dincolo de scopul curent
al demonstrarii teoremelor. Mai mult, o parte semnificativa a verificarii
este indeplinita automat in timpul reconstructiei termenilor, type-checking
si shema-checking.
O aplicatie pentru
utilizarea acestui limbaj este implementarea metodelor de sortare (quicksort,
sortarea prin selectie, insertie) si interclasarea a doua liste polimorfice.
Deoarece limbajul
Elf folseste SML-ul (Standard ML of New Jersey) pentru a executa intrebarile
la un nivel inalt, exista trei fisiere "sortari.elf",
"declaratii.elf" si "liste.elf" care
trebuie incarcate intr-un fisier sml "load.sml". Fiecare
fisier ".elf" defineste o semnatura, asociata cu numele fisierului.
Exista de asemenea o semnatura globala, fisierul "declaratii.elf",
care contine declaratii pentru toate constantele. Aceasta semnatura globala
este folosita pentru reconstructia tipurilor. Aici s-a definit predicatul
"maimic " ,care arata relatia dintre constantele 1,2,3,4,5
(se aleg arbitrar) ::
el
: type.
maimic : el ->
el -> type.
maimic1
: maimic 1 2.
maimic2 : maimic
2 3.
maimic3 : maimic
1 3.
maimic4 : maimic
3 4.
maimic5 : maimic
1 4.
maimic6 : maimic
2 4.
maimic7 : maimic
1 5.
maimic8 : maimic
2 5.
maimic9 : maimic
3 5.
maimic10 : maimic
4 5.
maimiceg1 : maimic
1 1.
maimiceg2 : maimic
2 2.
maimiceg3 : maimic
3 3.
maimiceg4 : maimic
4 4.
maimiceg5 : maimic
5 5.
In
fisierul "liste.elf" sunt declarate listele
polimorfice iar in "sortari.elf" sunt efectuate cateva
operatii asupra listelor si anume sortarea unei liste (in mai multe moduri
) si interclasarea a doua liste.
Exista mai multe
moduri de sortare a unei liste : sortarea pin selectie ,prin insertie
si quicksort. Prima sortare, cea prin selectie presupune folosirea unui
predicat de aflare a minimului dintr-o lista - minim. Este nevoie
si de un predicat de stergere a elementului din lista ( sterg:
elem -> lista -> lista). Aceasta sortare consta in gasirea minimului
, adaugarea lui intr-o noua lista, si stergerea din lista de sortat.
Sortarea prin insertie presupune inserarea,
pe rand, a fiecarui element al listei , intr-o lista ordonata crescator.
Elementele se insereaza pe pozitia corespunzatoare astfel incat lista
sa ramana ordonata. Este folosit si aici un predicat insert, pentru
inserarea unui element in lista.
Al treilea tip de sortare este
mai rapid, dupa cum ii este si numele. Predicatul quicksort se
refera la descompunerea listei in doua subliste si apoi apelarea recursiva
a predicatului pe cele doua subliste pana la lista vida. Pentru impartirea
listei in doua s-a folosit predicatul partitionare. Astfel lista
este partitionata in doua subliste in functie de un element dat. Una contine
elementele mai mici decat el, iar cealalta lista elementele mai mari.
Pe langa predicatele
de sortare mai exista un predicat de interclasare a doua liste. Astfel
doua liste ordonate sunt interclasate intr-una singura , lista rezultat
fiind de asemenea ordonata crescator.
Cateva intrebari pentru
verificarea predicatelor: minim, sterg ,sort_sel, insert, sort_ins, quicksort
si interclasare se gasesc in fisierul "exemple.quy".
Prin aceste intrebari se face matchingul cu predicatele corespunzatoare
si se realizeaza reconstructia tipurilor. Se vor explica in cele ce urmeaza
o serie de intrebari si rezulatele lor. Daca se doreste aflarea minimului
dintr-o lista polimorfica, atunci se pune intrebarea:
?- minim maimic (cons 3 (cons 1 (cons 4 (cons 2 (cons
5 nil))))) X.
Solving...
X = 1.
Maimic
este un predicat care testeaza relatia dintre doua elemente a unei liste.
Si anume daca intre doua constante exista o relatie de "mai mic sau
egal". El face parte din semnatura globala a programului.
Stergerea unui element
dintr-o lista, care are ca rezultat tot o lista , se face prin intrebarea:
?- sterg 3 (cons 2 (cons 3 (cons 5 nil))) X.
Solving...
X = cons 2 (cons 5 nil).
yes
?- sort_sel maimic (cons 5 (cons 3 (cons 1 (cons 4 (cons 2 nil)))))
X.
Solving...
X = cons 1 (cons 2 (cons 3 (cons 4 (cons 5 nil)))).
yes
?- sort_sel maimic (cons 3 (cons 5 (cons 1 (cons 2 (cons 3 nil)))))
X.
Solving...
X = cons 1 (cons 2 (cons 3 (cons 3 (cons 5 nil)))).
Intrebarile
de mai sus realizeaza sortarea listei data ca intrare. S-a tinut cont
si de faptul ca pot exista mai multe elemente cu aceeasi valoare.
De asemenea testarea
predicatului insert, se face prin intrebarea urmatoare unde variabilei
X i se va atribui lista formata prin inserarea unui element (in acest
caz elementul 3).
?- insert maimic 3 (cons 2 (cons 4 (cons 5 nil))) X.
Solving...
X = cons 2 (cons 3 (cons 4 (cons 5 nil))).
yes
Predicatul
sort_ins consta in descompunerea listei de sortat si inserarea , pe rand,
a elementelor la locul potrivit intr-o noua lista. Lista rezultat se pastreaza
in variabila X.
?- sort_ins maimic (cons 4 (cons 2 (cons 1 (cons 5
(cons 3 nil))))) X.
Solving...
X = cons 1 (cons 2 (cons 3 (cons 4 (cons 5 nil)))).
yes
Prin
partitionare lista de sortat se descompune in doua liste X1 si X2.
?- partitionare maimic (cons 2 (cons 5 (cons 1 (cons
4 nil)))) 3 X1 X2.
Solving...
X2 = cons 5 (cons 4 nil),
X1 = cons 2 (cons 1 nil).
yes
Sortarea rapida (quicksort):
?- quicksort maimic (cons 1
(cons 5 (cons 3 (cons 4 nil)))) X.
Solving...
X = cons 1 (cons 3 (cons 4 (cons 5 nil))).
yes
Doua liste
ordonate si interclaseaza, adica se formeaza o a treia lista cu elementele
celor doua in ordine crescatoare.
?- interclasare maimic (cons 2 (cons 4 nil)) (cons
1 (cons 3 (cons 5 nil))) X.
Solving...
X = cons 1 (cons 2 (cons 3 (cons 4 (cons 5 nil)))).
GC #1.2.5.11.226.9098: (0 ms)
yes
Pentru
rularea acestui exemplu, dupa ce s-a incarcat limbajul Elf si dupa ce
s-a setat calea corespunzatoare se executa urmatorii pasi:
-
use "load.sml";
-
load ();
-
top ();
?-
... intrebari ...
?-
^D % Control-D pentru a reveni la SML
Fisierul ce contine exemplele
se executa astfel:
-
batch_top "exemple.quy";
Este foarte important
faptul ca aceste intrebari nu sunt unice ci se pot formula si altele.
Predicatele descrise in "sortari.elf" se pot folosi pentru crearea
unora noi in functie de cerinte. Limbajul ELF permite si implementarea
unor algoritmi de demonstrare a teoremelor, deductia tipurilor , de evaluare
a demonstratie etc, avand o aplicabilitate foarte mare.
SURSELE :
liste.elf, declaratii.elf,
sortari.elf, exemple.quy,
load.sml
|