Uniwersytet Warszawski - Centralny System Uwierzytelniania
Strona główna

Rachunek lambda

Informacje ogólne

Kod przedmiotu: 1000-2M02RL
Kod Erasmus / ISCED: 11.303 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration Kod ISCED - Międzynarodowa Standardowa Klasyfikacja Kształcenia (International Standard Classification of Education) została opracowana przez UNESCO.
Nazwa przedmiotu: Rachunek lambda
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Przedmioty 4EU+ (z oferty jednostek dydaktycznych)
Przedmioty obieralne dla informatyki
Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka
Punkty ECTS i inne: 6.00 Podstawowe informacje o zasadach przyporządkowania punktów ECTS:
  • roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS;
  • tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h;
  • 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się;
  • tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS;
  • nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta.
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 zimowy 2023/24" (w trakcie)

Okres: 2023-10-01 - 2024-01-28
Wybrany podział planu:
Przejdź do planu
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
Przedmiot dedykowany programowi:

4EU+KURSY
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.
Krakowskie Przedmieście 26/28
00-927 Warszawa tel: +48 22 55 20 000 https://uw.edu.pl/ kontakt deklaracja dostępności USOSweb 7.0.0.0-4 (2023-10-17)