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

[deniok]

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

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

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

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

Comments

[deni-ok.livejournal.com]

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

[nponeccop.livejournal.com]

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

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

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

[deni-ok.livejournal.com]

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