SINTAXA SI SEMANTICA

           Sintaxa in Elf este foarte simpla,din moment ce avem de modelat doar cativa constructori din LF. Deoarece LF este impartit pe mai multe nivele de tipuri,familii si obiecte, sintaxa este supraincarcata in acestea. Se va mentine aceasta supraincarcare in sintaxa concreta si se vor referi expresiile din cele 3 nivele colective ca fiind termeni.
           Limbajul Elf contine cinci categorii sintactice: termeni,semnaturi (S::= <> | S, c:K | S, c:A), contexe (G::= <> | G, x:A), familii de tipuri (A ::= c | A M | {x:A} B | S x:A.B ) si moduri (K ::= Tip | {x:A} K). Termenii au urmatoarea sintaxa:
                          sigentry ::= id : term.
                          query ::= term.

                          term ::= type % Type
                          | term1 -> term2 % A -> B
                          | term1 <- term2 % B -> A
                          | {id : term1} term2 % \Pi x:A. K or \Pi x:A. B
                          | [id : term1] term2 % \lambda x:A. B or \lambda x:A. M
                          | term1 term2 % A M or M N
                          | term : term % explicit cast
                          | _ % hole, to be filled by term reconstruction
                          | {id} term % same as {id:_} term
                          | [id] term % same as [id:_] term
   
           Toate caracterele pot fi incluse in interiorul idntificatorilor, care sunt separati prin spatii sau caractere speciale (%, : , . , () , [] , {}). In particular, A ->B este un identificator, pe cand A->B reprezinta si tipul functiei definite de la A la B. Un identificator cu litera mare este cel care incepe cu _ (underscore) sau cu o litera intre A si Z. Iar un identificator cu litera mica incepe cu orice caracter in afara de numere si caractere rezervate. Variabilele libere dintr-o semnatura trebuie sa fie cu litera mare, iar variabilele legate si constantele trebuie sa fie identificatori cu litera mare sau cu litera mica.           Identificatorii sigma, #pr#, ` (backquote) si #`# nu sunt tratati special din punct de vedere lexical, dar sunt predefiniti si nu se recomanda utilizarea lor in programe. Constantele au un scop static, ceea ce inseamna ca pot fi “umbrite” de secventele urmatoare de declaratii. Un identificator “umbrit” se scrie sub forma %id%.
          Exista cateva functii care sunt de mare folos pentru programarea in Elf. Cea mai importanta ,de fapt ceea care da informatii despre celelalte functii este help () --- tipareste un scurt mesaj de help.
          Reconstructia termenilor si tipurilor are la baza un algoritm de solutionare a constrangerilor. Include reconstructia tipurilor in mod normal si in plus reconstructia unor argumente implicite ale functiilor. Principiul de baza care trebuie retinut este dualitatea dintre cuantificatorii omisi si argumentele implicite.
         O semnatura constituie un program si cautarea este realizata prin incercarea fiecarei constante din semnatura cu scopul de a construe un obiect de tipul intrebarii. Prima unificare care este asemanatoare cu cea din Prolog este ineficienta. Subscopurile sunt rezolvate in ordinea in care apar si se face backtracking la cea mai recenta alegere ori de cate ori un scop esueaza. Deci cautarea unui obiect se realizeaza prin cautarea in adancime, la fel ca si in Prolog. In programarea in limbajul Elf este normal sa se imparta o semnatura in doua parti: una statica si una dinamica, situate in fisiere diferite. Fiecare fisier contine declaratii de familii si obiecte.
         Cateva aspecte distincte dintre scopurile si variabilele logice din Prolog. O formula in Prolog corespunde unui tip dinamic in Elf, un predicat unei familii dinamice. O variabila logica in Prolog este aici o variabila de tip static, fiind instantiate doar prin unificare nu si prin cautare.