Обсуждение

>>ISO 15926 в качестве одного из своих формализмов указывает на теорию категорий. Это означает, что есть шанс попробовать и моноидальные диаграммы для записи (аккуратно скажем) в языке, эквивалентном части 2 или даже эквивалентном части 7. Пока ничего такого не придумывается. Т.е. я примерно вижу, как сделать категорную семантику для ISO 15926 (в формулах), но она наглядности не добавит: моноидальные диаграммы будут тут бедноваты, либо я не вижу пока математического решения. В тех обсуждениях, что Вы давали на прочит, даже того, что вижу я - нет. Все очень и очень отдаленно. Поэтому пока решил поближе войти в тематику, а потом уже додумывать насчет нотаций.

то есть табличная нотация Gellish (и следующие из нее "формы", подготовленные в Exel -- любимая инженерами форма) пока являются лучшей на сегодня придумкой. А ведь это как раз эквивалент бесчисленного числа всплывающих окошек "a la Windows" интерфейса с формочками, которые замучиваешься "прокликивать" и заполнять -- вместо того, чтобы как-то нормально и слитно писать. И эти окошки -- ужас, и эквивалентные им командные строки с "последовательностью триплетов" не меньший ужас... Все понял, думаем дальше.

Я считаю, что этот случай нужно воспринимать несколько иначе: моноидальные диаграммы показывают, что можно найти графическую нотацию, которая 1:1 соответствует исчислению. И я воспринимаю это как повод искать исчисления, соответствующие уже используемым нотациям (ведь именно так произошло с Фейнмановскими диаграммами - они создавались без малейшей связи с моноидальными категориями!) Остается найти людей, которые будут это делать. :) Те, кто знает нотации - не очень знают математику, а математикам не очень интересны эти нотации.

Кроме того, то, что я не могу пока найти графического представления для этого стандарта, говорит лишь о моих умственных способностях. :) А теория замкнутых моноидальных категорий сегодня активно взаимодействует с линейной логикой, которая является, возможно, естественной логикой для описания процессов (кстати, процесс можно понимать как морфизм, я несколько раз об этом писал). Так что м.б. будут найдены более подходящие области применения этой нотации.

Я вот думал об этом сегодня. Дело тут не в математике, а в привитии вкуса к формализации в стиле computer science (т.е. формализации необязательно математической! Сегодняшняя computer science с ее мультипарадигмальными языковыми изысканиями -- это продолжение той же математики, но с учетом важности нотации и понятия "языка"). Я думаю, что сегодняшнюю ситуацию уже не переломить: нужно делать исследовательскую программу, в которой специально выращивать синтетический (и сначала междисциплинарный) предмет для исследований связки конгломерата из моделирования/дизайна<-->исчислений/языка<-->нотаций/явных_представлений<-->психопрактик_для_овладения_операциями_в_уме. Грубо говоря, сажать рядышком физика, математика, системного инженера, нэлпера (neurolinguistic programmer) и задать им работку на десяток лет: поглядеть на то, что уже происходит, отмоделировать это и попробовать поучить детишек. Очень интересный проект бы мог получиться. Но такие люди вместе редко собираются.

Насчет "естественной логики" для описания процессов нужно обязательно познакомиться с точкой зрения Conrad Bock -- поглядите, например, презентации по PSL на conradbock.org (основной постулат там как раз в том, что "народное представление времени отнюдь не соответствует машинам состояний и прочим экзотическим придумкам компьютерщиков. Поэтому есть требования к выражению процессов людьми". В итоге BPMN принял эти требования, и будет распространяться как пожар: во всякие "машины состояний" он будет превращаться компиляторами, а люди будут иметь дело только с отношениями "позже" или "раньше". Вполне возможно, что для :2 и :7 нужно сделать что-то похожее: для :7 выбрать легко понимаемые народом способы презентации, а для :2 оставить дикий математико-логический вид.

Абсолютно с той же идеи начинался и на ней же продолжается мой журнал: привитие вкуса к формализации, во всех областях знания. Это не означает абсолютно какой-то "сухости" или "мертвости" знания - пример моноидальных категорий показывает, что формализм может быть выражен ярко и образно, без потери точности. Математическая формальность говорит лишь о точности мышления, о его осознанности. Я уверен, что люди со временем сумеют отобразить в точных нотациях самые расплывчатые знания - если это действительно знания. Вообще опыт общения с людьми, которые хорошо знают свое дело, показывают, что у них часто развиваются чрезвычайно точные языки, не терпящие отклонений. Причем это встречается даже в таких, казалось бы, смутных материях, как медитативная практика. Это означает, по-моему, что за таким отточенным мышлением, или за какой-то его существенной частью, скрыт - да, формализм.

Это верное направление. В этом же смысле я солидарен с людьми, предпочитающими императивные языки. Претензии функциональщиков: плохая семантика, трудно анализировать и верифицировать. Аргумент императивщиков, что это удобно, отметается с намеком на умственные способности. Но ребята из CS, то, что семантика пока не разработана, что вы не умеете верифицировать проги с побочными эффектами - это ведь ваша недоделка, строго говоря, так что работайте. Примерно тоже самое верно и для представления процессов. Я употребил слово "естественный" скорее в том смысле, что это естественная база для формализации (того, что будет выражено в "очеловеченных" нотациях).

Вот мой пафос в том, что "формализм" недостаточен, нужно еще к нему добавить "выразительность" и "мыслительное удобство" и какое-то соответствие жизненным проблемам/объектам/феноменам и много чего еще, чтобы получился хороший инструмент. Это и есть отличие computer science как мета-науки от логики-математики как мета-науки (части гносеологии), которая озабочена лишь "формализационной" частью. Нужно не только вкус людям к формализации прививать, но и формалистам вкус к людям!

Ниже уже ответил, фактически :)

