Em sua resposta a essa pergunta , Stephane Gimenez me indicou um algoritmo de normalização em tempo polinomial para provas em lógica linear. A prova no artigo de Girard usa redes de prova, que são um aspecto da lógica linear de que eu realmente não sei muito. Agora, eu tentei ler artigos sobre...
Provavelmente, a aplicação mais comum de tipos lineares no PL é usá-los para fornecer linguagens que controlam o aliasing (ou seja, um valor linear tem um único ponteiro para ele, mais ou menos). Mas há uma pequena incompatibilidade entre esse uso e os modelos denotacionais típicos da lógica...
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
Suponha que estamos lidando com uma linguagem de programação que suporta tipos lineares (os termos do tipo linear podem ser usados no máximo uma vez, por assim dizer). Isso permite tratar alguns efeitos computacionais (como mutação, até mesmo alterar o tipo do operando) de uma maneira...
Se você observar os combinadores recursivos no cálculo lambda sem tipo, como o combinador Y ou o combinador ômega: É claro que todos esses combinadores acabam duplicando uma variável em algum lugar de sua definição.ωY==( λ x .xx )( λ x .xx )λ f.( λ x .f( xx ) )( λ x .f( xx )...
A lógica linear é interpretada usando espaços coerentes , e eles aparecem com destaque nos papéis de Girard. Conheço todas as três principais maneiras de defini-las formalmente, e elas realmente não apresentam nenhum problema para usar e provar coisas, mas simplesmente não consigo entender o que...
\newcommand{\symp}{\Bumpeq} Uma relação de coerência ≎X≎X\symp_X em um conjunto XXX é uma relação reflexiva e simétrica. Um espaço de coerência é um par (X,≎X)(X,≎X)(X, \symp_X) , e um morfismo f:X→Yf:X→Yf : X \to Y entre espaços de coerência é uma relação f⊆X×Yf⊆X×Yf \subseteq X \times Y tal que...
Estou tentando entender a lógica linear para entender melhor os sistemas de tipos lineares. No entanto, quando li as regras, eu não conseguem obter uma intuição por trás dele como eu fiz na lógica modal - significa um é exigido como em Kripke quadros Um é necessário para cada mundo acessível [ ◊ A...
Somos capazes de provar um teorema de parametridade livre sobre funções como f:∀A.[A]⊸[A]f:∀A.[A]⊸[A]f : \forall A . [A] ⊸ [A] ? Supõe-se que fff pega uma lista e sempre retorna uma permutação dela. Outro exemplo: prove que a função f:∀A.(A⊸(A,A))⊸[A]⊸[A]f:∀A.(A⊸(A,A))⊸[A]⊸[A]f : \forall A . (A ⊸...
A questão é se é possível modelar na lógica linear dois modos de acesso a um recurso. Eu sei que dois modos de recursos são possíveis, ou seja: ! r ⊢!r⊢!r \vdash r está infinitamente disponível r ⊢r⊢r \vdash \quad r está disponível apenas uma vez Mas e se eu não quiser decidir se r é...
Na pesquisa de Melliès, Semântica categórica da lógica linear , é dado um procedimento de eliminação de corte para a lógica linear intuicionista, que inclui o seguinte caso: 3.9.3 Promoção x contração A prova é transformado em prova pi 1π1⋮! Y ⊢ Um! Y- ⊢ ! UMA Promoçãoπ2⋮Υ1, ! Um , ! A , Υ2⊢...