Slajdy do wykładów 1-2.
Slajdy do wykładu 3.
Slajdy do wykładu 4.
Zadania do wykładu 1.

Reprezentacja termów

  1. Zdefiniuj typ do reprezentacji termów rachunku lambda używając napisów jako nazw zmiennych.
  2. Napisz funkcję generującą "świeże" nazwy zmiennych.
  3. Zdefiniuj drugą reprezentację, używającą indeksów de Bruijna zamiast napisów jako zmiennych.
  4. Napisz funkcje konwersji z jednej reprezentacji do drugiej.
  5. Napisz funkcję wykonującą podstawienie termu pod zmienną w danym termie.
  6. Napisz funkcję konwertującą reprezentację termów do czytelnego dla użytkownika zapisu.

Redukcja i normalizacja

  1. Napisz funkcję wykonującą jeden krok β-redukcji stosując strategię lewostronną.
  2. Napisz funkcję sprowadzającą term do postaci normalnej przez iterowanie wywołania funkcji z poprzedniego punktu.
  3. Napisz funkcję sprawdzającą, czy dany term jest w postaci normalnej.
  4. Wykonaj punkty 6-8 dla (kanonicznej) czołowej postaci normalnej i słabej czołowej postaci normalnej.
  5. Znajdź term, który ma czołową postać normalną, ale nie ma postaci normalnej, oraz taki, który ma słabą czołową postać normalną, ale nie ma czołowej postaci normalnej. Przetestuj na nich zdefiniowane funkcje normalizujące.
  6. Jakiej strategii redukcji (ewaluacji) używa Ocaml? Napisz funkcję normalizującą termy według tej strategii.
Zadania do wykładu 2.

Rozgrzewka [Wprowadzenie do Scheme'a]

Napisz funkcję przechodzącą drzewa binarne w głąb (i drukującą etykiety), używając schematu reprezentacji z wykładu. Do reprezentacji etykiet użyj stałych liczbowych Scheme'a. Zdefiniuj operator stałopunktowy Y z modyfikacją, która pozwala na używanie go w języku z aplikatywną ewaluacją.

Ewaluator wyrażeń arytmetycznych

Napisz ewaluator wyrażeń arytmetycznych zbudowanych z liczb całkowitych i binarnych operacji +,*,-.
Jedną z wielu możliwych reprezentacji wyrażeń jako danych dla ewaluatora jest reprezentacja używana w samym Scheme'ie, tj. prefiksowa. Np. (+ (- 3 4) (* 1 2)) jest poprawnym wyrażeniem Scheme'a, które ma wartość 1: 
 
> (+ (- 3 4) (* 1 2))
1
Korzystając z mechanizmu cytowania, takie wyrażenie możemy reprezentować jako listę, poprzedzając je słowem quote lub, równoważnie, znakiem apostrofu ': 
 
> '(+ (- 3 4) (* 1 2))
(+ (- 3 4) (* 1 2))
Naszym celem jest napisanie funkcji eval, która obliczy wartość wyrażenia, którego reprezentacja jest zadana jako argument: 
 
> (eval '(+ (- 3 4) (* 1 2)))
1
Należy zdefiniować odpowiednie akcesory badające strukturę wyrażenia, korzystając z predefiniowanych predykatów number?, pair?, eq? do rozpoznawania, oraz operacji car i cdr do wybierania elementów listy.

Autoewaluator

Napisz autoewaluator lambda rachunku według definicji podanej na wykładzie, rozszerzając język o wartości obserwowalne, np. stałe liczbowe i operacje na nich.
Użyj reprezentacji HOAS i skorzystaj z faktu, że wyrażenia i wartości mogą być reprezentowane w ten sam sposób: abstrakcja ma być reprezentowana jako abstrakcja Scheme'a, a aplikacja jako cytowana lista. 
 
> (E (lambda (x) x))
#<procedure>
> ((E (lambda (x) (list 'suc x))) 5)
6
Co trzeba zmienić w ewaluatorze, gdybyśmy chcieli reprezentować termy jako listy etykietowane? Np.: 
(lambda (x) x) -> (list 'lam (lambda (x) x))
(suc 2) -> (list 'app 'suc 2)
Zadania do wykładu 3.

Autoewaluator, c.d. [Scheme]

  1. Zmień strategię ewaluatora z poprzedniego zadania na strategię CBN.
  2. Rozszerz ewaluator CBV tak, by mógł ewaluować sam siebie.

Ewaluator [Ocaml/Haskell]

Napisz autoewaluator lambda rachunku w swoim ulubionym języku typowanym.

Maszyna SECD [Ocaml/Haskell/Scheme]

  1. Zaimplementuj maszynę SECD. Rozszerz język definiowany o wartości obserwowalne.
  2. Zmodyfikuj maszynę tak, by wykonywała strategię CBN.
Zadania do wykładu 4.

Ewaluator, c.d. [Ocaml/Haskell]

Napisz ewaluator mini-języka funkcyjnego ze strategią aplikatywną (CBV), rozszerzającego rachunek lambda o reprezentacje liczb całkowitych, operacje dodawania, mnożenia i odejmowania, konstrukcję warunkową case (zamiast wartości logicznych, do rozgałęziania użyj własności "jest zerem"/"nie jest zerem"), oraz o definicje funkcji rekurencyjnych (jak na wykładzie).
  1. Użyj składni HOAS.
  2. Wartościami w tym języku są liczby całkowite oraz funkcje. Jak można reprezentować te wartości w ewaluatorze?
  3. Zmodyfikuj ewaluator tak, by strategia języka definiowanego była lewostronna zewnętrzna (CBN). Jak należy zmodyfikować typ wartości w Twojej reprezentacji w tym przypadku?
Zdefiniuj w języku definiowanym funkcję obliczającą silnię i przetestuj na niej ewaluator.

Maszyna abstrakcyjna [Ocaml/Haskell/Scheme]

Zaimplementuj maszynę abstrakcyjną ze środowiskiem dla języka z poprzedniego zadania.
Możesz zacząć od zaimplementowania odpowiedniej semantyki redukcyjnej, i przekształcenia funkcji ewaluującej na funkcję przejścia maszyny przez odpowiednie przekształcenia programu.
20. grudnia 2007