An Agda proof of the correctness of Valiant’s algorithm for context free parsing
| dc.contributor.author | Bååth Sjöblom, Thomas | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers) | sv |
| dc.contributor.department | Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers) | en |
| dc.date.accessioned | 2019-07-03T13:17:51Z | |
| dc.date.available | 2019-07-03T13:17:51Z | |
| dc.date.issued | 2013 | |
| dc.description.abstract | Parsing is an important problem with applications ranging from compilers to bioinformatics. To perform the parsing more quickly, it would be desirable to be able to parse in parallel. Valiant’s algorithm [Valiant, 1975] is a divide and conquer algorithm for parsing and can be used to perform a large part of the work in parallel. It is fairly easy to implement in a functional programming languages, using pattern matching. Agda is a dependently typed functional programming language that doubles as a proof assistant and is hence very suitable for implementing and proving the correctness of Valiant’s algorithm. In this thesis, we provide a very natural specification for the parsing problem and prove that it is equivalent to the specification of the transitive closure used in [Valiant, 1975], that is further removed from both parsing and proving. We compare the two specifications and use our specification to derive Valiant’s algorithm. We then implement it in Agda and prove our implementation correct (we prove that it satisfies our specification). We also give short introductions to parsing, programming and proving with Agda and to using algebraic structures in Agda. | |
| dc.identifier.uri | https://hdl.handle.net/20.500.12380/185016 | |
| dc.language.iso | eng | |
| dc.setspec.uppsok | Technology | |
| dc.subject | Data- och informationsvetenskap | |
| dc.subject | Computer and Information Science | |
| dc.title | An Agda proof of the correctness of Valiant’s algorithm for context free parsing | |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.degree | Master Thesis | en |
| dc.type.uppsok | H | |
| local.programme | Computer science – algorithms, languages and logic (MPALG), MSc |
Ladda ner
Original bundle
1 - 1 av 1
Hämtar...
- Namn:
- 185016.pdf
- Storlek:
- 911.29 KB
- Format:
- Adobe Portable Document Format
- Beskrivning:
- Fulltext