{"id":{"repo_id":"brock","oai_identifier":"oai:brocku.scholaris.ca:10464/12996"},"canonical_url":"https://search.dev.ndltd.org/etd/brock/oai:brocku.scholaris.ca:10464/12996","repository":{"repo_id":"brock","name":"Brock University","base_url":"https://brocku.scholaris.ca/server/oai/request"},"display":{"title":"Approximation Algorithms using Allegories and Coq","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Chowdhury, Durjay"],"institution":"Brock University","degree_name":"M.Sc. Computer Science","degree_level":"Masters","degree_discipline":"Faculty of Mathematics and Science","degree_department":"Department of Computer Science","school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2017,"date_issued":"2017-09-18T18:37:56Z","date_published":"2017-09-18T18:37:56Z","updated_at":"2026-07-24T01:23:20Z","subjects":["Approximation Algorithms","Allegory","Coq"],"languages":["eng"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10464/12996","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.department","label":"Department","values":["Department of Computer Science"]},{"key":"dc:creator","label":"Author","values":["Chowdhury, Durjay"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2017-09-18T18:37:56Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2017-09-18T18:37:56Z"]},{"key":"dc:date.issued","label":"Date","values":["2017-09-18T18:37:56Z"]},{"key":"dc:type","label":"Dc Type","values":["Electronic Thesis or Dissertation"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Faculty of Mathematics and Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.Sc. Computer Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Brock University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Approximation Algorithms","Allegory","Coq"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10464/12996"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["Approximation Algorithms using Allegories and Coq"]}]}],"canonical_facts":{"dc:contributor.department":["Department of Computer Science"],"dc:creator":["Chowdhury, Durjay"],"dc:date.accessioned":["2017-09-18T18:37:56Z"],"dc:date.available":["2017-09-18T18:37:56Z"],"dc:date.issued":["2017-09-18T18:37:56Z"],"dc:description.abstract":["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."],"dc:identifier.uri":["http://hdl.handle.net/10464/12996"],"dc:language.iso":["eng"],"dc:subject":["Approximation Algorithms","Allegory","Coq"],"dc:title":["Approximation Algorithms using Allegories and Coq"],"dc:type":["Electronic Thesis or Dissertation"],"thesis:degree_discipline":["Faculty of Mathematics and Science"],"thesis:degree_level":["Masters"],"thesis:degree_name":["M.Sc. Computer Science"],"thesis:institution_name":["Brock University"]},"updated_at":"2026-07-24T01:23:20Z"}