Atenção:
O eduCAPES é um repositório de objetos educacionais, não sendo responsável por materiais de terceiros submetidos na plataforma. O usuário assume ampla e total responsabilidade quanto à originalidade, à titularidade e ao conteúdo, citações de obras consultadas, referências e outros elementos que fazem parte do material que deseja submeter. Recomendamos que se reporte diretamente ao(s) autor(es), indicando qual parte do material foi considerada imprópria (cite página e parágrafo) e justificando sua denúncia.
Caso seja o autor original de algum material publicado indevidamente ou sem autorização, será necessário que se identifique informando nome completo, CPF e data de nascimento. Caso possua uma decisão judicial para retirada do material, solicitamos que informe o link de acesso ao documento, bem como quaisquer dados necessários ao acesso, no campo abaixo.
Todas as denúncias são sigilosas e sua identidade será preservada. Os campos nome e e-mail são de preenchimento opcional. Porém, ao deixar de informar seu e-mail, um possível retorno será inviabilizado e/ou sua denúncia poderá ser desconsiderada no caso de necessitar de informações complementares.
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Ayala-Rincón, Mauricio | - |
Autor(es): dc.contributor | Muñoz, César Augusto | - |
Autor(es): dc.creator | Ramos, Thiago Mendonça Ferreira | - |
Data de aceite: dc.date.accessioned | 2024-10-23T16:20:49Z | - |
Data de disponibilização: dc.date.available | 2024-10-23T16:20:49Z | - |
Data de envio: dc.date.issued | 2024-08-13 | - |
Data de envio: dc.date.issued | 2024-08-13 | - |
Data de envio: dc.date.issued | 2024-08-13 | - |
Data de envio: dc.date.issued | 2023-06-15 | - |
Fonte completa do material: dc.identifier | http://repositorio2.unb.br/jspui/handle/10482/49836 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/capes/906077 | - |
Descrição: dc.description | Tese (Doutorado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2023. | - |
Descrição: dc.description | Este 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.description | This 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.description | Instituto de Ciências Exatas (IE) | - |
Descrição: dc.description | Departamento de Ciência da Computação (IE CIC) | - |
Descrição: dc.description | Programa de Pós-Graduação em Informática | - |
Formato: dc.format | application/pdf | - |
Idioma: dc.language | pt_BR | - |
Direitos: dc.rights | Acesso Aberto | - |
Direitos: dc.rights | A 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.subject | Completude de Turing | - |
Palavras-chave: dc.subject | Problema da parada | - |
Palavras-chave: dc.subject | Teorema de Rice | - |
Palavras-chave: dc.subject | Teorema do Ponto Fixo | - |
Título: dc.title | Verificação das propriedades computacionais de um modelo funcional de primeira-ordem | - |
Título: dc.title | Verifying the computational properties of a first-order functional model | - |
Tipo de arquivo: dc.type | livro digital | - |
Aparece nas coleções: | Repositório Institucional – UNB |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: