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

При кодировании логики в ассистенте доказательства, таком как Coq или Isabelle, необходимо сделать выбор между использованием поверхностного и глубокого встраивания. При неглубоком встраивании логические формулы записываются непосредственно в логику доказательства теоремы, тогда как при глубоком...

Я перебираю примечания к курсу на CIS 500: основы программного обеспечения и упражнения - это очень весело. Я только на третьем упражнении, но я хотел бы узнать больше о том, что происходит, когда я использую тактику, чтобы доказать такие вещи, какforall (n m : nat), n + n = m + m -> n =...

Coq имеет тип Prop несущественных доказательств, которые отбрасываются при извлечении. Какова причина этого, если мы используем Coq только для доказательств? Prop является непредсказуемым, поэтому Prop: Prop, однако, Coq автоматически выводит индексы юниверса, и мы можем использовать Type (i)...

Я наткнулся на противоречивое разногласие между Агдой и Коком, которое, очевидно, не связано с наиболее известными различиями между их теориями типов (например, (im) предсказуемость, индукция-рекурсия и т. Д.). В частности, Агда принимает следующее определение: data Ty : Set0 -> Set0 where c1 :...

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

Я видел (и слышал), что он утверждал, что безопасно добавить классическую аксиому исключенного среднего к Coq, но я не могу найти документ, подтверждающий это утверждение. Статьи, которые я вижу в списке в вики Coq о исключенной середине, показывают несоответствие с нечетким множеством....

Есть ли способ доказать следующую теорему в Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. РЕДАКТИРОВАТЬ : Попытка дать краткое объяснение «что такое доказательство неуместности» (поправьте меня, если я ошибаюсь или неточен) Основная идея заключается в том, что в мире...

Coq, Agda и Idris имеют бесконечную иерархию типов (Тип 1: Тип 2: Тип 3: ...). Но почему бы не сделать это, как λC, систему в лямбда-кубе, которая ближе всего к исчислению конструкций и имеет только два , ∗** и , и эти правила?◽◽◽ ∅⊢∗:◽∅⊢∗:◽\frac {} {∅ ⊢ * : ◽}...

Мы часто хотим определить объект соответствии с некоторыми правилами вывода. Эти правила обозначают производящую функцию F , которая, когда она монотонна, возвращающую мере неподвижную точку М F . Возьму А : = μ F , чтобы быть «индуктивным определением» А . Кроме того, монотонность F позволяет нам...

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

Я искал формализацию теоремы компактности для FOL, но не нашел. Кто-нибудь знает о таком развитии или связанной

Как я могу убедить Coq, что приведенная ниже рекурсивная функция завершается? Функция принимает два индуктивных аргумента. Интуитивно понятно, что рекурсия завершается, потому что любой аргумент разлагается. В частности, функция принимает два дерева в качестве входных данных. Inductive Tree := |...

Семантика большого подмножества OCaml, называемого OCamllight , была формализована в HOL Оуэнсом несколько лет назад. Совсем недавно теоретическая семантика типов меньшего подмножества OCaml была реализована в Nuprl Крейцем, Хейденом и Хикки . Есть ли похожие разработки в...

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

Я программирую уже несколько лет, но очень незнаком с теоретической CS. Недавно я пытался изучать языки программирования и, как часть этого, проверку типов и вывод. Мой вопрос заключается в том, что если я пытаюсь написать программу для вывода и проверки типов для языка программирования, и я хочу...

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

Мне было интересно, может ли порядок объявлений индуктивного типа иметь значение. Например, в Coq вы можете определить Natлибо: Inductive Nat := | O : Nat | S : Nat -> Nat. или Inductive Nat := | S : Nat -> Nat | O : Nat. Возможно, это изменит порядок параметров в автоматически...