Вопросы с тегом «linear-logic»

24
Как я должен думать о проверочных сетях?

В своем ответе на этот вопрос , Стефан Хименес указал мне на алгоритм нормализации полиномиальное время для доказательств в линейной логике. В доказательстве в статье Жирара используются сети доказательств, которые являются аспектом линейной логики, о которой я на самом деле не очень много знаю. Я...

23
Что такое народная модель линейной логики?

Вероятно, наиболее распространенным применением линейных типов в PL является использование их для предоставления языков, которые управляют псевдонимами (т. Е. Линейное значение имеет единственный указатель на него, более или менее). Но есть небольшое несоответствие между этим использованием и...

18
Автоматическое доказательство теорем в линейной логике

Является ли автоматическое доказательство теорем и поиск доказательств более простым в линейных и других пропозициональных субструктурных логиках, в которых отсутствует сжатие? Где я могу прочитать больше об автоматическом доказательстве теорем в этих логиках и роли сокращения в поиске...

15
Структуры данных в языке программирования с линейными типами

Предположим, мы имеем дело с языком программирования, который поддерживает линейные типы (термины линейного типа можно использовать не более одного раза, так сказать). Это позволяет обрабатывать некоторые вычислительные эффекты (такие как мутация, даже изменение типа операнда) способом, который...

15
Является ли MALL + неограниченные рекурсивные типы Turing-complete?

Если вы посмотрите на рекурсивные комбинаторы в нетипизированном лямбда-исчислении, такие как Y-комбинатор или омега-комбинатор: Понятно, что все эти комбинаторы в конечном итоге дублируют переменную где-то в своем определении.ωYзнак равнознак равно( λ х .Иксх )( λ х .Иксх )λ f,( λ х .е( хх ) )( λ...

13
Можете ли вы объяснить интуицию за когерентными пространствами?

Линейная логика интерпретируется с использованием когерентных пространств , и они выделяются в работах Жирара. Я знаю все три основных способа их формального определения, и они на самом деле не представляют проблемы для использования и доказательства чего-либо, но я просто не могу понять, что они...

12
Когда у пространств когерентности есть откаты и отжимания?

\newcommand{\symp}{\Bumpeq} ≎X≎X\symp_XXXX(X,≎X)(X,≎X)(X, \symp_X)f:X→Yf:X→Yf : X \to Yf⊆X×Yf⊆X×Yf \subseteq X \times Y(x,y)∈f(x,y)∈f(x,y) \in f(x′,y′)∈f(x′,y′)∈f(x',y') \in f если то иx≎Xx′x≎Xx′x \symp_X x'y≎Yy′y≎Yy′y \symp_Y y' если и то .x≎Xx′x≎Xx′x \symp_X x'y=y′y=y′y = y'x=x′x=x′x = x'...

11
Какова интуиция за линейной логикой?

Я пытаюсь понять линейную логику, чтобы лучше понять системы линейного типа. Однако, когда я прочитал правила, я не в состоянии получить интуицию позади него , как я сделал в модальной логике - □ A◻A\Box A означает требуются , как в Крипке кадров требуются для каждого достижимого мира [ ◊ является...