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 :)

O ile nie zaznaczono inaczej, treść tej strony objęta jest licencją Creative Commons Attribution-ShareAlike 3.0 License