Certifying Time Complexity of Agda Programs Using Complexity Signatures
Translated title
Certificering af Tidskompleksitet af Agda Programmer Ved Brug af Kompleksitetssignaturer
Authors
Rannes, Simon Quist ; Elgaard, Johannes ; Møllnitz, Christian Bach
Term
4. term
Education
Publication year
2020
Submitted on
2020-06-14
Pages
86
Abstract
Previous work has shown that time-complexity analysis in functional languages is possible by annotating functions, but the question of how few annotations are needed has been less explored. We present a small library that enables certifying time complexity with minimal annotations using a Timed monad. In simple terms, a Timed monad is a programming construct that carries timing information through computations. Using this approach, we build a library of matrix functions with certified time complexity and implement the Cocke–Younger–Kasami (CYK) parsing algorithm for context-free grammars, which we certify to run in O(n^5). All implementations are in Agda, a dependently typed programming language that lets us express and prove such properties within the code.
Tidligere arbejde har vist, at man kan analysere tidskompleksitet i funktionelle programmeringssprog ved at annotere funktioner, men det er sparsomt undersøgt, hvor få annoteringer der kræves. Vi præsenterer et lille bibliotek, der gør det muligt at certificere tidskompleksitet med minimale annoteringer ved hjælp af en Timed monad. Kort sagt er en Timed monad en programmeringskonstruktion, der lader beregninger bære information om deres tidsforbrug. Med denne metode bygger vi et bibliotek af matrixfunktioner med certificeret tidskompleksitet og implementerer Cocke–Younger–Kasami (CYK) parseren for kontekstfrie grammatikker, som vi certificerer til at have O(n^5) tidskompleksitet. Alt er implementeret i Agda, et programmeringssprog med afhængige typer, der gør det muligt at udtrykke og bevise sådanne egenskaber direkte i koden.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords