Verificação das propriedades computacionais de um modelo funcional de primeira-ordem

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorAyala-Rincón, Mauricio-
Autor(es): dc.contributorMuñoz, César Augusto-
Autor(es): dc.creatorRamos, Thiago Mendonça Ferreira-
Data de aceite: dc.date.accessioned2024-10-23T16:20:49Z-
Data de disponibilização: dc.date.available2024-10-23T16:20:49Z-
Data de envio: dc.date.issued2024-08-13-
Data de envio: dc.date.issued2024-08-13-
Data de envio: dc.date.issued2024-08-13-
Data de envio: dc.date.issued2023-06-15-
Fonte completa do material: dc.identifierhttp://repositorio2.unb.br/jspui/handle/10482/49836-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/906077-
Descrição: dc.descriptionTese (Doutorado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2023.-
Descrição: dc.descriptionEste trabalho descreve a mecanização de propriedades computacionais de um modelo funcional que tem sido aplicado para automatizar o raciocínio sobre a terminação de programas. A formalização foi desenvolvida no assistente de provas de lógica de ordem superior, chamado Prototype Verification System (PVS). O modelo de linguagem foi projetado para imitar o fragmento de primeira ordem de especificações funcionais e é chamado PVS0. Foram considerados dois modelos computacionais: o primeiro modelo especifica um programa funcional por meio de uma única função (modelo single-function PVS0, ou SF-PVS0), e o segundo modelo permite a especificação simultânea de múltiplas funções (modelo multiple-function PVS0, ou MF-PVS0). A semântica operacional da recursão na especificação do modelo SF-PVS0suporta a recursão sobre o programa completo. Por outro lado, em programas MF-PVS0, as chamadas funcionais são permitidas para todas as funções especificadas no programa. Este trabalho tem como objetivo certificar matematicamente a robustez dos modelos PVS0 como modelos computacionais universais. Para isso, propriedades cruciais e teoremas foram formalizados, incluindo Turing Completude, a indecidibilidade do Problema da Parada, o teorema da recursão, o teorema de Rice e o teorema do Ponto Fixo. Além disso, o trabalho discute avanços na indecidibilidade do Problema da Palavra e do Problema da Correspondência de Post. A indecidibilidade do Problema da Parada foi formalizada considerando a avaliação semântica de programas PVS0 que foram aplicados na verificação da terminação de especificações em PVS. A equivalência entre a avaliação funcional e predicativa de operadores foi fundamental para esse objetivo. Além disso, a composicionalidade de programas MF-PVS0, habilitada diretamente pela possibilidade de chamar diferentes funções, torna fácil a formalização da Turing Completude. Portanto, enriquecer o modelo foi uma decisão de design importante para simplificar a mecanização dessa propriedade e dos teoremas mencionados acima.-
Descrição: dc.descriptionThis work describes the mechanization of the computational properties of a functionallanguage model that has been applied to reasoning about the automation of program termination. The formalization was developed using the higher-order proof assistant Prototype Verification System (PVS). The language model was designed to mimic the firstorder fragment of PVS functional specifications and is called PVS0. Two different computational models are considered: the first model specifies functional programs through a unique function (single-function PVS0 model, or SF-PVS0), and the second model allows simultaneous specification of multiple functions (multiple-function PVS0 model, or MF-PVS0). This work aims to mathematically certify the robustness of the PVS0 models as universal computational models. For doing that, crucial properties and theorems were formalized, including Turing Completeness, the undecidability of the Halting Problem, the Recursion Theorem, Rice’s Theorem, and the Fixed Point Theorem. Furthermore, the work discusses advances in the undecidability of the Word Problem and the Post Correspondence Problem. The undecidability of the Halting Problem was formalized considering properties of the semantic evaluation of PVS0 programs that were applied in verifying the termination of PVS specifications. The equivalence between predicative and functional evaluation operators was vital to this aim. Furthermore, the compositionality of multiple-function PVS0 programs, straightforwardly enabled by the possibility of calling different functions, makes it easy to formalize of properties such as Turing Completeness. Therefore, enriching the model was an important design decision to simplify the mechanization of this property and the theorems mentioned above.-
Descrição: dc.descriptionInstituto de Ciências Exatas (IE)-
Descrição: dc.descriptionDepartamento de Ciência da Computação (IE CIC)-
Descrição: dc.descriptionPrograma de Pós-Graduação em Informática-
Formato: dc.formatapplication/pdf-
Idioma: dc.languagept_BR-
Direitos: dc.rightsAcesso Aberto-
Direitos: dc.rightsA concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.unb.br, www.ibict.br, www.ndltd.org sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra supracitada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data.-
Palavras-chave: dc.subjectCompletude de Turing-
Palavras-chave: dc.subjectProblema da parada-
Palavras-chave: dc.subjectTeorema de Rice-
Palavras-chave: dc.subjectTeorema do Ponto Fixo-
Título: dc.titleVerificação das propriedades computacionais de um modelo funcional de primeira-ordem-
Título: dc.titleVerifying the computational properties of a first-order functional model-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Institucional – UNB

Não existem arquivos associados a este item.