HasLin - ett DSL för linjär algebra

Thumbnail Image

Files

CSE 22-21 Grupp 22-28.pdf (1.59 MB)

Date

2023-03-03

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Matematik är en viktig del av datavetenskap och ett vanligt förekommande ämne på teknikinriktade program på universitet är linjär algebra. Om matematik tolkas inom kontexten av ett domänspecifikt språk kan klyftan mellan matematik och datavetenskap överbryggas. Målet med projektet var därmed att skapa ett domänspecifikt språk för linjär algebra, benämnt HasLin. Arbetet var menat till att undersöka hur HasLins korrekthet kan bevisas samt hur domänen kan pedagogiskt förmedlas för att stärka framtida användares kunskaper inom domänen och datavetenskap. HasLin är inbäddat i det funktionella programmeringsspråket Haskell. För att visa HasLins korrekthet konstruerades tester i Haskell samt bevis i bevisassistenten Agda. Resultatet visar att HasLin stödjer en stor mängd grundläggande operationer för linjär algebra, däremot visas inte korrekthet i den mån syftet ämnade. HasLin är anpassat för att vara lätt-använt och är publicerat via ett webbbaserat användargränssnitt vilket tillåter användning av programmet utan ett behov av installerad mjukvara. Viss vidareutveckling behövs, främst inom test och verifikation, för att bevisa HasLins korrekthet för att bättre tjäna projektets syfte.

Description

Mathematics is an important part of computer science and linear algebra is a common subject at university-level engineering programmes. Interpreting mathematics within the context of a domain-specific language can bridge the gap between mathematics and computer science. The goal of the project was thus to create a domain-specific language for linear algebra, named HasLin. The purpose was to investigate how the correctness of Has- Lin can be proven and how the domain can be pedagogically communicated to strengthen future users’ knowledge of the domain and computer science. HasLin is embedded in the functional programming language Haskell. To demonstrate the correctness of HasLin, tests were constructed in Haskell as well as proofs in the proof assistant Agda. The results show that HasLin supports a large set of basic operations for linear algebra, however correctness is not shown to the extent that initially was intended. HasLin is adapted to be easy-to-use and is published via a browser-based user interface, which allows use of HasLin without the need for installed software. Some further development is needed, mainly in testing and verification, to prove the correctness of HasLin to better serve the purpose of the project.

Keywords

Haskell, DSL, Linjär algebra, Agda, pedagogik, bevis

Citation

URI

https://hdl.handle.net/2077/75397

ISBN

Articles

Department

Defence location

Collections

Kandidatuppsatser

Endorsement

Review

Supplemented By

Referenced By