Provable computable functions on abstract data types

Autor:	Jeffery I. Zucker, John V. Tucker, S. S. Wainer
Rok vydání:	2005
Předmět:	Discrete mathematics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computable function TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computability Primitive recursive function Sequent calculus Context (language use) Natural number Function (mathematics) Abstract data type Mathematics
Zdroj:	Automata, Languages and Programming ISBN: 3540528261 ICALP
DOI:	10.1007/bfb0032065
Popis:	We work in the context of abstract data types, modelled as classes of many-sorted algebras. We develop notions of computability over such data types, in particular notions of primitive recursiveness and μ-recursiveness, which generalize the corresponding classical notions over the natural numbers. We also develop classical and intuitionistic formal systems for theories over such data types, and prove (in the case of universal theories) that if an existential assertion is provable in either of these systems, then it has a primitive recursive selection function. It is a corollary that if a μ-recursive scheme is provably total, then it is extensionally equivalent to a primitive recursive scheme. The methods are proof-theoretical, involving cut elimination. These results generalize to an abstract setting previous results of Parsons and Mints over the natural numbers.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::c977ecbbe880a640be4231fcc8dfff7c https://doi.org/10.1007/bfb0032065 Zobrazit plný text záznamu