20.500.12556/RUL-113690 Denotacijska semantika PCF delo diplomskega seminarja Denotational Semantics of PCF V 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. A typed functional programming language, called PCF, is presented in this thesis together with its type checking rules, substitution rules and its operational semantics. The safety theorem is proven. It is shown that recursion is a fixed point. Domains, which are motivated by an attempt of implementing naive semantics, are presented. It is shown that every continuous function has the least fixed point and some of the continuous functions between domains are presented. A function that assigns to a continuous function its least fixed point is defined. Denotational semantics using domains is implemented. Substitution lemma and correctness theorem are proven, and soundness theorem is proved using logical relations. Computational adequacy is at the end shown as a consequence of correctness and soundness theorems. programski jezik PCF operacijska semantika denotacijska semantika domene substitucijska lema izrek o usklajenosti semantike izrek o ustreznosti semantike izrek o primernosti semantike programming language PCF operational semantics denotational semantics domains substitution lemma semantic correctness semantic completeness computational adequacy true false false Slovenski jezik Angleški jezik Delo diplomskega seminarja/zaključno seminarsko delo/naloga 2020-01-25 07:45:04 2020-01-25 07:45:07 2024-05-30 10:16:07 0000-00-00 00:00:00 2020 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 004.43 106296 18974041 1156.pdf 1156.pdf 1 20B8BCE864E5606DEA123A90A103CF74 20f64960416ddeeddfd68a8f3530a6651e617703ad7b3b146539349a0049330c 234f9b3b-a1b8-11eb-a523-00155dcfd717 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=125786 Fakulteta za matematiko in fiziko 0 0 0