Formalizing Abstract Computability: Turing Categories in Coq
| Autor: | Amy P. Felty, Polina Vinogradova, Philip J. Scott |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
General Computer Science
Computer science Computation Computability 010102 general mathematics Proof assistant 0102 computer and information sciences Mathematical proof 01 natural sciences Theoretical Computer Science Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computable function 010201 computation theory & mathematics Computability theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Mathematics::Category Theory 0101 mathematics Category theory Categorical algebra Turing computer computer.programming_language |
| Zdroj: | LSFA |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2018.10.013 |
| Popis: | The concept of computable functions (as developed by Godel, Church, Turing, and Kleene in the 1930's) has been extensively studied, leading to the modern subject of recursive function theory. However recent work by category theorists has led to a more conceptual and abstract foundation of computability theory—Turing categories. A Turing category models the notion of partial map as well as recursive computation, using methods of categorical algebra to formalize these concepts. The goal of this work is to provide a formal framework for analyzing this categorical model of computation. We use the Coq Proof Assistant, which implements the Calculus of (co)Inductive Constructions (CIC), and we build on an existing Coq library for general category theory. We focus on both formalizing Turing categories and on building a general framework in the form of a well-structured Coq library that can be further extended. We begin by formalizing definitions, propositions, and proofs pertaining to Turing categories, and then instantiate the more general Turing category formalism with a CIC description of the category which explicitly models the language of partial recursive functions. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect