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

10
10-я проблема Гильберта и диофантово уравнение Чейтина «Компьютер»?

В мета математике Чейтина! В Поисках Омеги он кратко рассказывает о 10-й проблеме Гильберта. Затем он говорит, что любое диофантово уравнение можно заменить на два равных полинома с положительными целыми коэффициентами: .p=0p=0p=0p=0⟺p1=p2p=0⟺p1=p2p=0 \iff p_1 = p_2 Затем он говорит, что мы можем...

10
анонимные лямбда-функции (функциональное программирование)

Что такое анонимные (лямбда) функции? Каково формальное определение анонимной функции в функциональном языке программирования? Проще говоря, когда я программирую на схеме / lisp, я бы сказал, что анонимная (лямбда) функция - это функция, которая не связана с идентификатором. Это все, что вы можете...

10
Язык программирования, который может реализовывать только вычислимые биективные функции?

Существуют ли языки программирования (или логика), которые могут реализовать (или выразить) функцию тогда и только тогда, когда f вычислимые биективные функции?f:N→Nf:N→Nf:\mathbb{N}\to...

10
Разные переменные для разных предложений

При доказательстве теоремы разрешения обычно предполагается, что переменные в разных разделах различны. Это не то, что происходит автоматически; это требует значительного дополнительного кода и вычислений для реализации. Учитывая это, я ищу тестовый пример для него. Проблема в том, что во всех...

9
Простейшая полная пара базисов комбинаторов для плоских выражений

В работе Криса Окасаки « Сглаживание комбинаторов: выживание без скобок » он показывает, что двух комбинаторов достаточно и необходимо в качестве основы для кодирования выражений по Тьюрингу без необходимости использования оператора приложения или скобок. По сравнению с кодировками комбинаторной...

9
Уловка, использованная в доказательстве двукратно экспоненциальной сложности арифметики Пресбургера

Я разместил это на MathUnderflow, но не получил ответов, поэтому решил попробовать здесь, Я читаю старую статью Рабина и Фишера [опубликует ссылку, когда это возможно], где, помимо прочего, доказана двоякая экспоненциальная сложность арифметики Пресбургера. Доказательство основывается на...

9
Цепи глубины-2 с вентилями OR и MOD не универсальны?

Хорошо известно, что каждая булева функция может быть реализована с использованием булевой схемы глубины 2 (над переменными, их отрицанием и постоянными значениями) содержащий логические элементы И на первом уровне и один логический элемент ИЛИ на верхнем уровне; это просто представление DNF из...

9
Каково текущее состояние параллельных или параллельных программ в изоморфизме Карри-Ховарда?

В « Доказательствах и типах» Жирара мы можем прочитать: С алгоритмической точки зрения, секвенциальное исчисление не имеет изоморфизма Карри-Ховарда из-за множества способов написания одного и того же доказательства. Это мешает нам использовать его в качестве типизированного исчисления, хотя мы...

9
Термины комбинаторной логики всегда больше?

Таким образом, существует алгоритм преобразования терминов лямбда-исчисления в комбинаторную логику с использованием комбинаторов SK. Это производит вещи, которые взрываются в размере. Я хотел бы знать больше об этом взрыве в размере. Однако я не могу придумать лучшего алгоритма. Я слышал, что...

9
Введение в проверку логики первого порядка

Я пытаюсь научить себя различным подходам к проверке программного обеспечения. Я прочитал несколько статей. Насколько я узнал, логика высказываний с темпоральным обычно использует проверку моделей с помощью решателей SAT (в текущих - реактивных системах), но как насчет логики первого порядка с...