Opis:
Podczas wykładu chciałbym przedstawić rachunek lambda i jego rozwój.
Wykład powinien być elementarny, choć będzie wykorzystywać język
matematyczny, który powinien być znany z wykładu logiki dla informatyków.
Jego celem jest pokazanie, w jaki sposób kształtowały się pojęcia,
które dzisiaj są wykorzystywane w róż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 typów.
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, The Lambda Calculus. Its Syntax and Semantics. Elsevier
# 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.
