Parece que eu encontrei uma maneira genérica de converter qualquer procedimento recursivo em recursão de cauda: Defina um subprocedimento auxiliar com um parâmetro "resultado" extra. Aplique o que seria aplicado ao valor de retorno do procedimento a esse parâmetro. Ligue para este procedimento...
Sou programador com domínio de autômatos, mas não de lógica. Li nos jornais que os dois estão muito relacionados. Autômatos finitos determinísticos (DFA), autômatos em árvore e autômatos visivelmente pushdown estão todos relacionados à lógica monádica de segunda ordem (MSO). Embora eu entenda que...
Uma expressão combinadora (digamos na base SK) pode ser pensada como uma função que mapeia expressões de cálculo combinador para expressões de cálculo combinador. Ou seja, pode-se pensar em uma expressão XXX como uma função X: L → LX:eu→euX:L \to L , onde eueuL é o conjunto de todas as expressões...
Eu estava pensando em provas e tive uma observação interessante. Portanto, as provas são equivalentes aos programas pelo isomorfismo de Curry-Howard, e as provas circulares correspondem a uma recursão infinita. Mas sabemos do problema da parada que, em geral, testar se um programa arbitrário se...
Eu estava lendo a pergunta Consistência e integridade implicam solidez? e a primeira afirmação diz: Entendo que a solidez implica consistência. O que me deixou bastante intrigado porque pensei que a consistência era uma afirmação mais fraca que a consistência (ou seja, pensei que sistemas...
Atualmente, tenho que aprender Coq e não sei como lidar com or: Como exemplo, por mais simples que seja, não vejo como provar: Theorem T0: x \/ ~x. Eu realmente aprecio isso, se alguém puder me ajudar. Para referência, eu uso esta folha de dicas . Também um exemplo de uma prova que tenho em...
Para descobrir a diferença, acabei de encontrar afirmações abaixo sobre lógica temporal na Wikipedia : outra variante da lógica modal, que compartilha muitas características comuns da lógica dinâmica, difere de todas as lógicas acima mencionadas por ser o que Pnueli caracterizou como lógica...
Em Fundamentos Práticos para Linguagens de Programação , Robert Harper diz Se uma proposição para ser verdadeira significa ter uma prova dela, o que significa que uma proposição seja falsa? Isso significa que a refutamos , mostrando que não pode ser provado. Ou seja, uma proposição é falsa se...
O exemplo a seguir está correto sobre se um algoritmo de inferência é sólido e completo ? Suponha que tenhamos agulhas a, b, c em um palheiro e também tenha um algoritmo de inferência projetado para encontrar agulhas. som - Somente as agulhas a, bec são obtidas. completo - as agulhas a, bec são...
Na discussão em torno dessa questão , Gilles menciona corretamente que qualquer prova de correção de um algoritmo que utiliza matrizes deve provar que não há acesso a matrizes fora dos limites; dependendo do modelo de tempo de execução, isso causaria um erro de tempo de execução ou acesso a...
Atualmente, estou aprendendo o cálculo lambda e estava pensando nos dois tipos diferentes de escrita de um termo lambda. λ x y. x yλxy.xy\lambda xy.xy λ x . λ y. x yλx.λy.xy\lambda x.\lambda y.xy Existe alguma diferença no significado ou na maneira como você aplica a redução beta, ou essas...
Você pode me dar algumas sugestões sobre um bom livro introdutório (mas abrangente) sobre lógica e computação? Alguns tópicos difusos que tenho em mente são: Presburger artihm., PA, ZF, ZFC, HOL Teoria dos conjuntos, Teoria dos tipos Computação de modelagem (máquinas de Turing) em diferentes...
Um dispensador de bebidas exige que o usuário insira uma moeda ( ) e pressione um dos três botões: solicita uma xícara de chá , o mesmo para café , e solicita um reembolso (ou seja, a máquina devolve a moeda: ). Este dispensador pode ser modelado pelo seguinte processo CCS :ˉ d cháechá ˉ r ˉ...
No trabalho, fui encarregado de deduzir algumas informações de tipo sobre uma linguagem dinâmica. Reescrevo seqüências de instruções em letexpressões aninhadas , da seguinte maneira: return x; Z => x var x; Z => let x = undefined in Z x = y; Z => let x = y in Z if x then T else F; Z =>...
O que são funções anônimas (lambda)? Qual é a definição formal de uma função anônima em uma linguagem de programação funcional? Em meus termos simples, quando estou programando no esquema / lisp, eu diria que uma função anônima (lambda) é uma função que não está vinculada a um identificador. É...
Estou curioso. Eu tenho trabalhado nesse tipo de dados no OCaml : type 'a exptree = | Epsilon | Delta of 'a exptree * 'a exptree | Omicron of 'a | Iota of 'a exptree exptree Que pode ser manipulado usando funções recursivas de tipo explícito (um recurso que foi adicionado recentemente)....
Tentei resolver o exercício a seguir, mas fiquei preso ao tentar encontrar todos os pares críticos . Tenho as seguintes perguntas: Como sei qual par crítico produziu uma nova regra? Como sei que encontrei todos os pares críticos? Seja onde é binário, é unário e é uma constante. ∘ i e E = {...
Pode-se mostrar que dois modelos de computação são completos, se cada um pode codificar um simulador universal para o outro. Pode-se mostrar que duas lógicas são completas se uma codificação das regras de inferências (e talvez axiomas, se presentes) de cada uma se mostrar como teoremas da outra. Na...
Na Meta Matemática de Chaitin ! The Quest For Omega , ele fala brevemente sobre o 10º Problema de Hilbert. Ele então diz que qualquer equação diofantina pode ser alterada em dois polinômios iguais com coeficientes inteiros positivos: .p = 0p = 0p=0p=0p = 0⟺p1 1= p2p=0⟺p1=p2p=0 \iff p_1 = p_2 Então...
De acordo com Peter Selinger , O cálculo lambda é algébrico (PDF). No início deste artigo, ele diz: Sabe-se que a interpretação combinatória do cálculo lambda é imperfeita, pois não satisfaz a regra ξξξ : sob a interpretação, M= NM=NM = N não implica λ x . M= λ x . Nλx.M=λx.N\lambda x.M =...