Approximation Algorithms using Allegories and Coq

In this thesis, we implement several approximation algorithms for solving optimization problems on graphs. The result computed by the algorithm may or may not be optimal. The approximation factor of an algorithm indicates how close the computed result is to an optimal solution. We are going to verify two properties of each algorithm in this thesis.First, we show that the algorithm computes a solution to the problem, and, second, we show that the approximation factor is satisfied. To implement these algorithms, we use the algebraic theory of relations, i.e., the theory of allegories and various extension thereof. An implementation of various kinds of lattices and the theory of categories is required for the declaration of allegories. The programming language and interactive theorem prover Coq is used for the implementation purposes. This language is based on Higher-Order Logic (HOL) with dependent types which support both reasoning and program execution. In addition to the abstract theory, we provide the model of set-theoretic relations between finite sets. This model is executable and used in our examples. Finally, we provide an example for each of the approximation algorithm.

Name thesis:degree_name

M.Sc. Computer Science

Level thesis:degree_level

Masters

Discipline thesis:degree_discipline

Faculty of Mathematics and Science

Department dc:contributor.department

Department of Computer Science

Grantor

Brock University

Year dc:date.issued

2017

Author dc:creator

• Chowdhury, Durjay

• Approximation Algorithms
• Allegory
• Coq

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/10464/12996

OAI identifier oai:identifier

oai:brocku.scholaris.ca:10464/12996