Нашёл у Гейтинга [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.
Подписаться на:
Комментарии к сообщению (Atom)
По теме поста мне сказать нечего, но есть зато вопрос: как удалось вставить в пост математические символы? Я нашёл тут какой-то вебсервис, который по запросу конвертит латеховский код в картинки. А здесь как это сделано?
ОтветитьУдалитьЭто обычные юникодные символы. Можно, например, из таблицы символов их копировать. Я ввожу с помощью XCompose. Про него написано, например, здесь: http://sovety.blogspot.com/2008/02/compose.html.
ОтветитьУдалить