Выражение комбинатора (скажем, в основе SK) можно рассматривать как функцию, которая отображает выражения исчисления комбинатора в выражения исчисления комбинатора. То есть выражение как функцию , где - множество всех синтаксически допустимых выражений комбинатора в базисе SK. Это отображение...
Я думал о доказательствах и столкнулся с интересным наблюдением. Таким образом, доказательства эквивалентны программам через изоморфизм Карри-Говарда, а круговые доказательства соответствуют бесконечной рекурсии. Но из проблемы остановки мы знаем, что в общем случае проверка того, будет ли...
Я думал, что правильно понял зависимую типизацию (DT), но ответ на этот вопрос: /cstheory/30651/why-was-there-a-need-for-martin-l%C3% Теория типа «создать творческий интуиционизм» заставила меня думать иначе. После прочтения DT и попыток понять, что они из себя представляют, я пытаюсь задаться...
Я читал вопрос, что последовательность и полнота означают разумность? и первое утверждение в нем говорит: Я понимаю, что разумность подразумевает последовательность. Что меня очень озадачило, потому что я думал, что разумность была более слабым утверждением, чем последовательность (то есть я думал,...
В практических основах Языки программирования , Роберт Харпер говорит Если для утверждения быть истинным означает иметь доказательство этого, что это означает для предложения быть ложным? Это значит, что у нас есть опровержение , доказывающее, что это невозможно доказать. То есть утверждение...
Чтобы найти разницу, я только что столкнулся с утверждениями ниже о временной логике в Википедии : Другой вариант модальной логики, разделяющий многие общие черты с динамической логикой, отличается от всех вышеупомянутых логик тем, что Пнуэли охарактеризовал как «эндогенную» логику, а другие -...
В настоящее время я должен изучить Coq и не знаю, как бороться с or: Как простой пример, я не вижу, как это доказать: Theorem T0: x \/ ~x. Буду очень признателен, если кто-нибудь сможет мне помочь. Для справки я использую этот шпаргалку . Также пример доказательства, которое я имею в виду: здесь...
В настоящее время я изучаю лямбда-исчисление, и мне было интересно узнать о двух разных видах написания лямбда-термина. λxy.xyλxy.xy\lambda xy.xy λx.λy.xyλx.λy.xy\lambda x.\lambda y.xy Есть ли разница в значении или способе применения бета-сокращения, или это просто два способа выразить одно и то...
Диспенсер для напитков требует, чтобы пользователь вставил монету ( ), а затем нажмите одну из трех кнопок: запрашивает чашку чая , то же самое для кофе , и запрашивает возврат (т. е. автомат возвращает монету: ). Этот дозатор может быть смоделирован следующим процессом CCS :c¯c¯\bar...
Можете ли вы дать мне несколько советов о хорошей вводной (но всеобъемлющей) книге о логике и вычислениях? Некоторые нечеткие темы, которые я имею в виду: Presburger artihm., PA, ZF, ZFC, HOL Теория множеств, Теория типов Моделирование вычислений (машины Тьюринга) в разных теориях Связи с...
На работе мне было поручено вывести некоторую информацию о типах динамического языка. Я переписываю последовательности операторов во вложенные letвыражения, например так: 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 => if x then {...
Правильный ли следующий пример о том, является ли алгоритм вывода правильным и полным ? Предположим, у нас есть стебли игл a, b, c в стоге сена, а также алгоритм вывода, предназначенный для поиска игл. звук - получаются только иглы a, b и c. завершено - иглы a, b и c получены. Другое сено также...
В дискуссии вокруг этого вопроса Жиль правильно упоминает, что любое доказательство правильности алгоритма, использующего массивы, должно доказывать, что нет доступа к массиву вне пределов; в зависимости от модели времени выполнения это может вызвать ошибку времени выполнения или доступ к...
Я попытался выполнить следующее упражнение, но застрял, пытаясь найти все критические пары . У меня есть следующие вопросы: Как мне узнать, какая критическая пара произвела новое правило? Как я узнал, что нашел все критические пары? Пусть где бинарный, унарный, а константа....
Относительно потока, Доказывающего, что преобразование из CNF в DNF является NP-Hard (и связанный математический поток ): Как насчет другого направления, от DNF до CNF? Это легко или сложно? На странице 2 этой статьи они, похоже, намекают на то, что оба направления одинаково трудны, когда говорят:...
По словам Питера Селинджера , Лямбда-исчисление алгебраическое (PDF). В начале этой статьи он говорит: Известно, что комбинаторная интерпретация лямбда-исчисления несовершенна, поскольку она не удовлетворяет правилу: при интерпретации не подразумевает (Barendregt, 1984).ξξξM=NM=NM =...
Я пытаюсь научить себя квантовым вычислениям, и у меня есть приличное понимание линейной алгебры. Я прошел через ворота НЕ, что было не так уж плохо, но затем я добрался до ворот Адамара. И я застрял. Главным образом потому, что, хотя я «понимаю» манипуляции, я не понимаю, что они на самом деле...
В частности, если я определил новый K2K2K_2 как K2=λx.(λy.y)K2=λx.(λy.y)K_2 = \lambda x. (\lambda y. y) вместо K=λx.(λy.x)K=λx.(λy.x)K = \lambda x. (\lambda y. x) будет ли {S,K2,I}{S,K2,I}\{S, K_2,I\} -счет вычисляться на основе конкуренции? Я предполагаю «нет» только потому, что я не могу...
Существуют ли языки программирования (или логика), которые могут реализовать (или выразить) функцию тогда и только тогда, когда f вычислимые биективные функции?f:N→Nf:N→Nf:\mathbb{N}\to...
При доказательстве теоремы разрешения обычно предполагается, что переменные в разных разделах различны. Это не то, что происходит автоматически; это требует значительного дополнительного кода и вычислений для реализации. Учитывая это, я ищу тестовый пример для него. Проблема в том, что во всех...