FUNKTSIONAALPROGRAMMEERIMISE ÕPIK

Kalmer Apinis, Varmo Vene

[Mustand, 9. 9. 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
  • Ülesanded
• λ-arvutus
  • Arvutusmudelid
  • Termid konstantidega λ-arvutuses
  • Makrodefinitsioonid
  • Ülesanded
• Reduktsioon
  • β-reduktsioon
  • α-ekvivalentsus
  • η-reduktsioon
  • Reduktsioonijärjekorrad
  • Ülesanded
• Listid ja muud andmestruktuurid
  • Abstraktsioonid Idrises
  • Paarid ja ühiktüüp
  • Naturaalarvud
  • Järjendid e. listid
  • Enumeratioonid
  • Listikomprehensioon
  • Ülesanded
• Kõrgemat järku funktsioonid
  • Funktsioon map
  • Funktsioon foldr
  • Funktsioon foldl
  • Funktsioon filter
  • rohkem funktsioone
  • Ülesanded
• Uued andmestruktuurid
  • Tüübifunktsioonid
  • Algebralised andmestruktuurid
  • Kirjed
  • Ülesanded
• Andmestruktuurid puhtas λ-arvutuses
  • Tõeväärtuste implementatsioon
  • Paaride implementatsioon
  • Naturaalarvud
  • Listid
  • Püsipunktid
  • Ülesanded
• Polümorfism ja liidesed
  • Alamtüüpimine
  • Parameetriline polümorfism
  • Ad-hoc polümorfism ehk liidesed
  • Monad liides
  • Ülesanded
• Sisend ja väljund
  • Ülesanded
• Parsimine
• Laiskus
• λ-termide efektiivne väärtustamine
  • Virtuaalmasin LVM
  • λ-termi tõlkimine LVM programmiks
  • Reduktsioon vs. virtuaalmasinad
  • Ülesanded
• Lihtsalt tüübitud λ-arvutus
  • Tüüpide algebra
  • Listid lihtsalt tüübitud λ-arvutuses
  • Tüüpide ja tüübisüsteemide omadused
  • Ülesanded
• Tüübituletus
  • Intuitiivne tüübituletus lihtsalt tüübitud λ-arvutuses
  • Formaalne tüübituletus lihtsalt tüübitud λ-arvutuses
• Tõestamine
  • Curry-Howard vastavus λ-arvutuses
  • Tõestamine Idrises
  • Tõestamine teistes programmeerimiskeeltes
  • Ülesanded
• Sõltuvate tüüpidega arvutamine Idrises
  • Ülesanded
• Kvantitatiivne tüübiteooria
  • Arv null
  • Arv üks
  • Teistes programmeerimiskeeltes/süsteemides

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