Непостоянство

Помню, в детстве меня очень впечатлила заметка про тибетских монахов, которые много дней строят из цветного песка сложное изображение (мандалу),





а потом, едва закончив, быстро ее разрушают, демонстрируя непостоянство всего обусловленного. Вчера и я себя почувствовал таким монахом: написал длинный пост, хотел добавить один штрих, переключился из режима HTML в визуальный, затем обратно, а из-за ошибки разбора разметки мне ЖЖ большую часть текста выкинул (тут же сохранив новый вариант в черновик). Придется еще раз писать, будет мне урок.

Propositional Calculus

Для многих моих френдов описанное в этом посте - детский сад, поэтому они могут смело пропустить текст и просто полюбоваться фотографией типизированной лямбды в конце. Я же с данной темой познакомился недавно, мне было интересно, возможно кому-то еще будет тоже. Недавно я писал про логику высказываний и ее параллели в программировании. Но там связи этих двух областей были неформальные, на уровне аналогий. Оказывается, до их формализации был всего один шаг.

Пусть мы оперируем некоторыми высказываниями A,B,C и т.д. Пусть у нас есть доказательство a достоверности высказывания А. Этот факт будем обозначать как a : А.

( Read more... )

( Read more... )