Zadanie 1 (10p) Zaimplementuj funkcję
normalizującą (do postaci β-normalnej) lambda
termy (w reprezentacji z nazwami zmiennych) przy
strategii redukcji w porządku normalnym. W tym celu
zdefiniuj najpierw strategię redukcji w porządku
normalnym za pomocą systemu reguł w stylu "dużych
kroków". Całkiem możliwe, że przyda Ci się
zdefiniowana na wykładzie relacja redukcji do słabej
czołowej postaci normalnej ⇓n.
Upewnij się, że Twoja implementacja operacji
podstawienia jest poprawna.
|
Zadanie 2 (5p) Zaimplementuj ewaluator lambda
termów w reprezentacji z indeksami de Bruijna do
słabej czołowej postaci normalnej w oparciu o
definicję relacji ⇒n z wykładu.
|
Zadanie 3 (5p) Zaimplementuj dwie funkcje, z
których jedna będzie tłumaczyła lambda termy w
reprezentacji z nazwami zmiennych na lambda termy w
reprezentacji z indeksami de Bruijna, a druga
odwrotnie.
|
Zadanie 4 (10p)
Rozważmy omawiany na wykładzie język funkcyjny o następujacej składni abstrakcyjnej:
t ::= x | λx.t | t t | 0 | suc t | case t of 0 => t || suc x => t | fix x.t
-
Zadaj semantykę dużych kroków przy ewaluacji
gorliwej dla tego języka, a następnie
zaimplementuj ją w postaci interpretera używjącego
operacji podstawienia.
-
Napisz interpreter powyższego języka, w którym
poszczególne wyrażenia języka będą interpretowane
przez odpowiadające im wyrażenia metajęzyka, w
którym implementujesz interpreter. Tak więc, na
przykład wyrażenie λx.t powinno być
interpretowane przez odpowiednią funkcję Twojego
metajęzyka, a wyrażenie t1
t2 przez aplikację interpretacji
t1 do interpretacji t2 (w
ten sposób to metajęzyk jest odpowiedzialny za
podstawienie). Wartości zwracane przez interpreter
powinny być postaci (używając składni Ocamla):
type value = Nat of int | Fun of value -> value
Zamiast podstawienia wykorzystaj środowisko czyli
funkcję typu var -> value, wiążącą zmienne z ich
wartością. Interpreter powinien mieć typ:
term -> (var -> value) -> value
W celu zinterpretowania wyrażenia fix x.t posłuż
się rekursją dostępną w metajęzyku.
|
|