Магнитогорская группа пользователей Linux

Нашёл у Гейтинга [1] иллюстрацию к изоморфизму Карри-Ховарда. Что интересно: насколько я понял, эта иллюстрация была сформулирована до самого изоморфизма.

«Пусть A обозначает свойство натурального числа быть кратным 8, B — быть кратным 4, C — кратным 2. 8a мы можем записать как 4∙2a; благодаря этому математическому построению (P) мы видим, что свойство A влечёт свойство B, или A → B. Подобное построение (Q) показывает, что B → C. Употребляя сначала P, потом Q (суперпозиция P и Q), мы получаем 8a = 2∙(2∙2a), что доказывает A → C. Этот процесс остаётся пригодным, если вместо A, B, C мы подставим произвольные свойства. А именно, если построение P доказывает, что A → B, и построение Q доказывает, что B → C, то суперпозиция P и Q доказывает, что A → C».

Если считать «построения» функциями, то из этого рассуждения увидим, что существование операции суперпозиции двух функций (P и Q) доказывает транзитивность импликации:

(.) :: (b -> c) -> (a -> b) -> a -> c

[1] А. Гейтинг. Введение в интуиционизм. М.: Мир, 1965.