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

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

Упражнение на вывод типов: вывод какой тавтологии пропозициональной логики я строю в исчислении секвенций?

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 25th, 2017 02:53 pm
Powered by Dreamwidth Studios