FUNKTSIONAALPROGRAMMEERIMISE ÕPIK

Kalmer Apinis, Varmo Vene

[Mustand, 17. 2. 2026]

• Eessõna
• Motivatsioon
  • Modulaarsus
  • Tõestamine
• Keel Idris
  • Definitsioonid, tüübid ja baasväärtused
  • Tüübid
  • Matemaatilised funktsioonid ja funktsioonitüüp
  • Funktsioonikutsed Idrises
  • Funktsiooni defineerimine Idrises
  • Prefix ja infix operaatorid
  • Taanded, blokid ja abifunktsioonid
• λ-arvutus
  • Arvutusmudelid
  • Termid konstantidega λ-arvutuses
  • Makrodefinitsioonid
• Reduktsioon
  • β-reduktsioon
  • α-ekvivalentsus
  • η-reduktsioon
  • Reduktsioonijärjekorrad
• Listid ja muud andmestruktuurid
  • Abstraktsioonid Idrises
  • Paarid ja ühiktüüp
  • Naturaalarvud
  • Järjendid e. listid
  • Enumeratioonid
  • Listikomprehensioon
• Kõrgemat järku funktsioonid
  • Funktsioon map
  • Funktsioon foldr
  • Funktsioon foldl
  • Funktsioon filter
  • rohkem funktsioone
• Uued andmestruktuurid
  • Tüübifunktsioonid
  • Algebralised andmestruktuurid
  • Kirjed
• Andmestruktuurid puhtas λ-arvutuses
  • Tõeväärtuste implementatsioon
  • Paaride implementatsioon
  • Naturaalarvud
  • Listid
  • Püsipunktid
• Polümorfism ja liidesed
  • Alamtüüpimine
  • Parameetriline polümorfism
  • Ad-hoc polümorfism ehk liidesed
  • Monad liides
• Sisend ja väljund
• Laiskus
• λ-termide efektiivne väärtustamine
  • Virtuaalmasin LVM
  • λ-termi tõlkimine LVM programmiks
  • Reduktsioon vs. virtuaalmasinad
• Lihtsalt tüübitud λ-arvutus
  • Tüüpide algebra
  • Listid lihtsalt tüübitud λ-arvutuses
  • Tüüpide ja tüübisüsteemide omadused
• Tüübituletus
  • Intuitiivne tüübituletus lihtsalt tüübitud λ-arvutuses
  • Formaalne tüübituletus lihtsalt tüübitud λ-arvutuses
• Curry-Howard vastavus λ-arvutuses
• Tõestamine Idrises
• Sõltuvate tüüpidega arvutamine Idrises
• Kvantitatiivne tüübiteooria
  • Arv null
  • Arv üks
  • Teistes programmeerimiskeeltes/süsteemides

This document was translated from L^AT_EX by H^EV^EA.