Rachunek Lambda, Typy i Logika Intuicjonistyczna

Prowadzący: Radosław Rowicki

Zadania kwalifikacyjne
Kategorie: informatyka teoretyczna matematyka

[11.05.2020 – zmiany w zadaniu 3.2 oraz 4.3]

Rachunek Lambda

Wszyscy znamy słynną maszynę Turinga, a nawet jeśli nie, to na tych warsztatach zobaczymy coś dużo ciekawszego! Rachunek lambda to system formalny o identycznej mocy obliczeniowej co wspomniana maszyna, lecz realizujący swój cel w zupełnie innym paradygmacie. O ile maszyna Turinga definiuje obliczenia poprzez budowanie pewnego grafu stanów z pamięcią, to rachunek lambda przyjmuje podejście bardziej "funkcyjne" i skupia się na wykorzystywaniu pewnego abstraktu funkcji do definiowania wszystkiego co tylko się da.

Na warsztatach zapoznamy się ze wspomnianym systemem i nauczymy definiować obliczenia w nowym języku. Poznamy jego możliwości oraz ograniczenia, ale dowiemy się też jak sobie sprawnie z tymi ograniczeniami radzić poprzez wyrobienie pewnych wzorców.

Teoria Typów

Czym byłby javascript bez typów? ...wait, chyba zły przykład. 

Czym byłby dobry język programowania bez typów? O ile istnieją języki z tzw dynamicznymi typowaniami, to zazwyczaj większą wydajnością i odpornością na głupie błędy cieszą się jednak języki statycznie typowane*. Okazuje się niestety że nasz surowy rachunek lambda należy do tych pierwszych i pozwala robić bardzo złe rzeczy nie oferując przy tym żadnej kontroli nad tym czy dana zmienna jest liczbą, wartością logiczną czy listą (bo tych pojęć w zasadzie tam nie ma). W tym celu stworzono tzw simply typed lambda calculus – rachunek lambda poszerzony o system typów pozwalający zachować pewną względną kontrolę poprawności. Dowiemy się czym tak naprawdę są typy i formalnie zdefiniujemy reguły typowania wyrażeń naszego języka. Zobaczymy też jakie nakłada to na nas ograniczenia i jakie możliwości zamyka nam bezwzględna restrykcja typecheckera.

Po tym wszystkim dowiemy się jak sobie radzić z polimorfizmem – w tym celu wprowadzę dużo mocniejszy system F na którym zbudujemy sobie bardziej zaawansowane i uniwersalne mechanizmy obliczeniowe. W tym celu będziemy musieli się zapoznać z typami wyższych rzędów oraz typami wyższej rangi.

* dynamiczne typowanie – kontrola typów (można by rzec, dziedzin zmiennych) odbywa się ad hoc w trakcie działania programu, statycznie – check jest wykonywany raz a dobrze przed wykonaniem. Od wspomnianej reguły oczywiście są wyjątki.

Logika Intuicjonistyczna

No i na koniec – co ma do tego wszystkiego logika? Okazuje się że bardzo, bardzo dużo. W tej części poznamy izomorfizm Curry'eg-Howarda który traktuje o związku logiki z powyższymi zagadnieniami. Ponadto, nie będzie to zwykła logika – będzie to jej specjalne wydanie w której wszystko jest konstruktywne i która w naturalny sposób dopuszcza brak możliwości oceny prawdziwości pewnych zdań, a także zależność stanu naszej wiedzy od pewnego kontekstu. Definitywnie odrzuca ona prawo wyłączonego środka – tutaj nie jest prawdą że każde zdanie jest prawdziwe lub fałszywe. Prawo eliminacji podwójnej negacji również idzie do lamusa, a w związku z tym odrzuca się wszelkie dowody nie-wprost. Wartość zdania nie zależy już od (jak w logice klasycznej) od wartości składowych, lecz od fizycznej obecności dowodu na to zdanie. I takimi dowodami będziemy właśnie żonglować w naszym systemie!

 

Wymagania

Wiedza licealna, niekoniecznie informatyczna (ale zadania kwalifikacyjne mocno zachęcają do ogarnięcia podstaw programowania). To są warsztaty których tematyka stanowi most między matematyką a informatyką, więc wypada mieć jakieś podstawowe pojęcie w obu dziedzinach.

Wymagane cechy i umiejętności:

  1. Znajomość logiki klasycznej
  2. Znajomość podstaw teorii zbiorów
  3. Znajomość pojęcia funkcji
  4. Brak strachu przed funkcjami które przyjmują funkcje jako argumenty i zwracają funkcje które przyjmują funkcje które...

Nie trzeba umieć dodawać liczb.

 

Przydatne rzeczy

  • Zawsze możesz do mnie napisać, chętnie pomogę wyjaśnić wszelkie wątpliwości i trudności, w szczególności te związane z programowaniem
  • Jako prosty i łopatologiczny język programowania mogę polecić JavaScript, jest do niego pełno tutoriali w internecie. Jako punktowany język myślę że najwygodniej użyć OCamla lub Haskella. Przykładowy tutorial do pierwszego: https://learnxinyminutes.com/docs/ocaml/ i do drugiego: https://www.tryhaskell.org/ (ten jest interaktywny!). 
  • Podstawowe listy w wielu językach funkcyjnych to tak naprawdę stosy
  • Zmianę wartości zmiennej można zastąpić wrzuceniem jej do argumentu funkcji i wywoływanie się rekurencyjnie z nową wartością tej zmiennej. Przykład:
```
silnia_iter(const int x) {
  int result = 1;
  for(int i = 1; i <= x; i = i + 1) {
    result = result * i;
  }
  return result;
}
 
silnia_func(const int x) { return silnia_func_loop(x, 1, 1); }
silnia_func_loop(const int x, const int result, const int i) {
  if(i <= x) return silnia_func_loop(x, result * i, i + 1);
  else return result;
}
```