неділя, 2 вересня 2012 р.

Почему вместо exist пишут forall?

А вот почему...
Читал  сегодня про экзистенциальные типы. Там автор пишет, что мол нам надо 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 с реализациями зависимого произведения и дополнительных функций.

Немає коментарів:

Дописати коментар