Encoding Finite State Automata in Agda using coinduction
Evaluating the support for coinduction in Agda
N.P. Soekarman (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Jesper Cockx – Mentor (TU Delft - Programming Languages)
B. Liesnikov – Mentor (TU Delft - Programming Languages)
Diomidis Spinellis – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
The proof assistant Agda supports coinduction, which can be used to reason about infinite and cyclic structures. The possibilities and limitations of using coinduction in Agda are not well known. To better understand these, I will implement Finite State Automata and their equivalence in Agda. Finite State Automata (FSA) is an example of a cyclic structure. FSA are an introductory model in computation theory, and can be used text processing and hardware design. Equivalence of two FSA is used in software and hardware verification. I created various encodings for FSA and prove equivalence between two deterministic FSA for each of them. At the end, I compared them and see whether they are limited by the support for coinduction in Agda.