А вот почему...
Читал сегодня про экзистенциальные типы. Там автор пишет, что мол нам надо exist, а мы пишем forall, но они эквивалентны и это легко доказывается. Но доказательства автор не привел, а поскольку я сижу сейчас на интуиционистской логике и Агде, решил доказать, и поскольку доказательство ну очень простое решил, что все должны его знать.
Значит есть у нас такое:
F : Set → Set
T : Set
C₁ : (∃ α. F α) → T
C₂ : ∀ α. (F α → T)
Set ─ это так обозначается множество типов. Нужно доказать, что C₁ и C₂ эквивалентны. Докажем это в смысле, что с C₁ можно получить C₂, и наоборот, то есть:
(Exist → Forall) ∧ (Forall → Exist)
где:
Exist = (∃ α. F α) → T
Forall = ∀ α. (F α → T)
∀ представим в типизированном лямбда исчислении следующим образом:
Forall = (α : Set) → F α → T
Но для ∃ ничего подобного нету. Но что значит существование в интуиционистской логике? Если утверждаешь существование чего-то, предъяви это. То есть, например, доказательством ∃ x. x>1 может быть число 3 и доказательство, что 3>1. А на языке типизированного лямбда исчисления это есть ни что иное как зависимое произведение, то есть произведение в котором тип второго элемента зависит от значения первого.
Итак в Agda то, что нам надо, запишется так:
Exist = Σ[ α ∶ Set ] F α → T
Forall = (α : Set) → F α → T
где Σ[ α ∶ Set ] F α ─ это тип с двух элементов: первый имеет тип Set, а второй тип F α, где α ─ значение первого элемента.
Что мы тут имеем? Два типа функций от двух аргументов, причем отличаются лишь тем, что первый вариант некаррированный, а второй каррированный. По-этому доказательство следующее (мы помним, что логическое "и" в нашей интерпретации ─ это тоже произведение):
Exist≡Forall : (Exist → Forall) × (Forall → Exist)
Exist≡Forall = curry , uncurry
Тут curry и uncurry ─ функции со стандартной библиотеки. Это ─ подсвеченная библиотека Product с реализациями зависимого произведения и дополнительных функций.
Читал сегодня про экзистенциальные типы. Там автор пишет, что мол нам надо exist, а мы пишем forall, но они эквивалентны и это легко доказывается. Но доказательства автор не привел, а поскольку я сижу сейчас на интуиционистской логике и Агде, решил доказать, и поскольку доказательство ну очень простое решил, что все должны его знать.
Значит есть у нас такое:
F : Set → Set
T : Set
C₁ : (∃ α. F α) → T
C₂ : ∀ α. (F α → T)
Set ─ это так обозначается множество типов. Нужно доказать, что C₁ и C₂ эквивалентны. Докажем это в смысле, что с C₁ можно получить C₂, и наоборот, то есть:
(Exist → Forall) ∧ (Forall → Exist)
где:
Exist = (∃ α. F α) → T
Forall = ∀ α. (F α → T)
∀ представим в типизированном лямбда исчислении следующим образом:
Forall = (α : Set) → F α → T
Но для ∃ ничего подобного нету. Но что значит существование в интуиционистской логике? Если утверждаешь существование чего-то, предъяви это. То есть, например, доказательством ∃ x. x>1 может быть число 3 и доказательство, что 3>1. А на языке типизированного лямбда исчисления это есть ни что иное как зависимое произведение, то есть произведение в котором тип второго элемента зависит от значения первого.
Итак в Agda то, что нам надо, запишется так:
Exist = Σ[ α ∶ Set ] F α → T
Forall = (α : Set) → F α → T
где Σ[ α ∶ Set ] F α ─ это тип с двух элементов: первый имеет тип Set, а второй тип F α, где α ─ значение первого элемента.
Что мы тут имеем? Два типа функций от двух аргументов, причем отличаются лишь тем, что первый вариант некаррированный, а второй каррированный. По-этому доказательство следующее (мы помним, что логическое "и" в нашей интерпретации ─ это тоже произведение):
Exist≡Forall : (Exist → Forall) × (Forall → Exist)
Exist≡Forall = curry , uncurry
Тут curry и uncurry ─ функции со стандартной библиотеки. Это ─ подсвеченная библиотека Product с реализациями зависимого произведения и дополнительных функций.
Немає коментарів:
Дописати коментар