Serwisy internetowe Uniwersytetu Warszawskiego Nie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Rachunek lambda

Informacje ogólne

Kod przedmiotu: 1000-2M02RL Kod Erasmus / ISCED: 11.303 / (0612) Database and network design and administration
Nazwa przedmiotu: Rachunek lambda
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Przedmioty monograficzne dla III - V roku informatyki
Przedmioty obieralne dla informatyki
Punkty ECTS i inne: 6.00
zobacz reguły punktacji
Język prowadzenia: angielski
Rodzaj przedmiotu:

monograficzne

Założenia (lista przedmiotów):

Języki, automaty i obliczenia 1000-214bJAO

Skrócony opis:

Wprowadzenie do rachunku lambda jako abstrakcyjnyego modelu procesu obliczenia. Rachunek bez typów: wlasnosci redukcji, konstrukcja modeli, nierozstrzygalność. Rachunki z typami prostymi i polimorficznymi: normalizacja, siła wyrazu, związki z logiką.

Pełny opis:

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.

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.

Efekty uczenia się:

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.

Metody i 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ą.

Zajęcia w cyklu "Semestr letni 2021/22" (jeszcze nie rozpoczęty)

Okres: 2022-02-21 - 2022-06-15

Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Paweł Urzyczyn
Prowadzący grup: Paweł Urzyczyn
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.