Rachunek lambda 1000-2M02RL
1. Składnia rachunku bez typów. Alfa-konwersja.
2. Własności beta- i eta-redukcji. Siła obliczeniowa.
3. Semantyka denotacyjna dla rachunku bez typów.
4. Rozwiązalność i drzewa Boehma.
5. Rachunek z typami prostymi. Silna normalizacja.
6. Semantyka typów prostych.
7. Formuły-typy (izomorfizm Curry'ego-Howarda).
8. Logika kombinatoryczna.
9. Typy iloczynowe.
10. Polimorficzny rachunek lambda (system F).
11. Problemy decyzyjne dla rachunków z typami.
Rodzaj przedmiotu
Założenia (lista przedmiotów)
Koordynatorzy przedmiotu
Efekty kształcenia
Wiedza:
* Zna język rachunku lambda i logiki kombinatorycznej.
* Zna metody semantyki operacyjnej (redukcja, drzewa
Bohma) i denotacyjnej (modele Scotta) dla rachunku bez typów.
* Zna siłę wyrazu rachunków lambda z typami i bez typów oraz
ich związek z konstruktywną logiką.
* Zna różne rodzaje polimorfizmu (system F, typy iloczynowe).
Umiejętności:
* Potrafi wyrażać algorytmy (definiować funkcje) w języku rachunku lambda
i badać ich własności.
* Potrafi analizować wyrażenia ze względu na ich typowalność.
Kompetencje:
* Rozumie związki pomiędzy zjawiskami obliczeniowymi i logicznymi.
* Rozumie teoretyczne podstawy semantyki i programowania funkcyjnego.
* Rozumie zjawisko polimorfizmu.
Kryteria oceniania
Aby zaliczyć przedmiot należy zaliczyć ćwiczenia i zdać egzamin.
Ocena końcowa będzie wystawiona na podstawie egzaminu.
Aby zaliczyć ćwiczenia należy koniecznie zaliczyć prace domowe. O zaliczeniu ćwiczeń decyduje prowadzący ćwiczenia.
Do egzaminu zerowego mogą przystąpić osoby, które zaliczyły prace domowe i zgłosiły gotowość do egzaminu najpóźniej 7 stycznia.
W przypadku zaliczania przedmiotu przez doktoranta, dodatkowym kryterium zaliczenia jest przeczytanie aktalnego artykułu naukowego i omówienie go z wykładowcą.
Literatura
1. www.mimuw.edu.pl/~urzy/Lambda/rlambda.ps
2. Barendregt, H. Lambda Calculus, Elsevier, 1984.
3. Girard, J.-Y. Proofs and Types, Cambridge UP, 1989.
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami:
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: