deniok: (typed lambda)
deniok ([personal profile] deniok) wrote2014-10-05 09:23 am

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

Доказать, используя Хаскель, что следующие тавтологии верны интуиционистски
(a -> c) /\ (b -> c) -> a \/ b -> c
(a \/ b -> c) -> (a -> c) /\ (b -> c)
(Понятно, что конъюнкция - это пара, а дизъюнкция - Either.)

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

Post a comment in response:

This account has disabled anonymous posting.
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting