Простые задачки на Карри-Говарда

[deniok]

Доказать, используя Хаскель, что следующие тавтологии верны интуиционистски

(a -> c) /\ (b -> c) -> a \/ b -> c
(a \/ b -> c) -> (a -> c) /\ (b -> c)

(Понятно, что конъюнкция - это пара, а дизъюнкция - Either.)

UPD. Стоит напомнить, что изоморфизм Карри-Говарда имеет место между интуиционистской версией пропозициональной логики и подмножеством Хаскеля без рекурсии. То есть использовать рекурсию нельзя - ни явно, ни неявно. Ну и определение отрицания требует в Хаскелле некоторых хаков, но при доказательстве этих формул оно не требуется.

Comments

[juan-gandhi.livejournal.com]

Прелесть какая. А как это в Хаскеле "верность интуиционистски" вообще доказывается? Уж не написанием ли кода?

[deni-ok.livejournal.com]

Да, именно так. Но, конечно, на подмножестве Хаскеля без рекурсии , иначе система not sound: fix :: (a -> a) -> a.

[rvp74.livejournal.com]

для первого как-то сразу код в голову пришел:

ex1 :: (a -> c, b -> c) -> Either a b -> c
ex1 (f,g) = h where
   h (Left l) = f l
   h (Right r) = g r

[rvp74.livejournal.com]

второй почему-то сразу не дался, но решение оказалось еще проще:

ex2 :: (Either a b -> c) -> (a -> c, b -> c)
ex2 h = (h . Left, h . Right)

[voidex.livejournal.com]

1.

uncurry (|||)

2.

(. Left) &&& (. Right)

[sassa-nf.livejournal.com]

import Control.Arrow
f :: (a->c, b->c) -> Either a b -> c
f = uncurry (|||)

g :: (Either a b -> c) -> (a->c, b->c)
g = (.Left) &&& (.Right)

[gds.livejournal.com]

мой вариант:

Extraction Language Haskell.

Inductive Either A B := Left : A -> Either A B | Right : B -> Either A B.

Extraction Inline prod_rect.
Extraction Inline Either_rect.

Lemma l1 : forall a b c,
(a -> c) * (b -> c) -> Either a b -> c.
firstorder.
Defined.
Extraction l1.

Lemma l2 : forall a b c,
(Either a b -> c) -> (a -> c) * (b -> c).
firstorder.
Defined.
Extraction l2.

(результат в отдельной пасте, http://pastebin.com/H2T1cw7B , чтобы не спойлерить.)
(до канонiчного можно довести, указав, во что экстрактить Prod и Pair.)

[deni-ok.livejournal.com]

Стрелочник.

[deni-ok.livejournal.com]

Еще один стрелочник.

[migmit.livejournal.com]

И без рекурсивных типов в том числе.

[deni-ok.livejournal.com]

Да, data Mu f = In (f (Mu f)) и тому подобное тоже, конечно, все попортит.

[nponeccop.livejournal.com]

Ну, если быть педантичным, то и без unsafeCoerse, неполных кейсов и всяких странных констант вроде undefined, error, Control.Exception.throw и т. д.

Даже оговорка о Хиндли-Милнере будет неточна, потому что есть его версия с расширением имени Майкрофта, дающая рекурсию.

Проще уж написать маленький парсер с тайпчекером, и для него задания формулировать :) Чтобы никакая противоречивость уж точно не просочилась.

[deni-ok.livejournal.com]

Проще, конечно, было попросить сделать все на Агде, но это, боюсь, сузило бы аудиторию. И хотя Хаскель не заточен напрямую под доказательства, по факту все, кто тут сделал задачку, вполне себе ограничились допустимыми средствами.