Хорошо известно, что комбинаторы S и K образуют базис для исчисления комбинаторов в том смысле, что все другие комбинаторы могут быть выражены через них. Существует также базис Карри B, C, K, W, который обладает тем же свойством. Таких баз должно быть бесконечное количество, но я не знаю других....
У нас есть логика Хоара. Почему все еще возможно, что алгоритм верен, но нет никаких доказательств того, что он верен? Предположим, что алгоритм выражен в C. Тогда мы можем шаг за шагом утверждать, что он делает то, что должен делать. Итак, мой вопрос: Приведите мне пример алгоритма, который...
Я знаю немного теории зависимых типов. Из википедии: Зависимый тип - это тип, определение которого зависит от значения. И из моего курса теории типов я вспоминаю, что зависимый тип: Семейство типов, проиндексированных по типу. Но у меня путаница в отношении зависимых типов, типов уточнения и логики...
Разрешены ли проблемы типа «посещение вечеринки» в Прологе? Например: Лопух Малдун и Карлотта Пинкстоун сказали, что придут, если придет Альбус Дамблдор. Альбус Дамблдор и Дейзи Доддридж оба сказали, что придут, если придет Карлотта Пинкстоун. Альбус Дамблдор, Бердок Малдун и Карлотта Пинкстоун...
Я начал читать все больше и больше статей по языковым исследованиям. Я нахожу это очень интересным и хорошим способом узнать больше о программировании в целом. Тем не менее, как правило , приходит раздел , где я всегда борюсь с (Возьмем, например , части третьей этой ) , так как мне не хватает...
Кто-нибудь когда-либо писал систему (программное обеспечение или подробное объяснение на бумаге с простыми примерами), которая генерирует компьютерные программы? Я ввожу и он создает программу, которая перечисляет простые числа меньше 10. P r i m e ( x ) просто определяется как 1 < x ∧ ∄ Aпг я м...
xorворота, теперь мне нужно построить эти ворота, используя только 4 nandворот a b out 0 0 0 0 1 1 1 0 1 1 1 0 the xor = (a and not b) or (not a and b), который является A¯¯¯¯B+AB¯¯¯¯A¯B+AB¯\begin{split}\overline{A}{B}+{A}\overline{B}\end{split} Я знаю ответ, но как получить диаграмму ворот из...
Я сам изучаю Автоматизированное доказательство теорем / SMT-решатели / Помощники по проверке и выкладываю серию вопросов о процессе, начиная здесь . Я продолжаю читать об Алгоритме Объединения . Что это такое и почему это так важно для двигателей вывода ? Почему это так важно для информатики?...
Я пытался придумать систему, которая оценивала бы устав организации для определения их базовой логики. Я думаю, что система предикатов первого порядка будет работать для представления правил, которые могут быть переведены из текста с помощью тегов части речи и других методов НЛП. Существует ли...
Я сам изучаю Автоматизированное доказательство теорем / SMT-решатели / Помощники по проверке и выкладываю серию вопросов о процессе, начиная здесь . Почему автоматические средства проверки теорем, то есть ACL2 , и решатели SMT не нуждаются в помощи человека, в то время как помощники по...
Y комбинатор имеет тип . Согласно соответствию Карри-Говарда, поскольку тип является обитаемым, он должен соответствовать истинной теореме. Однако всегда истинно, поэтому кажется, что тип Y-комбинатора соответствует теореме , что не всегда верно. Как это может быть?( a → a ) → a(a→a)→a(a...
Я самообучающийся помощник по доказательствам и решил начать с некоторых базовых доказательств и продолжить работу. Поскольку доказательства основаны на других доказательствах и поэтому образуют иерархию, существует ли хранилище иерархии доказательств? Я знаю, что могу выбрать конкретного помощника...
Я работаю над компилятором для конкатенативного языка и хотел бы добавить поддержку вывода типов. Я понимаю Хиндли-Милнера, но я изучаю теорию типов по ходу дела, поэтому не знаю, как ее адаптировать. Является ли следующая система надежной и достоверной? Термин - это литерал, композиция терминов,...
Я пытаюсь обернуть голову вокруг доказательства полноты NP, которое, кажется, вращается вокруг SAT / 3CNF-SAT. Возможно, это поздний час, но я боюсь, что не могу придумать формулу 3CNF, которая не может быть удовлетворена (возможно, я упускаю что-то очевидное). Можете ли вы привести пример такой...
Аппликативный порядок: всегда полностью оценивайте аргументы функции перед оценкой самой функции, например: (λx.x2(λx.(x+1) 2)))→(λx.x2(2+1))→ (λx.x2(3))→ 32 → 9(λx.x2(λx.(x+1) 2)))→(λx.x2(2+1))→ (λx.x2(3))→ 32 → 9(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x....
Вот контекст ( Структура и интерпретация компьютерных программ , раздел 1.1.8, под заголовком «Локальные имена»): Формальный параметр процедуры играет особую роль в определении процедуры, поскольку не имеет значения, какое имя имеет формальный параметр. Такое имя называется связанной переменной , и...
Я могу понять важность того, что компьютерные ученые или любые инженеры, связанные с разработкой программного обеспечения, должны были понимать основы логики как основу. Но есть ли какие-либо задачи / задания, которые явно требуют знания об этом, кроме задач, которые требуют какого-либо...
Я программист с автоматом, но не с логикой. Я читал в газетах, что они очень тесно связаны. Детерминированные конечные автоматы (DFA), древовидные автоматы и автоматы видимого нажатия - все они связаны с монадической логикой второго порядка (MSO). Хотя, я понимаю, что автоматы и люди (в статьях)...
Предположим, у нас есть простой язык, который состоит из терминов: truetrue\mathtt{true} falsefalse\mathtt{false} если являются терминами, тоt1,t2,t3t1,t2,t3t_1,t_2,t_3ift1thent2elset3ift1thent2elset3\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 Теперь предположим следующие...
Я думал о доказательствах и столкнулся с интересным наблюдением. Таким образом, доказательства эквивалентны программам через изоморфизм Карри-Говарда, а круговые доказательства соответствуют бесконечной рекурсии. Но из проблемы остановки мы знаем, что в общем случае проверка того, будет ли...