Kartezijanski zatvorene kategorije

master's thesis

• Author: Nikola Henezi
• Mentor: Mladen Vuković (mentor)
• Mentor: Boris Širola (mentor)
• Committee member: Mladen Vuković (predsjednik povjerenstva)
• Committee member: Boris Širola (član povjerenstva)
• Committee member: Mladen Jurak (član povjerenstva)
• Committee member: Maja Resman (član povjerenstva)
• Granter: University of Zagreb; Faculty of Science; (Department of Mathematics); Zagreb
• Defense date and country: 2018-09-26, Croatia
• Scientific / art field, discipline and subdiscipline: NATURAL SCIENCES; Mathematics

Abstract

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.

Abstract (english)

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.

• Keywords: teorija kategorija; kartezijanski zatvorene kategorije; Curry-Howard-Lambekov izomorfizam; Haskell; \(\lambda-\)račun; lambda-račun; λ-račun
• Keywords (english): category theory; Cartesian closed categories; Curry-Howard-Lambek isomorphism; Haskell; \(\lambda-\)calculus; lambda-calculus; λ-calculus
• Language: croatian
• URN:NBN: urn:nbn:hr:217:507297
• Study programme: Title: Computer Science and Mathematics; Study programme type: university; Study level: graduate; Academic / professional title: magistar/magistra računarstva i matematike (magistar/magistra računarstva i matematike)
• Type of resource: Text
• File origin: Born digital
• Access conditions: Open access
• Repository: Repository of the Faculty of Science
• Created on: 2019-04-24 11:41:40