Визуальное логическое исчисление
языка ДРАКОНОпубликовано на стр. 427-435 книги
Паронджанов В.Д. Учись писать, читать и понимать алгоритмы. Алгоритмы для правильного мышления. Основы алгоритмизации. — М.: ДМК Пресс, 2012, 2014, 2016. — 520 с. — Иллюстраций 272. Глава 34. Исчисление иконЦитата:
Для кого предназначены главы 34, 35 и 36?
Данный материал предназначен не для начинающих, а для профессионалов, которые хотят познакомиться с теоретическим фундаментом языка ДРАКОН.
Если же вы только начинаете изучать язык ДРАКОН, если ваша
цель – научиться рисовать дракон-схемы и пользоваться программой «дракон-конструктор», вам не стоит тратить время и читать главы 34, 35 и 36.
§1. ВВЕДЕНИЕГлава посвящена исследованию связи языка ДРАКОН и математической логики. Мы покажем, что:
• графический синтаксис языка ДРАКОН опирается на идеи математической логики;
• исчисление икон – это раздел математической логики;
• внутренние алгоритмы дракон-конструктора реализуют исчисление икон, то есть опираются на положения математической логики;
• математическую логику можно рассматривать как одно из теоретических оснований языка ДРАКОН.
§2. ШАМПУР-СХЕМАЦитата:
Шампур-схема – абстрактная дракон-схема. Подчеркнем,
что шампур-схема по определению является абстрактной,
то есть полностью лишенной текста.
§3. ВИЗУАЛЬНОЕ ЛОГИЧЕСКОЕ ИСЧИСЛЕНИЕПопытаемся взглянуть на графический (визуальный) синтаксис языка ДРАКОН с позиций математической логики. Нашему взору откроется необычная картина.
Оказывается, любая абстрактная дракон-схема (шампур-схема) представляет собой теорему, которая строго выводится (доказывается) из двух аксиом, каковыми являются заготовка-примитив и заготовка-силуэт.
Цитата:
– Какие же это аксиомы? – вправе удивиться читатель.
– Ведь это просто картинки-слепыши! А шампур-схемы вовсе не похожи на теоремы! Кто и зачем их должен доказывать? Наверно, это шутка или метафора.
Цитата:
– Вовсе нет, отнюдь не метафора. Ниже будет показано, что визуальный синтаксис ДРАКОНа построен как логическое
исчисление (назовем его «исчисление икон»). Данное исчисление можно рассматривать как раздел визуальной математической логики.
Последнее понятие не является традиционным. Математическая логика и ее основные понятия (исчисление, логический вывод и т. д.) сформировались в рамках текстовой парадигмы. В данной главе, по-видимому, впервые вводятся визуальные аналоги этих понятий. И на их основе строится исчисление икон.
§4. ОБЩЕИЗВЕСТНЫЕ СВЕДЕНИЯ О МАТЕМАТИЧЕСКОЙ
ЛОГИКЕПринципиальным достижением математической логики является разработка современного аксиоматического метода, который характеризуется тремя чертами:
• явной формулировкой исходных положений (аксиом) развиваемой теории (формальной системы);
• явной формулировкой правил логического вывода, с помощью которых из аксиом выводятся теоремы теории;
• использованием формальных языков для изложения теорем рассматриваемой теории [1].
Основным объектом изучения в математической логике являются логические исчисления. В понятие исчисления входят:
а) формальный язык, который задается с помощью алфавита и синтаксиса,
б) аксиомы,
в) правила вывода [1].
Таким образом, исчисление позволяет, зная аксиомы и правила вывода, получить (то есть вывести, доказать) все теоремы теории. Причем теоремы, как и аксиомы, записываются на формальном языке.
Напомним, что в рамках математической логики следующие термины можно рассматривать как синонимы:
• логическое исчисление,
• формальная система
• теория.
Следовательно, теоремы исчисления, теоремы формальной системы и теоремы теории – одно и то же.
§5. ОБ ОДНОМ РАСПРОСТРАНЕННОМ ЗАБЛУЖДЕНИИСуществуют два подхода к формализации человеческих знаний: визуальный и текстовый. С этой проблемой связано любопытное противоречие.
С одной стороны, преимущество графики перед текстом для человеческого восприятия считается общепризнанным.
Человеческий мозг в основном ориентирован на визуальное восприятие, и люди получают информацию при рассмотрении графических образов быстрее, чем при чтении текста.
Игорь Вельбицкий справедливо указывает:
Цитата:
«Текст – наиболее общая и наименее информативная в
смысле наглядности и скорости восприятия форма представления информации», а чертеж – «наиболее развитая
интегрированная форма представления знаний» [2].
С другой стороны, теоретическая разработка принципов визуальной формализации знаний все еще не развернута в должной мере.
Причину отставания следует искать в истории науки, в частности в особенностях развития математики и логики.
В этих дисциплинах с давних пор (иногда явно, чаще неявно) предполагалось, что результаты математической и логической формализации знаний в подавляющем большинстве случаев должны иметь форму текста (а не чертежа, не изображения).
Например, Стефен Клини пишет:
Цитата:
«Будучи формализованной, теория по своей структуре является уже не системой осмысленных предложений, а системой фраз, рассматриваемых как последовательность слов, которые, в свою очередь, являются последовательностями букв...
В символическом языке символы будут обычно соответствовать
целым словам, а не буквам, а последовательности символов,
соответствующие фразам, будут называться «формулами»...
Теория доказательств... предполагает... построение произвольно длинных последовательностей символов» [3].
Из этих рассуждений видно, что Клини (как и многие другие авторы) ставит в центр исследования проблему текстовой формализации и полностью упускает из виду всю совокупность проблем, связанных с визуальной формализацией.
Анализ литературы, посвященной данной теме, показывает, что большинство ученых исходит из неявного предположения, что научное знание – это, прежде всего, «текстовое» знание.
Они полагают, что наиболее адекватной (или даже единственно возможной) формой для представления результатов научного исследования является последовательность формализованных и неформализованных фраз. То есть текст (а отнюдь не
графические, визуальные образы).
Цитата:
Вопреки этому мнению, язык ДРАКОН опирается не
на текстовую, а на визуальную формализацию знаний.
Визуальный синтаксис языка ДРАКОН является не текстовым, а формальным визуальным объектом.
Таким образом, упомянутые выше ученые защищают ошибочную точку зрения, которую можно охарактеризовать как «принцип абсолютизации текста».
§6. ПРИНЦИП АБСОЛЮТИЗАЦИИ ТЕКСТАСуть его можно выразить, например, в форме следующих рассуждений.
Цитата:
Прогресс науки обеспечивается успехами логико-математической формализации и разработкой новых научных понятий и принципов, а не усовершенствованием рисунков.
Формулы и слова выражают сущность научной мысли.
Рисунки – это всего лишь иллюстрации к научному тексту. Они
облегчают понимание уже готовой, сформированной научной мысли, но не участвуют в ее формировании.
Короче говоря, язык науки – это формулы и предложения, но никак не картинки.
В науке есть суть, сердцевина, от которой зависит успех научно-
го творчества и получение новых научных результатов. Она выражается логико-математическими формализмами, научными понятиями и суждениями, выраженными в словах.
И есть вспомогательные задачи – обучение новичков, обмен ин-
формацией между учеными. Здесь-то и помогают картинки, облегчая взаимопонимание.
Кроме того, рисунки имеют необязательную, свободную и нестрогую форму, их невозможно формализовать. Поэтому формализация научного знания несовместима с использованием рисунков.
Таким образом, рисунки и чертежи есть нечто внешнее по от-
ношению к науке. Совершенствование языка рисунков и научный прогресс – разные вещи, они не связаны между собой.
Существует ряд работ, косвенным образом доказывающих, что принцип абсолютизации текста является ошибочным и вредным [4, 5 и др.].
Сегодня все больше ученых приходит к выводу, что визуальную формализацию знаний нельзя рассматривать как нечто второстепенное для научного познания, поскольку она входит в саму ткань мысленного процесса ученого и «может опосредовать самые глубинные, творческие шаги научного познания» [4].
Вместе с тем в математической логике визуальные методы, насколько нам известно, пока еще не нашли широкого применения. Иными словами, математическая логика по сей день остается оплотом текстового мышления и текстовых методов формализации знаний.
Это обстоятельство играет отрицательную роль, мешая поставить последнюю точку в доказательстве ошибочности «принципа абсолютизации текста».
Далее мы попытаемся на частном примере исчисления икон продемонстрировать принципиальную возможность визуализации, по крайней мере, некоторых разделов или, скажем аккуратнее, вопросов математической логики.
§7. ВИЗУАЛИЗАЦИЯ ПОНЯТИЙ МАТЕМАТИЧЕСКОЙ ЛОГИКИНам понадобится определение двух понятий:
• визуальный логический вывод (для краткости – видеовывод);
• визуальное логическое исчисление (для краткости – видеоисчисление).
Чтобы облегчить изучение материала, используем метод «очной
ставки». Поместим в левой графе таблицы 1 хорошо известное «текстовое» понятие. А в правой – определение нового, визуального понятия.
Таблица 1Определение понятия «логический вывод»Вывод в исчислении V есть последовательность C1, ... Cn формул, такая, что для любого i формула Ci
есть:
• либо аксиома исчисления V;
• либо непосредственное следствие предыдущих формул по
одному из правил вывода.
Формула Cn называется теоремой исчисления V, если существует
вывод в V, в котором последней формулой является Cn [6].
Определение понятия «видеовывод» (визуальный логический вывод)Видеовывод в видеоисчислении V есть последовательность C1, ... Cn видеоформул, такая, что для любого i видеоформула Ci
есть:
•либо видеоаксиома видеоисчисления V;
• либо непосредственное следствие предыдущих видеоформул
по одному из правил видеовывода.
Видеоформула Cn называется видеотеоремой видеоисчисления V, если существует видеовывод в V, в котором последней видеоформулой является Cn.
Нетрудно заметить, что новое определение (справа) почти дословно совпадает с классическим (слева). Разница состоит лишь в добавлении приставки «видео».
Развивая этот подход и опираясь на «текстовое» определение логического исчисления, можно по аналогии ввести понятие «видеоисчисление» (табл. 2).
Таблица 2Определение понятия «логическое исчисление»Логическое исчисление может быть представлено как формальная система в виде четверки V = < И, S0 , A, F >
где
• И – множество базовых элементов (букв алфавита);
• S0 – множество синтаксических правил, на основе которых
из букв строятся правильно построенные формулы;
•А – множество правильно построенных формул, элементы которого называются аксиомами;
•F – правила вывода, которые из
множества А позволяют получать новые правильно постро-
енные формулы – теоремы [7].
Определение понятия «видеоисчисление» (визуальное логическое исчисление)Видеоисчисление может быть представлено как формальная система в виде четверки V = < И, S0 , A, F >
где
• И – множество икон (букв визуального алфавита);
• S0 – множество правил визуального синтаксиса, на основе которых из икон строятся правильно построенные видеоформулы;
• А – множество правильно построенных видеоформул, элементы которого называются видеоаксиомами;
• F – правила видеовывода, которые из множества А позволяют
получать новые правильно построенные видеоформулы – ви-
деотеоремы. (Множество теорем обозначим через Т.)
§8. ИСЧИСЛЕНИЕ ИКОНИтак, мы определили нужные понятия визуальной математической логики. С их помощью можно построить исчисление икон.
• Множество икон И (букв визуального алфавита) задано тезисом 1 (см. главу 33) и показано на рис. 17.
• Множество S0 правил визуального синтаксиса описано в главе 33 в тезисах 2–37.
• Множество А визуальных аксиом включает всего два элемента: заготовку-примитив и заготовку-силуэт (рис. 232). Далее будем называть их аксиома-примитив и аксиома-силуэт.
• Множество Т, охватывающее все видеотеоремы исчисления V, есть не что иное как множество шампур-схем (абстрактных дракон-схем).
Заметим, что множество Т не включает аксиомы, так как последние содержат незаполненные критические точки и, следовательно, эквивалентны пустым операторам.
Множество Т распадается на две части: множество примитивов Т1 и множество силуэтов Т2.
• Множество F правил видеовывода также делится на две части F1 и F2. Множество F1 позволяет выводить все теоремы-примитивы, принадлежащие множеству Т1, из единственной аксиомы-примитива.
Оно содержит пять правил вывода: ввод атома, добавление
варианта, пересадка лианы, боковое присоединение, удаление конца примитива. Эти правила описаны в тезисах 10, 21, 28, 30, 31, 34 главы 33.
• Множество F2 дает возможность выводить все теоремы-силуэты множества Т2 из единственной аксиомы-силуэта. Оно содержит восемь правил вывода: ввод атома, добавление варианта, добавление ветки, пересадка лианы, заземление лианы, боковое присоединение, удаление последней ветки, дополнительный вход.
Правила вывода для силуэта описаны в тезисах 10, 21, 28–33, 35 главы 33.
На этом построение исчисления икон заканчивается.
§9. СЕМАНТИКА ШАМПУР-СХЕМИзвестно, что изучение исчислений составляет синтаксическую часть математической логики. Кроме того, последняя занимается семантическим изучением формальных языков, причем основным понятием семантики служит понятие истинности [1].
В исчислении икон семантика тривиальна. Различные видеоформулы (блок-схемы) могут быть истинными или ложными.
Цитата:
Видеоформула называется истинной, если она – либо ак-
сиома, либо выводится из аксиом с помощью правил вы-
вода (то есть является теоремой). И ложной в противном
случае.
Таким образом, все правильно построенные шампур-схемы (теоремы) истинны.
И наоборот, неправильно построенные схемы, не удовлетворяю-
щие визуальным правилам языка ДРАКОН, считаются ложными.
Примеры ложных схем показаны на рис. 156, 158, 160, 162, 164.
§10. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ АЛГОРИТМОВРоберт Андерсон подчеркивает: «целью многих исследований в области доказательства правильности программ является... механизация таких доказательств» [8].
Дэвид Грис указывает, что «доказательство должно опережать построение программы» [9].
Объединив оба требования, получим, что автоматическое доказательство правильности должно опережать построение алгоритма. Нетрудно убедиться, что предлагаемый метод обеспечивает частичное выполнение этого требования.
В самом деле, в начале главы было показано, что любая
правильно построенная шампур-схема является строго доказанной теоремой.
В алгоритмах дракон-конструктора закодировано исчисление икон.
Поэтому любая шампур-схема, построенная с его помощью, является истинной, то есть правильно построенной. Этот результат очень важен.
Он означает, что:
Цитата:
Дракон-конструктор осуществляет 100%-е автоматическое доказательство правильности шампур-схем, гарантируя принципиальную невозможность ошибок визуального синтаксиса.
В начале главы мы задали смешной вопрос: если шампур-схемы – это теоремы, кто должен их доказывать? Ответ прост. Их никто не должен доказывать, так как все они раз и навсегда доказаны.
Потому что работа дракон-конструктора построена как реализация исчисления икон.
А теперь добавим ложку дегтя в бочку меда. К сожалению, данный метод позволяет доказать правильность шампур-схемы и только.
Это составляет лишь часть от общего объема работы, которую нужно выполнить, чтобы доказать правильность алгоритма на 100%.
Здесь необходима оговорка.
Частичное доказательство правильности алгоритма с помощью дракон-конструктора осуществляется без какого-либо участия человека и достигается совершенно бесплатно, так как дополнительные затраты труда, времени и ресурсов не требуются.
Так что полученный результат (безошибочное автоматическое проектирование графики дракон-схем) следует признать значительным шагом вперед.
§11. ВЫВОДЫ1. Построено визуальное логическое исчисление, которое мы назвали «исчислением икон».
2. Данное исчисление можно рассматривать как раздел нового направления – визуальной математической логики.
3. Показано, что графический синтаксис языка ДРАКОН представляет собой исчисление икон.
4. Исчисление икон является теоретическим обоснованием языка
ДРАКОН.
5. Исчисление икон полностью реализовано во внутренних алгоритмах работы дракон-конструктора.
6. Дракон-конструктор осуществляет 100%-е автоматическое доказательство правильности шампур-схем, гарантируя принципиальную невозможность ошибок визуального синтаксиса.
7. Безошибочное автоматическое проектирование графики дракон-схем следует признать значительным шагом вперед, повышающим производительность труда при практическом работе.
8. Вторым (наряду с математическим) направлением, использованным при создании языка ДРАКОН, является научный подход к эргономизации конструкций языка. Такой подход позволяет улучшить визуальные образы языка (визуальные формы фиксации знаний), согласовав их с известными характеристиками глаза и мозга.
9. Разработка исчисления икон говорит в пользу этой идеи и служит примером, подтверждающим актуальность когнитивной эргономики.