Back to Search
Start Over
Formalizing Abstract Computability: Turing Categories in Coq
- Source :
- LSFA
- Publication Year :
- 2018
- Publisher :
- Elsevier BV, 2018.
-
Abstract
- 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.
- Subjects :
- 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
Subjects
Details
- ISSN :
- 15710661
- Volume :
- 338
- Database :
- OpenAIRE
- Journal :
- Electronic Notes in Theoretical Computer Science
- Accession number :
- edsair.doi...........bdac495ad178035f3fddd8367e4b42d4