![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Простые задачки на Карри-Говарда
Oct. 5th, 2014 09:23 amДоказать, используя Хаскель, что следующие тавтологии верны интуиционистски
UPD. Стоит напомнить, что изоморфизм Карри-Говарда имеет место между интуиционистской версией пропозициональной логики и подмножеством Хаскеля без рекурсии. То есть использовать рекурсию нельзя - ни явно, ни неявно. Ну и определение отрицания требует в Хаскелле некоторых хаков, но при доказательстве этих формул оно не требуется.
(a -> c) /\ (b -> c) -> a \/ b -> c (a \/ b -> c) -> (a -> c) /\ (b -> c)(Понятно, что конъюнкция - это пара, а дизъюнкция - Either.)
UPD. Стоит напомнить, что изоморфизм Карри-Говарда имеет место между интуиционистской версией пропозициональной логики и подмножеством Хаскеля без рекурсии. То есть использовать рекурсию нельзя - ни явно, ни неявно. Ну и определение отрицания требует в Хаскелле некоторых хаков, но при доказательстве этих формул оно не требуется.
