20.500.12556/RUL-139401 Curry-Howardova korespondenca delo diplomskega seminarja Curry-Howard correspondence Teorija tipov je teorija matematičnih konstrukcij. Tipi niso le zbirke objektov, tako kot množice, ampak dopustni načini konstrukcije objektov. Zato elementov tipa ne določa zgolj njihova vsebovanost, ampak predvsem način konstrukcije. Intuicionistična logika je logični sistem, kjer veljavnost izjave ne temelji na njeni resničnostni vrednosti, pač pa na obstoju konstrukcije oziroma dokaza te izjave. Izkaže se, da med teorijo tipov in intuicionistično logiko obstaja naravna povezava, imenovana Curry-Howardov izomorfizem ali korespondenca, ki nam pokaže, kako se izjave v logiki lahko pretvorijo v tipe, njihovi dokazi pa v elemente ustreznih tipov. Type theory is a theory of mathematical constructions. Types represent various possible ways of constructing objects rather than collections of objects as seen in set theory. Terms of a type are not only determined by their inhabitation of that type but also by their construction. Intuitionistic logic is a system in which validity of a statement is not determined by its value but rather by the existence of a construction, or a proof, of that statement. As it turns out, there exists a natural connection between the two systems, called Curry-Howard correspondence or Curry-Howard isomorphism, that maps logical propositions to types, and their respective proofs into terms of corresponding types. teorija tipov lambda račun intuicionistična logika dedukcija Curry-Howardova korepondenca type theory typed lambda calculus intuitionistic logic deduction Curry-Howard correspondence true false false Slovenski jezik Angleški jezik Delo diplomskega seminarja/zaključno seminarsko delo/naloga 2022-09-02 08:15:07 2022-09-02 08:15:10 2024-05-29 12:17:53 0000-00-00 00:00:00 2022 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.6 125419 120035587 5332.pdf 5332.pdf 1 2DA01B48E6AD402E10375DE5B7074855 94ed0ff1f29f95196b4980631c0ef2e52b39afa53543a46dbc2a1cd60a943527 8ece4820-2a86-11ed-92af-00155dcfd717 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=159962 Fakulteta za matematiko in fiziko 0 0 0