Rachunek lambda

Prowadzący

Paweł Marczewski

Opis

the snow falls slowly

the lambdas are lifting -

weak head normal form.

^źródło

Rachunek lambda

• to bardzo prosty system formalny - taki, w którym "wszystko jest funkcją", a jedyną operacją jest podstawienie wartości pod zmienną.
• to model obliczeń, równoważny maszynie Turinga - ale ładniejszy i do pewnych celów znacznie przydatniejszy. Rachunek lambda to w pewnym sensie najprostszy język programowania.
• to "druga strona" rachunku kombinatorów - każdy $\lambda$-term da się przekształcić w wyrażenie w rachunku kombinatorów, i odwrotnie.
• to, w zaskakujący sposób, "druga strona" logiki - istnieje odpowiedniość między lambda-termami i dowodami (izomorfizm Curry'ego-Howarda).

Zapraszam matematyków i informatyków.

Program zajęć

Pojawi się pewnie część z poniższych tematów:

• Podstawy formalizmu, własności beta-redukcji
• Różne konstrukcje - liczby, pary, działania, związek z innymi modelami obliczeń
• Kombinator Y i rekursja
• Postać normalna i drzewa Boehma
• Związek z rachunkiem kombinatorów
• Typy, związek z logiką

Wymagania

Poziom trudności: średni
Trzeba umieć: chyba nic… Podstawy matematyki. Indukcja i takie tam.
Można umieć (tzn. ma związek z tematem): rachunek kombinatorów, programowanie funkcyjne

Zadania kwalifikacyjne

Plik PDF z zadaniami kwalifikacyjnymi. (drugi adres) Może się zmienić, jeśli zauważę (lub ktoś inny zauważy) jakieś błędy.

Rozwiązania wysyłajcie na moc.liamg|celopmuh#moc.liamg|celopmuh, lub poprzez warsztatową aplikację.

Zadania mają tylko trochę wspólnego z tematyką warsztatów :)