Kartezijanski zatvorene kategorije

diplomski rad

• Autor: Nikola Henezi
• Mentor: Mladen Vuković (mentor)
• Mentor: Boris Širola (mentor)
• Član povjerenstva: Mladen Vuković (predsjednik povjerenstva)
• Član povjerenstva: Boris Širola (član povjerenstva)
• Član povjerenstva: Mladen Jurak (član povjerenstva)
• Član povjerenstva: Maja Resman (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Prirodoslovno-matematički fakultet; (Matematički odsjek); Zagreb
• Datum i država obrane: 2018-09-26, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: PRIRODNE ZNANOSTI; Matematika

Sažetak

U ovom diplomskom radu proučavamo teoriju kategorija s posebnim fokusom na kartezijanski zatvorene kategorije, jednostavno tipizirani \(\lambda-\)račun i opisujemo vezu između njih koja je poznata kao Curry-Howard-Lambekov izomorfizam. Dan je uvod u teoriju kategorija, te kroz brojne primjere definiramo osnovne pojmove nužne za razumijevanje Curry-Howard-Lambekov izomorfizma. Koristimo programski jezik Haskell za demonstraciju praktične primjene teorija kategorija i lakše razumijevanje nekih koncepata. Definirane su kartezijanski zatvorene kategorije, vrsta kategorije koja ima ekspresivnu moć jednaku tipiziranom \(\lambda-\)računu i pokazano je nekoliko primjera kartezijanski zatvorenih kategorija. Definirano je proširenje jednostavno tipiziranog \(\lambda-\)računa s pravilima dedukcije i osnovni pojmovi vezani za tipizirani \(\lambda-\)račun. U posljednjem poglavlju je opisana konstrukcija kojom se pokazala veza između tipiziranog \(\lambda-\)računa i kartezijanski zatvorenih kategorija. Rad završavamo s primjerom kojim se pokazuje razmjenjivost funkcija u \(\lambda-\)-računu s projekcijama u kartezijanski zatvorenim kategorijama. Dajemo kratki ostvrt na prednosti kategorijskog pristupa u programiranju pozivajući se na nekoliko najčešće korištenih programskih paketa.

Sažetak (engleski)

In this master thesis we study category theory with special focus on Cartesian closed categories and simply typed \(\lambda-\)calculus. We describe the relationship between them, known as Curry-Howard-Lambek isomorphism. An introduction to the category theory and neccesary terms required for understanding the Curry-Howard-Lambek isomorphism are given. Programming language Haskell is used to demonstrate practical applications of category theory. We define Cartesian closed categories, type of category which has expressive power equivalent to the simply typed \(\lambda-\)calculus and demonstrate few examples of Cartesian closed categories. In the last chapter we define a construction that describes relationship between simply typed \(\lambda-\)calculus and Cartesian closed categories. Master thesis is finalized with an example which demonstrates interchangeability of functions in simply typed \(\lambda-\)caluclus with projections in Cartesian closed categories. A short overview with advantages of categorical approach to computation is given, demonstrating practicality with few well known programming libraries.

• Ključne riječi: teorija kategorija; kartezijanski zatvorene kategorije; Curry-Howard-Lambekov izomorfizam; Haskell; \(\lambda-\)račun; lambda-račun; λ-račun
• Ključne riječi (engleski): category theory; Cartesian closed categories; Curry-Howard-Lambek isomorphism; Haskell; \(\lambda-\)calculus; lambda-calculus; λ-calculus
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:217:507297
• Studijski program: Naziv: Računarstvo i matematika; Vrsta studija: sveučilišni; Stupanj studija: diplomski; Akademski / stručni naziv: magistar/magistra računarstva i matematike (mag. inf. et math.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Otvoreni pristup
• Datum i vrijeme pohrane: 2019-04-24 11:41:40