Denotacijska semantika PCFKostelec, Kristjan (Avtor) Bauer, Andrej (Mentor) programski jezik PCFoperacijska semantikadenotacijska semantikadomenesubstitucijska lemaizrek o usklajenosti semantikeizrek o ustreznosti semantikeizrek o primernosti semantikeV diplomskem delu je v celoti predstavljen funkcijski programski jezik s tipi, imenovan PCF, skupaj z njegovimi pravili za preverjanje tipov, pravili za substitucijo ter operacijsko semantiko. Dokazan je izrek o varnosti. Pokazano je, da je rekurzija negibna točka. Predstavljene so domene, ki so motivirane preko poskusa vpeljave naivne semantike. Pokazano je, da ima vsaka zvezna funkcija najmanjšo negibno točko in predstavljene so nekatere zvezne funkcije med domenami. Definirana je funkcija, ki zvezni funkciji priredi njeno najmanjšo negibno točko. Vpeljana je denotacijska semantika PCF s pomočjo domen. Dokazana sta substitucijska lema ter izrek o usklajenosti, s pomočjo logičnih relacij pa je dokazan izrek o ustreznosti. Na koncu je zapisan izrek o primernosti kot posledica izreka o usklajenosti in izreka o ustreznosti.20202020-01-25 07:45:04Delo diplomskega seminarja/zaključno seminarsko delo/naloga113690UDK: 004.43VisID: 106296COBISS_ID: 18974041sl