Induktiiviset tyypit
Authors
Date
2024Copyright
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
Induktiiviset tyypit ovat tapa mallintaa erilaisia tietotyyppejä kuten listoja, luonnollisia lukuja ja binäärihakupuita tyyppiteoriassa. Induktiivisia tyyppejä käytetään laajasti todistusassistenteissa erilaisten teoreemojen ja tietokoneohjelmien toteutukseen. Yleistys induktiivisista tyypeistä ovat korkeammat induktiiviset tyypit, jotka laajentavat induktiivisia tyyppejä mahdollistamalla tyypin alkioiden välisten ekvivalenssirelaatioiden määrittämisen. Tässä kirjallisuuskatsauksessa käsitellään induktiivisten ja korkeampien induktiivisten tyyppien teoriaa, niiden toteutuksia eri
ohjelmointikielissä sekä erilaisia sovelluskohteita. Inductive types are a way to represent complex datatypes such as lists, natural numbers and binary search trees in type theory. Inductive types are currently widely used in proof assistants to implement mathematical theorems and computer
programs. A generalization of inductive types are higher inductive types, which extend inductive types by making it possible to define equivalence relations between inhabitants of a type. This thesis explores theory behind inductive and higher inductive types, their implementations in different programming languages and their use cases.
Keywords
Metadata
Show full item recordCollections
- Kandidaatintutkielmat [5319]
Related items
Showing items with similar title or keywords.
-
Ariteetti- ja tietotyyppigeneerinen ohjelmointi Coq-todistusassistentilla
Pehkonen, Jere (2021)Tutkielman tavoitteena on luoda toimiva kirjasto ariteetti- ja tietotyyppigeneeristä ohjelmointia varten. Ariteetti- ja tietotyyppigeneerinen ohjelmointi edesauttaa toisteisen lähdekoodin määrän vähentämistä sekä määritelmien ... -
Metatieto tietovarastoympäristössä
Niemijärvi, Ville (2002)