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

[deniok]

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

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

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

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

Comments

[voidex.livejournal.com]

1.

uncurry (|||)

2.

(. Left) &&& (. Right)

[deni-ok.livejournal.com]

Стрелочник.