EXEMPLE

            Un program Elf presupune existenta mai multor fisiere cu extensia ".elf" ,care sunt apoi incarcate prin rularea unui fisier "load.sml". Exemple de intrebari se gasesc in fisierul "examples.quy".
            Am ales pentru rulare exemplul din "/elf-examples.tar/lists". Aici sunt implementate liste polimorfice,si anume cateva operatii pe liste. Avem trei fisiere ".elf" care sunt incarcate in fisierul "load.sml" si un fisier "examples.quy". Acesta din urma contine cateva exemple de intrebari. Declararea tipurilor se face in fisierul "elements.elf" si "lists.elf" iar operatiile asupra listelor sunt scrise sub forma unor predicate in fisierul "preds.elf".

         LISTE POLIMORFICE

-batch_top "examples.quy";
[reading queries from file examples.quy]
Using: preds.elf elements.elf
Solving for: member append map2 el bool eq
?- member X (cons a (cons b (cons a nil))).
            X = a.
            yes
?- append X Y (cons a (cons b (cons c (cons d nil)))).
            Y = cons a (cons b (cons c (cons d nil))),
            X = nil.
             yes
?- % this should fail.
?- map2 eq (cons a (cons b (cons c (cons d nil))))
?- (cons d (cons b (cons c (cons a nil)))).
            no
?- map2 eq (cons a (cons b (cons c (cons d nil))))
?- (cons a (cons b (cons c (cons d nil)))).
           solved
           yes

?- [closed query file examples.quy]
val it = () : unit
-
         Prin rularea fisierului "examples.quy" s-a facut matching intre fiecare intrebare si predicatele respective, realizandu-le astfel reconstructia tipurilor.
         In intrebarea "?- member X (cons a (cons b (cons a nil))). " , X este o variabila care ia la inceput valoare 'a' iar apoi,daca se repeta intrebarea va lua pe rand valorile 'b' si 'a'. In acest caz, X va contine pe rand toate elementele listei. Predicatul append realizeaza concatenarea a doua liste,iar intrebarea :"?- append X Y (cons a (cons b (cons c (cons d nil))))." descompune lista in doua subliste X si Y. Iar map2 aplica un operator logic asupra a doua liste. "map2 eq (cons a (cons b (cons c (cons d nil)))) (cons d (cons b (cons c (cons a nil))))." va esua din cauza ca cele doua liste nu sunt echivalente.
        Bineinteles se pot formula si alte intrebari pentru predicatele din "preds.elf". Acesta fiind doar un exemplu despre lucrul cu listele polimorfice.

EXPRESII LAMDA

        Un alt exemplu este "lam" care se gaseste in directorul "elf-examples". Acesta implementeaza calculul lamda si egalitatea termenilor. Se efectueaza reduceri alfa si beta. Cateva intrebari sunt :

?- eq _ (app (lam [x] x) s) (app (app (app (lam [f] (lam [x] (app f x)))
           (lam [x] lam [y] x)) s) z) .
            solved
            yes
        Intrebarea a reusit ceea ce inseamna ca cei doi termeni sunt echivalenti. Intr-adevar in urma reducerii beta cei doi termeni sunt identici. Aceasta ilustreaza pierderea informatiei cand nu sunt sintetizate toate argumentele implicite. Se foloseste reprezentarea interna.

?- sigma [Tr:eq _ (app (lam [x] x) s) (app (app (app (lam [f] (lam [x] (app f x)))(lam [x] lam [y] x)) s) z)] treq Tr P.
          p =

e_trans (e_trans e_eta  
     (e_lam [x:term nat] e_trans    (e_trans
           (e_sym (e_app e_refl (e_app e_refl (e_app e_refl e_beta))))
                 (e_trans (e_sym (e_app e_refl (e_app e_refl e_beta)))
                     (e_trans (e_sym (e_app e_refl (e_app e_refl e_beta)))
                         (e_trans (e_sym (e_app e_refl e_beta))
                            (e_app e_refl e_refl)))))
                            (e_app e_refl e_beta)))
(e_sym e_eta).
yes

Acesta a doua intrebare foloseste reprezentarea externa si ambigua a rezultatului intermediar.Ceea ce conduce la constrangeri.

?- treq (eq_arrow ([x:term nat] [tr':eq' x x] eq_whrl (eq_whrr (eq_whrr
       ?- (eq_whrr (eq_whrr (eq_base (eq'_app (eq_base tr') eq'_s)) (whr_left
          ?- whr_redex)) (whr_left (whr_left whr_redex)))
            ?- (whr_left (whr_left whr_redex))) (whr_left (whr_left (whr_left whr_redex))))
              ?- (whr_left whr_redex))) P. 

P =
    e_trans (e_trans e_eta (e_lam [x:term nat]
        e_trans (e_trans (e_sym (e_app e_refl (e_app e_refl (e_app e_refl e_beta))))
           (e_trans (e_sym (e_app e_refl (e_app e_refl e_beta)))
              (e_trans (e_sym (e_app e_refl (e_app e_refl e_beta)))
                 (e_trans (e_sym (e_app e_refl e_beta))
                    (e_app e_refl e_refl)))))
                    (e_app e_refl e_beta)))
(e_sym e_eta).

yes

?- eq _ s M.
        M = s.
        yes

?- sigma [Tr:eq _ s M] treq Tr P.
P =
        e_trans (e_trans e_eta (e_lam [x:term nat] e_app e_refl e_refl))
       (e_sym e_eta),
M = s.
yes

?- eq _ (app s (app s z)) M.
           M = app s (app s z).
           yes

?- sigma [Tr:eq _ (app s (app s z)) M] treq Tr P.
          P = e_app (e_app e_refl e_refl) e_refl,
         M = app s (app s z).
          yes

        Bineinteles se pot formula si alte intrebari pe langa acestea date ca exemplu. In acest scop am formulat alte intrebari pentru a verifica reducerea beta pentru expresiile lamda.

?- eq _ (app (app (lam [x] x) (lam [y] y) ) s) M.
        Solving...
        M = s.
         yes
?-sigma [Tr:eq _ (app (app (lam [x] x) (lam [y] y) ) s) M] treq Tr P.
        Solving
        P =
             e_trans
                 (e_trans e_eta
                    (e_lam [x:term nat]
                      e_trans (e_trans (e_app e_refl e_refl) (e_app e_refl e_beta))
                   (e_app e_refl (e_app e_refl e_beta))))
             (e_sym e_eta),
          M = s.
        yes
        Acesta intrebare sigma [x:A] B, este o intrebare speciala in limbajul Elf. Se executa mai intai A si se instantiaza x la un obiect de tip apropiat. Apoi este rezolvat B sub aceasta instantiere.