Abaixo, o MSO denota a lógica monádica de segunda ordem de gráficos com quantificações de conjuntos de vértices e de arestas. Seja uma pequena família fechada de gráficos. Segue-se da teoria menor do gráfico de Robertson e Seymour que é caracterizada por uma lista finita de menores proibidos. Em...
Recentemente, Dana Scott propôs o cálculo lambda estocástico, uma tentativa de introduzir elementos probabilísticos no cálculo lambda (sem tipo) com base em uma semântica chamada modelo gráfico. Você pode encontrar seus slides on-line, por exemplo, aqui e seu artigo no Journal of Applied Logic ,...
É sabido que os combinadores S e K são Turing Complete. Existem combinadores que são suficientes para produzir (apenas) as funções recursivas
O problema da satisfação é, obviamente, um problema fundamental no CS teórico. Eu estava brincando com uma versão do problema com infinitas variáveis. \newcommand{\sat}{\mathrm{sat}} \newcommand{\unsat}{\mathrm{unsat}} Configuração básica. Seja XXX um conjunto de variáveis não vazio e...
Em um tópico recente na lista de discussão da Agda, surgiu a questão das leis ηη\eta , na qual Peter Hancock fez comentários instigantes . Meu entendimento é que leis vêm com tipos negativos, ie. conectivos cujas regras de introdução são invertíveis. Para desabilitar para funções, Hank sugere o...
Eu acho que não estou entendendo isso, mas -conversion me parece uma conversão que não faz nada, um caso especial de -conversion em que o resultado é apenas o termo na abstração lambda porque não há nada para fazer, uma espécie de conversão inútil .β β βηη\etaββ\betaββ\betaββ\beta Portanto, talvez...
Alguém pode explicar brevemente (se isso for possível!) Ou me referir a uma referência, resumindo as diferenças entre o cálculo lambda não digitado e o cálculo lambda digitado mais comum? Estou particularmente procurando declarações de seu poder expressivo, equivalências a sistemas lógicos /...
É possível testar algoritmicamente se um número computável é racional ou inteiro? Em outras palavras, seria possível para uma biblioteca que implementa números computáveis fornecer as funções isIntegerou isRational? Suponho que isso não seja possível e que isso esteja de alguma forma relacionado...
O teorema automático de prova e pesquisa de provas é mais fácil em lógicas subestruturais lineares e outras proposicionais que carecem de contração? Onde posso ler mais sobre o teorema automático de prova nessas lógicas e o papel da contração na pesquisa de
Este artigo sugere que existem combinadores (representando cálculos simbólicos) que não podem ser representados pelo cálculo Lambda (se eu entendi as coisas
Em sistemas de prova para lógica proposicional clássica se quero mostrar que uma determinada fórmula não é um derivável simplesmente mostra que ¬ ψ pode ser derivada (embora outras técnicas certamente são possíveis). A não derivabilidade decorre essencialmente da solidez e integridade do sistema de...
Existe uma maneira de provar o seguinte teorema em Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDIT : Uma tentativa de dar uma breve explicação sobre "o que é irrelevância para a prova" (corrija-me alguém se eu estiver errado ou impreciso) A idéia básica é que, no...
Eu sei que é impossível decidir equivalência para o cálculo lambda sem tipo. Citando Barendregt, HP O cálculo Lambda: sua sintaxe e semântica. Holanda do Norte, Amsterdã (1984). :ββ\beta Se A e B são disjuntos, conjuntos não vazios de termos lambda que são fechados em igualdade, então A e B são...
Estou procurando exemplos naturais de algoritmos eficientes (isto é, em tempo polinomial) st sua correção e eficiência podem ser comprovadas construtivamente (por exemplo, na ou na ), masPR APRUMAPRAHUMAHUMAHA nenhuma prova usando apenas conceitos eficientes é conhecida (ou seja, não sabemos como...
Contexto: relações entre lógica e autômatos O Teorema de Büchi afirma que a lógica monádica de segunda ordem sobre seqüências de caracteres (MSO) captura a classe de linguagens regulares. A prova realmente mostra que o MSO existencial ( ou EMSO ) sobre cadeias de caracteres é suficiente para...
Eu sou um estudante de graduação em matemática com uma sólida formação em lógica. Eu fiz um curso de graduação de um ano em lógica, juntamente com cursos de teoria dos modelos finitos e outro sobre forçar e definir teoria. A maioria dos textos de CS parece assumir apenas um fundo muito modesto da...
Estou procurando um exemplo fácil de dois sistemas de transição equivalentes a LTL, mas não equivalentes a traços. Li a prova de que a Equivalência de traços é mais refinada do que a Equivalência de LTL no livro "Princípios de verificação de modelos" (Baier / Katoen), mas não tenho certeza se...
A partir de Curry-Howard-Lambek, houve uma boa trindade de teorias de tipos, lógicas e categorias. Estou curioso sobre a semântica categórica que você obtém ao adicionar subtipos (coercitivos) a uma teoria de tipos - parece que isso não foi muito explorado, se é que realmente foi. Em geral,...
Na teoria dos autômatos (autômatos finitos, autômatos de empilhamento, ...) e na complexidade, existe a noção de "ambiguidade". Um autômato é ambíguo se houver uma palavra com pelo menos duas execuções de aceitação distintas. Uma máquina é ambígua se, para cada palavra aceita pela máquina, houver...
No passado, implementei modelos de coordenação usando SAT e satisfação regular de restrições como o cavalo de batalha principal em seus motores. Continuando nesta linha de trabalho, gostaria de tornar os modelos mais interativos, e a melhor maneira de fazer isso é abrir o solucionador de restrições...