Почему мы не рассматриваем религию как императив симуляции? Именно по той причине, что она является развитым семиотическим явлением с художественными образами и индивидуальной рефлексией. В любой монотеистической религии каждое явление - это знак, указывающий на Бога (в качестве примера приведем сакраментальную фразу - «каждая березка указывает на
(
Read more... )
Вспомнился "изоморфизм Карри-Ховарда", о том, что компьютерные программы имеют ту же структуру, что и математические доказательства. Ту же самую структуру имеют физические процессы и что-то из топологии. (В общем-то, это просто категории из теории категорий - категория это что угодно с точками и стрелочками; категории типа этих четырех это "closed symmetric monoidal category")
Все и так знают, что доказательство это процесс перехода от одних утверждений к другим, например: "Любой епископский осел бежит, и Брунеллус - осел => Брунелуус бежит". Доказательство ложности чего-то это доказательство "Что-то => False": если из утверждения можно вывести Ложь, оно - ложно. Из ложного утверждения можно вывести все угодно: "forall a, False => a"; соответственно, ложность чего-то можно еще и сформулировать как "forall a, Что-то => a", если из чего-то можно вывести все что угодно, то оно - ложно. Для сравнения, любое истинное утверждение можно вывести из любого (даже из ложного).
Компьютерная программа это функция из одного множества в другое. Эти множества называются "типами". Иногда, если знать только типы, можно догадаться, или доказать, что программа делает (например, программа из множества слов в множество чисел (Слово -> Число), если она не тривиальна, конечно, скорее всего что-то считает: количество букв, или гласных, или мягких знаков?). Эти догадки называются, кстати, "Theorems for free". Лжи соответствует "пустой тип", или bottom, с обозначением _|_. Почему для любого типа "а" существует программа "_|_ -> a"? Т.к. пустое множество не содержит элементов, "f :: _|_ -> a" тривиальна - ее даже не надо придумывать. Аналогично, "g :: a -> _|_" может существовать тогда и только тогда, когда и a не содержит элементов (если в a есть элемент x, то g(x) принадлежит _|_, что невозможно). Что-то типа того. "Истинные" типы, то есть типы у которых есть значения, можно легко вывести из любого другого типа, просто проигнорировав этот тип и подставив одно из значений типа результата: функция f(x) = 3 это функция из любого типа в Числа.
Возможно, категория тварей Божьих тоже похожа на эти штуки. Творец - Истина; все что угодно "указывает" на Творца (forall a, a => True); дьявол "указывает" на все что угодно (forall b, False => b); если что-то указывает на все что угодно, оно относится к дьяволу; если что-то указывает на Бога, оно к указанию на него дьяволом равнодушно. У меня есть какое-то интуитивное понимание того, что это "указание" здесь может значить, но уточнить его у меня не выходит. Скорее всего, я просто брежу. Надеюсь, это все равно было интересно.
Reply
Reply
Leave a comment