Описание тега curry-howard
Соответствие Карри – Ховарда - это прямая связь между компьютерными программами и доказательствами в теории языков программирования и теории доказательств.
1
ответ
Что такое "окольное доказательство" в "Предложениях как типы" П. Вадлера?
В предложениях как типы написано: В 1935 году, в возрасте 25 лет, Генцен15 ввел не одну, а две новые формулировки логики - естественное дедукция и последовательное исчисление - которые утвердились как две основные системы для формулировки логики и о…
22 янв '16 в 10:57
1
ответ
Есть ли функция Scala типа `Nothing => A`? Или как его построить?
Сквозь карри-ховардский изоморфизм Скалы Unit соответствует логической истине и Nothing к логическому ложному. Факт, что логическая истина подразумевается чем-либо, засвидетельствован простой функцией, которая просто отбрасывает аргумент: def toUnit…
24 ноя '12 в 09:46
1
ответ
Как кодировать аксиому выбора в Haskell/ Функциональное программирование?
> {-# LANGUAGE RankNTypes #-} Мне было интересно, есть ли способ представить аксиому выбора в Haskell и / или некотором другом функциональном языке программирования. Как мы знаем, false представлен типом без значений (Void в хаскеле). > import…
06 дек '15 в 02:33
6
ответов
Для чего нужна абсурдная функция в Data.Void?
absurd функция в Data.Void имеет следующую подпись, где Void логически необитаемый тип, экспортируемый этим пакетом: -- | Since 'Void' values logically don't exist, this witnesses the logical -- reasoning tool of \"ex falso quodlibet\". absurd :: Vo…
03 янв '13 в 01:25
2
ответа
Можно ли использовать GADT для доказательства неравенства типов в GHC?
Итак, в моих текущих попытках наполовину понять Карри-Ховарда с помощью небольших упражнений на Хаскелле, я застрял в этой точке: {-# LANGUAGE GADTs #-} import Data.Void type Not a = a -> Void -- | The type of type equality proofs, which can only…
11 янв '13 в 06:58
2
ответа
Как доказать принцип взрыва (ex falso sequitur quodlibet) в Scala?
Как мне показать, что что-либо следует из значения типа без конструкторов в Scala? Я хотел бы сделать сопоставление с шаблоном для значения и сделать так, чтобы Scala сообщала мне, что ни один шаблон не может соответствовать, но я открыт для других …
22 окт '18 в 21:15
1
ответ
Последствия как функции в Coq?
Я читал, что последствия являются функциями. Но мне трудно понять пример, приведенный на вышеупомянутой странице: Термин доказательства для импликации P → Q - это функция, которая принимает доказательства для P в качестве входных данных и выдает док…
26 сен '15 в 16:53
0
ответов
Карри-Говард для синтеза терминов в Изабель
Скажем, я доказал некоторые основные положения интуиционистской логики высказываний в Изабель /HOL: theorem ‹(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))› proof - { assume ‹A ⟶ B› { assume ‹B ⟶ C› { assume ‹A› with ‹A ⟶ B› have ‹B› by (rule mp) with ‹B ⟶ C› have ‹…
15 ноя '18 в 13:28
1
ответ
Практические примеры использования Void
Редактировать: По VoidЯ имею ввиду Хаскелла Void тип, т.е. пустой тип, который не может иметь значения, но undefined, Существует постоянная дискуссия о Swift Evolution о том, стоит ли заменить noreturn атрибут функции с фактическим Void тип. Для это…
24 июн '16 в 13:13
3
ответа
Для чего еще можно использовать функцию `loeb`?
Я пытаюсь понять "Löb and möb: странные петли в Хаскеле", но сейчас значение от меня ускользает, я просто не понимаю, почему это может быть полезно. Просто чтобы вспомнить функцию loeb определяется как loeb :: Functor f => f (f a -> a) -> f…
16 мар '14 в 17:07
1
ответ
Не смог вывести SingI предшественника Nat
Я пытаюсь написать weaken функция для конечных множеств целых чисел. Я использую singletons пакет. Я определил и продвинул функции сложения, вычитания и предшественника, а также доказал некоторые уравнения для них, чтобы помочь при проверке типов. Н…
02 сен '16 в 13:00
6
ответов
Зависимые типы: как тип зависимой пары аналогичен дизъюнктному объединению?
Я изучал зависимые типы, и я понимаю следующее: Почему универсальное количественное представление представляется как зависимый тип функции. ∀(x:A).B(x) означает "для всех" x типа A есть значение типа B(x) " Следовательно, он представлен как функция,…
24 окт '14 в 06:02
2
ответа
Законы де Моргана в Хаскеле через переписку Карри-Ховарда
Я реализовал три из четырех законов Де Моргана в Хаскеле: notAandNotB :: (a -> c, b -> c) -> Either a b -> c notAandNotB (f, g) (Left x) = f x notAandNotB (f, g) (Right y) = g y notAorB :: (Either a b -> c) -> (a -> c, b -> c…
04 май '16 в 00:47
1
ответ
Как или это возможно доказать или фальсифицировать `forall (P Q: Prop), (P -> Q) -> (Q -> P) -> P = Q` в Coq?
Я хочу доказать или фальсифицировать forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q. в Coq. Вот мой подход. Inductive True2 : Prop := | One : True2 | Two : True2. Lemma True_has_one : forall (t0 t1 : True), t0 = t1. Proof. intros. de…
26 окт '14 в 10:39
10
ответов
Какие наиболее интересные эквивалентности вытекают из изоморфизма Карри-Ховарда?
Я столкнулся с изоморфизмом Карри-Ховарда относительно поздно в моей жизни программиста, и, возможно, это способствует тому, что он меня полностью очаровывает. Это подразумевает, что для каждой концепции программирования существует точный аналог в ф…
03 июн '10 в 19:31
2
ответа
Карри Говард соответствие и равенство
Некоторое время назад я прочитал, что тип функции a -> b соответствует отношению a ≤ b, либо это a ≥ b? Это имеет смысл для меня, потому что два типа изоморфны, если между ними есть биекция (т.е. (a ≈ b) ≡ (a -> b, b -> a)). Так же, (a = b)…
22 дек '15 в 03:37
1
ответ
Что является эквивалентом ошибки изоморфизма Карри-Ховарда?
Проще говоря, соответствие Карри-Говарда утверждает, что тип является теоремой и что программа, возвращающая этот тип, является доказательством соответствующей теоремы. Соответствие основано на формализации математических доказательств в таких языка…
24 фев '17 в 16:37
1
ответ
Использование карри Говарда для статической проверки того, что два типа не равны в Scala
Поэтому я недавно прочитал следующий пост: http://www.chuusai.com/2011/06/09/scala-union-types-curry-howard/ И я действительно оценил подход! Я пытаюсь сделать функцию def neq[A,B] = ... Где neq[String, String] не будет компилироваться, но neq[Strin…
11 июл '14 в 04:15
4
ответа
Построение эффективных экземпляров монады в `Set` (и других контейнерах с ограничениями) с использованием монады продолжения
Setаналогично [] имеет четко определенные монадические операции. Проблема в том, что они требуют, чтобы значения удовлетворяли Ord ограничение, и поэтому невозможно определить return а также >>= без каких-либо ограничений. Та же проблема относ…
29 авг '12 в 17:49
3
ответа
Изоморфизм Карри-Говарда
Я искал в Интернете, и я не могу найти никаких объяснений ОМС, которые бы быстро не переросли в лекцию по теории логики, которая резко у меня над головой. (Эти люди говорят так, как будто "исчисление интуиционистских высказываний" - это фраза, котор…
18 апр '12 в 15:24