Т.е. да, согласен, правильное движение - не только к точности и формальности, но и к доступности этого "точного" всем. Гуманизм форева. :) И возможностей, на мой взгляд, все больше.

Интересно всё это. И, вроде, в осносной своей массе, в какую-то конструктивную сторону движется.

Вот только убери рассуждения про римскую нотацию для чисел в десятичной системе. Ибо чушь написана :-((((

С арабской нотацией против римской -- это классический пример. Так что не уберу, пока ты не продемонстрируешь, в чем тут чушь.

Чушь не в примере, а в формулировке про нотацию ДЛЯ десятичной системы. Число можно считать существующим в десятичной системе только ПОСЛЕ того как оно записано арабскими цифрами, грубо говоря. число в десятичной системе НЕ МОЖЕТ быть записано римских цифрами, извини. Эти оба высказывания - о языках (разумеется о двух разных).

"если речь идет о числах в десятичной системе счисления, то " уже по определению речь идёт о нотации из 10символов и не может идти о римских числах.

А, ты про позиционные и непозиционные системы. Да, конечно, поправил. Ты бы как-то свой стиль комментариев поправил: указание на "чушь написана" не указывает на то, что не так. Указание на "в вашей программе есть баги", если ты эти баги уже нашел, но не говоришь, где и какие, обычно бессмысленно.

>>Дальше у меня мысли пошли в сторону моего любимого текста (много лет я таскал листочек с его распечаткой у себя в портфеле) Accretion model of theory formation (кратенько пересказана в конце постинга http://ailev.livejournal.com/469995.html). Нужно время от времени находить новые формализмы (и непосредственно соответствующие им нотации), и перекодировать большие куски знания в эти формализмы. Иначе каюк, не будет хватать мощности головы (да и компьютера впридачу тоже не хватит). John Baez и The n-Category Café (и того, и другое Вы упоминали уже) как раз являются двигателями одного из проектов по такой перекодировке. А именно, большие куски математического знания перекодируются в очень удобную и единообразную форму - теория категорий (n-категорий). Самый мощный текст по этой программе - это конечно лекции Баеца, но тут нужна уже сильная подготовка. А так тексты Баеца бывают очень и очень популярны (мне кажется, он из тех, кого потом назовут "великий популяризатор").

Тут очень сложный вопрос: чтобы воспользоваться мировым опытом, "категорным нинзя" нужно будет разобраться с "обычной математикой". А чтобы стать "категорным нинзя", сегодня также нужно разбираться с обычной математикой -- и стимул "выучить немного, чтобы уметь много" пропадает. Тут нужно поставить задачу "глобальной перекодировки", которая больше связана с культурой и образованием, нежели с собственно перекодировочной работой. Как я понимаю, развитие софта устроено примерно так же: legacy-приложения делают почти невозможной задачу развития. В 1975 году легко было развивать софт, ибо legacy еще не было. А вот сегодня тебе дадут предзаданную среду из ОС, библиотек, фреймворка и соглашений кодирования -- и будешь писать свой маленький кусочек. С формализмами все еще хуже: прикоснешься к ним, и затем нужно будет переписывать всю физику, всю инженерную литературу и т.д. В 1750-м году именно так и делали, но тогда наработано было много меньше. Я бы подумал-подумал и поставил задачу "перекодирования" для искусственного интеллекта: пусть переписывает книжки со старых языков на новые, по мере затребования этих книжек читателями! Будет еще один google.translate.com с "докатегорного" на "посткатегорный" ;) Это в 2010 году только наполовину шутка...

Стимул в том, чтобы сделать культуру более связной. Сегодня алгебраист, тополог и computer scientist могут разговаривать на одном языке. Во всяком случае, все идет к тому. Именно то, что сделает культуру более связной, сможет преодолеть все существующие ограничения и запустить проект переучивания (возможно, даже со школьных лет, но не обязательно). То же самое в мире софта. Например, я не ограничен операционной системой - устанавливаю vbox, если нужно, и вперед. Культура живет по законам (взаимо)понимания, причем не обязательно между людьми. :) Насколько я понимаю, одна из целей ISO 15926 именно в этом.