Opis:
Podczas wykładu chciałbym przedstawić rachunek lambda i jego rozwoj.
Wykład powinien być elementarny, choć będzie wykorzystywać język
matematyczny, ktory powinien być znany z wykładu logiki dla informatykow.
Jego celem jest pokazanie, w jaki sposob kształtowały się pojęcia,
ktore dzisiaj są wykorzystywane w rożnych językach programowania (np. w Haskelu),
a także ich precyzyjne określenie i zdefiniowanie. Wykład zostanie uzupełniony
o uwagi historyczne i teoretyczne. Są łatwo dostępne i godne polecenia teksty
ułatwiające opanowanie proponowanego wykładu, na przykład niżej wspomniany
Introduction to Lambda Calculus.
Program:
# Rachunek lambda -- motywacje, trochę historii.
#Formalna definicja rachunku lambda, relacje redukcji.
#Formalizacja pojęcia obliczalności za pomocą rachunku lambda,
teza (Turinga)-Churcha, moc rachunku lambda.
#Własności relacji redukcji, twierdzenie Churcha - Rossera.
#Rachunek lambda z typami. #Rozstrzygalność prostego systemu typow.
Twierdzenie o silnej normalizacji.
#Związki rachunku lambda z logiką.
#Elementy semantyki.
#Paradoks Kleene'ego-Rossera, modele dla rachunku lambda.
Bibliografia:
# H.P. Barendregt, The type free lambda calculus,
in J. Barwise, Handbook of Mathematic Logic.
# H.P. Barendregt, E. Barendsen, Introduction to Lambda Calculus
# H.P. Barendregt, {\sl Lambda calculi with types}, in: S. Abramsky,
D.M. Gabbay and T.S.E. Maibaum (eds.),
Handbook of Logic in Computer Science, (1992).
# A. Church, An unsolvable problem of elementary number theory,
American Journal of Mathematics 58, (1936).
# A. Church, A formulation of the simple theory of types,
Journal of Symbolic Logic 5, (1940).
# R. Loader, Notes on Simply Typed Lambda Calculus, (1998).
# John C. Reynolds, Theories of Programming Languages.
sem. letni 2023/24: piątki, godz. 12.30-13.30, pokój 311, a także konsultacje zdalne za pośrednictwem MSTeams, w piątki, godz. 19.15 - 19.30 i dłużej, jeżeli będą zainteresowani.
Zapraszam też na konsultacje zdalne lub w Instytucie w terminach uzgodnionych ze stosownym wyprzedzeniem np. pocztą elektroniczną.
