HasLin - ett DSL för linjär algebra
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.
Degree
Student essay
Other 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.
Collections
View/ Open
Date
2023-03-03Author
Eliasson, Adam
Nikoalev, Daniel
Nordmark, Filip
Sjögren, Sebastian
Sundkvist, Linus
Keywords
Haskell
DSL
Linjär algebra
Agda
pedagogik
bevis
Language
swe