Cilj predmeta je nadgraditi osnovno poznavanje in razumevanje pojmov matematične analize in linearne algebre z zahtevnejšimi pojmi, prikazati njihovo uporabo pri matematičnem modeliranju pojavov v računalništvu in drugih znanostih in osnovne metode za računanje dobljenih modelov.
Za opravljen predmet mora študent rešiti tri samostojne domače naloge (ena DN ob koncu vsakega izmed naslednjih mesecev: marec, april, maj), en skupinski projekt (v maju) in uspešno opraviti teoretični izpit v enem od razpisanih izpitnih rokih.
- nosilec: Polona Oblak
- nosilec: Žiga Virk
- nosilec: Aljaž Zalar
Pri predmetu spoznamo koncepte in principe, na katerih slonijo moderni programski jeziki. Poudarek je na razumevanju s stališča programerja, čeprav se posvetimo tudi teoretičnim osnovam, na katerih sloni načrtovanje programskih jezikov.
1. Uvod in artimetični izrazi
- o programskih jezikih na splošno
- anatomija programskega jezika
- prvi primer: aritmetični izrazi s spremenljivkami
2. Ukazni programski jezik
- spremenljivke in aritmetika
- boolove vrednosti
- osnovne kontrolne strukture (zanke in pogojni stavek)
- operacijska semantika ukaznega jezika
- denotacijska semantika
- ekvivalenca programov
3. Dokazovanje pravilnosti programov
- dokazovanje pravilnosti za ukazni jezik (Hoare-style)
- pravilnost programa glede na dano specifikacijo
- Delna pravilnost `{P} c {Q}` in popolna pravilnost `[P] c [Q]`
- Pravila za dokazovanje: splošna pravila, invarianta zanke, dokazovanje popolne pravilnosti
4. Lambda račun
- zapis funkcij s funkcijskim predpisom:
- vezane in proste spremenljivke
- računsko pravilo (β-redukcija) za funkcijski predpis
- λ-račun brez tipov
- evaluacijske strategije (neučakana, lena)
- konfluentnost λ-računa
- primeri programov v λ-računu
5. Deklarativno programiranje in algebrajski tipi
- deklarativno programiranje
- algebrajski tipi:
- konstruktorji in destruktorji
- primeri deklarativnih jezikov: Haskell, ML, Racket
6. Rekurzivni tipi in rekurzija
- rekurzivni tipi, primeri
- rekurzivne definicije
- rekurzija kot negibna točka
- leno in neučakano računanje
- induktivni tipi – strukturna indukcija
- koinduktivni tipi
7. Polimorfizem in izpeljava tipov
- polimorfni tipi
- parametrični polimorfizem, najsplošnejši tip
- ad-hoc polimorfizem
- generično programiranje
- izpeljava tipov
8. Abstrakcija
- specifikacija/vmesnik in implementacija/modul
- abstrakcija implementacije, abstraktni tipi
- funktorji: preslikave iz implementacije v implementacijo
- primeri v OCaml, Javi in Haskellu
9. Logično programiranje
- pravila sklepanja kot program
- izvajanje programa je iskanje dokaza
- kako deluje prolog, zruževanje in meta-spremenljivke
- programiranje z omejitvami
10. Zapisi in objekti
- zapisi in tipi zapisov
- strukturni podtipi
- objekti kot rekurzivni zapisi
- objekti kot "encapsulated state" in metode kot "message passing"
- razredi
- nosilec: Andrej Bauer
- nosilec: Matija Pretnar
Cilj predmeta Računalniške tehnologije je študentom računalništva in informatike predstaviti fizikalne in tehnološke temelje delovanja in izdelave računalnikov, kvantitativno obravnavo nekaterih relevantnih primerov s področja fizike trdne snovi in predstavitev uporabe fizikalnih zakonitosti v tehniki izdelave mikroelektronskih, monolitnih vezij, temeljnih gradnikov računalnikov. Eden od ciljev predmeta je tudi predstavitev osnov kvantne mehanike, ki že sama po sebi postaja v računalništvu vse pomembnejša fizikalne teorija.
Izvedba predmeta: predavanja in dodatno branje doma, dva kolokvija (ali pisni izpit) in seminarska naloga, ustni izpit. Na voljo je skripta, zbirka vaj in zbirka izpitni vprašanj.
Potrebna predznanja: osnove klasične fizike, osnove linearne algebre in infinitezimalnega računa.
Course practicalities: Lectures and individual reading. Two colloquia (or a written exam), seminar work, oral exam. Lecture notes, exercise book and a list of examination questions are available.
Prerequisites: elementary classical physics, basic linear algebra and calculus.
- nosilec: Rok Žitko