К чему я так подробно
расписывал получение свёртки для розы? Очевидно, что интуитивно получить её можно сразу. Так я обычно и делаю, воспользовавшись методом размерностей, пардон, программированием
"от типов". Возможно, так делаете и вы. Я хочу показать главный недостаток этого подхода - он неформален.
( Read more... )В данном конкретном случае нам очень сильно помогает Curry-Howard, но он не гарантирует уникальности доказательства (реализации), т.е. этот метод не формализуем. А вот на основе ТК, думаю, можно построить CataEval.
