INTRODUCERE

           Sistemele deductive formale au devenit importante in stiinta calculatoarelor. Ele sunt folosite pentru a specifica semantici logice si operationale,tipul sistemelor si alte aspecte ale limbajelor.
           LF (Lucrul cu Frame-uri) a fost realizat cu scopul obtinerii unui limbaj pentru specificarea la nivel inalt a sistemelor deductive. In LF, deciziile sunt reprezentate ca si tipuri si deductiile ca obiecte. In timp ce in LF tipul teoriei este determinabil, deductiile sustinute pot fi automat verificate . Oricum, LF este o puternica baza pentru probleme mult mai cuprinzatoare decat orice verificare a corectitudinii. O gama larga de sisteme deductive sunt specificate in LF si implementate in ELF. In continuare se va prezenta utilitatea folisirii limbajului ELF in implementarea meta-toeriei sistemelor deductive.
          Cateva cercetari in acest domeniu au fost realizate de catre Frank Plenning, Profesor la departamentul Stiinta Calculatoarelor, la Universitatea Carnegie Mellon, Pittsburgh, PA 15213-3891,USA.

 

LIMBAJUL ELF

          ELF-ul este un meta -limbaj pentru formalizarea teoriei limbajelor de programare si a logicii. Este utilizat pentru:
               - specificarea sintaxei abstracte si semanticii unui limbaj obiectual intr-un mod natural si direct;
               - implementarea algoritmilor relativi (de ex: deductia tipurilor, evaluarea sau cautarea demonstratiei);
               - reprezentarea demonstrarii meta-teoremelor despre un limbaj obiectual,semantica si implementarea lui.
          Blocul de baza in realizarea unui program Elf este semnatura, care este o secventa de declaratii ale constantelor. Cateva din aceste constante sunt pentru declararea constructorilor sau a predicatelor, altele pentru deductia regulilor sau a clauzelor.           Folosind modulul sistem Elf se poate distinge explicit rolul diferit al declaratiilor. La baza limbajului Elf sta unificarea dintre definirea logica (intalnita in LF) cu programarea logica (intalnita in Lamda -Prolog), fiind un limbaj folosit pentru demonstrarea teoremelor si pentru manipularea demonstratiilor. Cautarea demonstratiei (" proof search") este modelata in LF prin cautarea unui obiect de un tip dat. Astfel un tip joaca rolul unei intrebari in Prolog si poate contine mai multe variabile libere. Interpretorul ELF trebuie sa realizeze reconstructia tipului din programe si probleme inainte sa le execute.
          Chiar daca Elf-ul nu compileaza programe sau intrebari, el aplica cateva optimizari standard cunoscute din interpretoarele programarii logice si cateva care sunt specifice Elf-ului. Dintre optimizarile generale amintim : indexarea clauzelor, eliminarea unor verificari care nu sunt necesare si folosirea unui tabel global de simboluri mult mai efficient. Iar dintre optimizarile specifice fac parte eliminarea unificarilor redundante si a demonstratii unor obiecte care nu sunt necesare.