Whereas early researchers in computability theory described effective computability in terms of such models as Turing machines, Markov algorithms, and register machines, a recent trend has been to use simple programming languages as computability models. A parallel development to this programming approach to computability theory is the current interest in systematic and scientific development and proof of programs. This paper investigates the feasibility of using formal proofs of programs in computability theory. After describing a framework for formal verification of programs written in a simple theoretical programming language, we discuss the proofs of several typical programs used in computability theory.

Submitted by Maike Costa (maiksebas@gmail.com) on 2016-08-10T14:17:41Z No. of bitstreams: 1 arquivo total.pdf: 975005 bytes, checksum: 6f8194b9c0cb9c0bbd07b1d2b0ba4b9e (MD5) / Made available in DSpace on 2016-08-10T14:17:41Z (GMT). No. of bitstreams: 1 arquivo total.pdf: 975005 bytes, checksum: 6f8194b9c0cb9c0bbd07b1d2b0ba4b9e (MD5) Previous issue date: 2016-06-21 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / The class of primitive recursive functions is not a formal version to the class of algorithmic functions, we study this special class of numerical functions due to the fact of that many of the functions known as algorithmic are primitive recursive. The approach on the class of primitive recursive functions aims to explore this special class of functions and from that, present solutions for the following problems: (1) given the class of primitive recursive derivations, is there an algorithm, that is, a mechanical procedure for recognizing primitive recursive derivations? (2) Is there a universal function for the class of primitive recursive functions? If so, is this function primitive recursive? (3) Are all the algorithmic functions primitive recursive? To provide solutions to these issues, we base on the hypothetical-deductive method and argue based on the works of Davis (1982), Mendelson (2009), Dias e Weber (2010), Rogers (1987), Soare (1987), Cooper (2004), among others. We present the theory of Turing machines which is a formal version to the intuitive notion of algorithm, and after that the famous Church-Turing tesis which identifies the class of algorithmic functions with the class of Turing-computable functions. We display the class of primitive recursive functions and show that it is a subclass of Turing-computable functions. Having explored the class of primitive recursive functions we proved as results that there is a recognizer algorithm to the class of primitive recursive derivations; that there is a universal function to the class of primitive recursive functions which does not belong to this class; and that not every algorithmic function is primitive recursive. / A classe das funções recursivas primitivas não constitui uma versão formal para a classe das funções algorítmicas, estudamos esta classe especial de funções numéricas devido ao fato de que muitas das funções conhecidas como algorítmicas são recursivas primitivas. A abordagem acerca da classe das funções recursivas primitivas tem como objetivo explorar esta classe especial de funções e, a partir disto, apresentar soluções para os seguintes problemas: (1) dada a classe das derivações recursivas primitivas, há um algoritmo, ou seja, um procedimento mecânico, para reconhecer derivações recursivas primitivas? (2) Existe uma função universal para a classe das funções recursivas primitivas? Se sim, essa função é recursiva primitiva? (3) Toda função algorítmica é recursiva primitiva? Para apresentar soluções para estas questões, nos pautamos no método hipotético-dedutivo e argumentamos com base nos manuais de Davis (1982), Mendelson (2009), Dias e Weber (2010), Rogers (1987), Soare (1987), Cooper (2004), entre outros. Apresentamos a teoria das máquinas de Turing, que constitui uma versão formal para a noção intuitiva de algoritmo, e, em seguida, a famosa tese de Church-Turing, a qual identifica a classe das funções algorítmicas com a classe das funções Turing-computáveis. Exibimos a classe das funções recursivas primitivas, e mostramos que a mesma constitui uma subclasse das funções Turing-computáveis. Tendo explorado a classe das funções recursivas primitivas, como resultados, provamos que existe um algoritmo reconhecedor para a classe das derivações recursivas primitivas; que existe uma função universal para a classe das funções recursivas primitivas a qual não pertence a esta classe; e que nem toda função algorítmica é recursiva primitiva.

La complexité implicite est la caractérisation de classes de complexité par des restrictions syntaxiques sur des modèles de calcul. Plusieurs sous-systèmes de la logique linéaire caractérisant le temps polynomial ont été définis: ces systèmes sont corrects (les termes normalisent en temps polynomial) et complets (il est possible de simuler une machine de Turing pendant un nombre polynomial d'étapes). Un des buts sur le long terme est de donner statiquement des bornes de complexité. C’est pourquoi nous cherchons les caractérisations du temps polynomial les plus expressives possible. Notre principal outil est la sémantique des contextes: des jetons voyagent à travers le réseau selon certaines règles. Les chemins définis par ces jetons représentent la réduction du réseau. Contrairement aux travaux précédents, nous ne définissons pas directement des sous-systèmes de la logique linéaire. Nous définissons d'abord des relations -> sur les sous-termes des réseaux de preuves tel que: B -> C ssi ”le nombre de copies de B dépend du nombre de copies de C”. L’acyclicité de -> borne le nombre de copies de chaque sous-terme, donc la complexité du terme. Ensuite nous définissons des sous-systèmes de la logique linéaire assurant l’acyclicité de ->. Nous étudions aussi des caractérisations du temps élémentaire et primitif récursif. Dans le but d’adapter nos sous-systèmes de la logique linéaire à des langages plus riches, nous adaptons la sémantique des contextes aux réseaux d’interaction, utilisés comme langage cible pour de petits langage de programmation. Nous utilisons cette sémantique des contexte pour définir une sémantique dénotationnelle sur les réseaux d’interactions. / Implicit computational complexity is the characterization of complexity classes by syntactic restrictions on computation models. Several subsystems of linear logic characterizing polynomial time have been defined : these systems are sound (terms normalize in polynomial time) and complete (it is possible to simulate a Turing machine during a polynomial number of steps). One of the long term goals is to statically prove complexity bounds. This is why we are looking for the most expressive characterizations possible. Our main tool is context semantics : tokens travel across proof-nets (programs of linear logic) according to some rules. The paths defined by these tokens represent the reduction of the proof-net.Contrary to previous works, we do not directly define subsystems of linear logic. We first define relations -> on subterms of proof-nets such that: B -> C means \the number of copies of B depends on the number of copies of C". The acyclicity of -> allows us to bound the number of copies of any subterm, this bounds the complexity of the term. Then, we define subsystems of linear logic guaranteeing the acyclicity of ->. We also study characterizations of elementary time and primitive recursive time. In orderto adapt our linear logic subsystems to richer languages, we adapt the context semantics to interaction nets, used as a target language for small programming languages. We use this context semantics to define a denotational semantics on interaction nets.