Они то как раз на пег дро... молятся. Даже макрос Peg какой-то наваляли и теперь пиарятся им в каждом углу РСДНа

Хочу напомнить, что иерархические и графовые СУБД доминировали до тех пор, пока не пришли теоретики и не навешали лохам из IBM много лапши на уши - а те, в свою очередь, не подключили маркетинговую мощь своей говноконторки. И никакого «формализма» в этих СУБД не было, они просто делали свое дело, работали, никому не мешали.

Да какой там PEG, если у них Pratt во все щели? От того, что они своё говнище назвали PEG-ом, оно меньшим говнищем не стало.

Можедли автоматическое доказательство теорем доказать само себя, вот в чём вопрос.

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

Во всем треде анонимусы почему-то думают, что вся наука в компиляторе - в парсерах.

Ололо. Это теоретик-борщехлеб тут сам пел про «теорию формальных языков» - к нему и претензии. Начал бы про эвристики для tiling в instruction selection вякать, ему бы рассказали, как это делать по-инженерному и без говнотеорий. И про SSA и domination frontier без теорий рассказали бы. Но борщехлебы-то как раз только про парсеры и горазды рассуждать.

Попробуйте сделать хоть сколько-нибудь приличную оптимизацию кода на коленке, без теории.

Все приличные оптимизации строятся на эвристиках. Теории обосрались и не нужны.

Начал бы про эвристики для tiling в instruction selection вякать, ему бы рассказали, как это делать по-инженерному и без говнотеорий. И про SSA и domination frontier без теорий рассказали бы.

И как?

фортран и лисп были написаны крутыми мастерами(практико-теориками) при не существующей на тот момент теории формальных языков.

А потом из-за кривого парсера Фортрана американская автоматичекая станция промахнулась мимо Венеры.

Tiling делается экспериментально полученными эвристиками. Все заумные теории приводят к чрезмерно дорогостоящим решениям, которые в лучшем случае дают на 2% более быстрый код, чем средненькая тупая эвристика.

Алгоритм SSA-преобразования вообще очевиден, и легко формулируется без всяких там понятий о domination frontier - тупо ставим phi-узлы везде, где пересекаются пути видимости двух разрушающих записей в переменную. Никакой теории, и все очевидно.

Ок, RSA тоже создавали брутальные инженеры, не опиравшиеся на теорию?

Почему ты так не любишь борщ? Он же офигенный.

Раз уж у нас поле чудес, то (голосом Якубовича): «Ссылку на доказательство - в студию!»

а как в ПОМИ сейчас со входом, я б сходил?

пролетарий (или хлебороб? в общем, «практик») в комментах порадовал.

Лекции будут проходить в ПОМИ РАН (Санкт-Петербург, наб. р. Фонтанки, 27), Мраморный зал, второй этаж.
Background, history and propositional logic.
First-order logic with and without equality.
Decidable problems in logic and algebra.
Interactive theorem proving and proof-checking.
Applications to mathematics and computer verification.

Я не понял, лекции будут на англицком языке? Так у нас гасударственный язык - русский, и в образовании должен использоваться русский, за исключением курсов иностранных языков.

Лекции на английском, да.

Так у нас гасударственный язык - русский

продолжай наблюдения.

Согласен, гнать в шею этого харрюсона, этого агента мировой закулисы! http://www.cl.cam.ac.uk/~jrh13/ - видите, видите! Сатанист! Вон со Священной Рассеи-Матушки!

нехило у тебя бомбануло (:

Тоже английский не осилил? Страдай молча.

Так у нас гасударственный язык - русский

продолжай наблюдения.

То есть, от «англицкий» тебя не покоробило?

Нужны практики, которые работу работают. Теоретики никогда ничего полезного не делали.

Такие «практики», о которых говоришь ты (делающие «еще вчера» мутные требования говнозаказчика) не только не делают ничего полезного, но и своей деятельностью наносят немалый экономический ущерб, как прямой, так и косвенный.

Жаль, что не в МИАН'е или НМУ. Санкт-Петербургу повезло.

Так СПбГУ немалые деньги влили. Вот только сомневаюсь что хоть какой-то выхлоп будет кроме дачных поселков администрации.

PS Перечитал новость - лекции не в СПбГУ, а в «неэффективной» РАН.

Инженер ставит эксперименты, и исходит всегда только из фактов.

Facepalm.jpg Инженер экспериментов не ставит. И с фактами не работает. Тебя где-то жестоко обманули. Инженер занимается реализацией моделей, разработанными «ненужными» теоретиками. Когда инженер начинает самостоятельно обобщать факты он становится тем самым «теоретиком». Или, что более вероятно - фриком.

Почему ты так не любишь борщ? Он же офигенный.

Судя по всему у него плохие отношения с мамой. Эдипов комплекс и все дела, cast Freud.

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

Борщехлеба нехило бомбануло, ошметки пердака с потолка свисают!

Но нищеброды-терететики этого себе позволить не могут

Почему? У них же грантики есть.

ну до физфака даже дошло, что-то во всяком случае новый кластер имеется и ремонт в НИИФе пытаются делать.

Грантиков на покушать недостаточно. По грантикам отчитываться надо. «Купил ЭВМ IBM PC» это нормально в отчете, а «похавал устриц в ресторане» - херня какая-то.

Вспомнилось: http://habrahabr.ru/post/183374/ Интересно, это доказательство как-то можно формализовать и проверить на компьютере?

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

Вспомнилось

http://cdn.memegenerator.net/instances/250x250/38249767.jpg

Алексей Николаевич Крылов, Борис Григорьевич Галёркин, Иван Григорьевич Бубнов.

А потом из-за кривого парсера Фортрана американская автоматичекая станция промахнулась мимо Венеры.

да, над этим стоит задуматься

в частности: современных программистов хотя и называют инженерами, но зачастую они выполняют работу не инженеров, а *ученых*

где проходит грань?

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

а при проектировании, допустим, языка программирования цели необходимо придумать, скажем, «устойчивость к опечаткам» — и придумать цели это уже *научная* работа, а вот достигать эту цель — возможно что и инженерская

и в догонку:

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

в частности: современных программистов хотя и называют инженерами, но зачастую они выполняют работу не инженеров, а *ученых*

Да «программистами» сейчас кого только не называют... но всё же программистов, выполняющих работу ученых, я, пожалуй, не встречал. Или я понимаю под работой ученого что-то другое.

остальное время питаться разнообразной, здоровой, качественной пищей в дорогих ресторанах.

/0 Качественная пища в ресторанах встречается разве что за пределами РФ и особенно за пределами Москвы.

Правда ли дорогая рыба вкуснее дешевой? Или нам это только кажется? Чтобы это проверить, «Среда обитания» устроила эксперимент. По просьбе программы шеф–повар рыбного ресторана приготовил изысканные блюда из самой дешевой рыбы. В ход пошла мороженая треска за 70 рублей, мороженая пикша за 65 рублей и филе масляной рыбы за 200 рублей. Из филе масляной рыбы шеф–повар приготовил «тартар из серо–белого тунца». С легкой руки мастера мороженая пикша превратилась в «блюдо из свежевыловленного подкопченого угря», а обыкновенная, самая дешевая мурманская треска стала «охлажденной черной треской». Это редкий деликатес, и купить его в магазинах просто невозможно.
Изысканные блюда дали попробовать звездам шоу–бизнеса. Правда, им сказали, что это элитная и изысканная рыба редких сортов. Никто так и не узнал, что ел обыкновенную треску, и не смог отличить пикшу от копченого угря. Только один гость вечеринки – Алексей Митрофанов — догадался, что закуски сделаны из мороженой рыбы.

Так потому их имена и сохранились что их довольно мало. А если каждый начнет NIH-синдромом страдать и положит на стандартизацию? Хотите чтобы везде такой бардак был как в софтостроении?

здорово. хотя обзорных лекций на эту тему и так хоть отбавляй - хотелось бы конкретики

Да, современные «универсальные человеки» недостаточно универсальны. Куда им до того же Леонардо:

…Пусты и полны заблуждений те науки, которые не порождены опытом, отцом всякой достоверности, и не завершаются в наглядном опыте…

Ни одно человеческое исследование не может называться истинной наукой, если оно не прошло через математические доказательства. И если ты скажешь, что науки, начинающиеся и заканчивающиеся в мысли, обладают истиной, то в этом нельзя с тобой согласиться, …потому, что в таких чисто мысленных рассуждениях не участвует опыт, без которого нет никакой достоверности

Вообще, разделение на «чисто науку» и «чисто инженерство с эвристиками» — это шиза, которая создаёт неправильную точку зрения.

and we need to go deeper

где проходит грань?

Нет её, см. выше

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

Вот например, инженеришки строят здания

Ну и где тут щупанье эвристик наобум? Это всё вымерло с цеховой организацией и прочими вольными каменьщиками.

Сейчас копать надо глубже, и системный подход и есть если не к «универсальному человеку», то к НАСТОЯЩЕМУ творцу из професии (инженеру там или учёному)

а при проектировании, допустим, языка программирования цели необходимо придумать, скажем, «устойчивость к опечаткам» — и придумать цели это уже *научная* работа, а вот достигать эту цель — возможно что и инженерская

Большинство языков программирования слепили из того, что было, а потом «чем поливали, то и выросло».

Но это ведь не причина не менять парадигму?

К примеру, инженеришки-строители уже наступили на грабли в отстутствие хорошей, практичной теории и обмазываются всеми этими моделями типа BIM или вот не от хорошей жизни, а от того, что дальше уже без хорошей, практичной теории можно строить только сортиры ну или «дорого, быстро, качественно — выберите любые два» отмазки. Копать нужно глубже, во все три, а не два.

А для этого и нужны все эти модели и теории — вот нагрянут массово вот такие например, девайсы, и будут программеры ныть как строители по первой ссылке.

Вместо того, чтобы просто сменить парадигму.

Вообще, разделение на «чисто науку» и «чисто инженерство с эвристиками» — это шиза, которая создаёт неправильную точку зрения.

гы

я делю совсем не так — на research (наука) и на development (инженерщина), а есть еще r&d

и мой пойнт был в том, что современный development требует хоть игрушечного, но research-а, и видимо поэтому ты (или другой анонимус?) и не понимаешь между ними разницы

чисто наука — это например нахождение и доказательство соотношение aᵖ ≡ a (mod p) без всякой цели его использовать где-то в development

эвристики вполне могут быть в науке и не делают ее инженерщиной

а вот то, что в современной науке часто ищут алгоритмы, опять же затрудняет различение ее от инженерщины

Да «программистами» сейчас кого только не называют... но всё же программистов, выполняющих работу ученых, я, пожалуй, не встречал. Или я понимаю под работой ученого что-то другое.

хорошо, вот конкретный вопрос: анализ требований заказчика и составление по нему технического задания — это:

1. research
2. development
3. r&d
4. ни одно из этих

з.ы. ты, конечно, можешь совершенно верно сказать, что заниматься этим должен аналитик, а не программист, однако часто этим занимаются программисты, и я бы не сказал, что это совсем уж abuse терминологии

я делю совсем не так — на research (наука) и на development (инженерщина), а есть еще r&d

а ещё есть теория, в которой всё работает, и все знают, почему и практика, в которой ничего не работает, и никто не знает почему :)

но мы же не об этом· а об том, как бы их совместить

нет ничего практичнее хорошей, годной теории

и мой пойнт был в том, что современный development требует хоть игрушечного, но research-а, и видимо поэтому ты (или другой анонимус?) и не понимаешь между ними разницы

а с этим никто и не спорит, что требует (это другой анонимус)·

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

чисто инженерный подход (ну или физиков), в худшем его проявлении — это изобрести какую-нибудь простенькую эвристику, описываемую простенькой моделью, которую и то не считают потребным нормально формализовывать· в итоге Быстро & Грязно™ наговнякаем какую-то псевдомоделишку, и быстро заткнём свою частную задачу·

это может быть и работает в краткосрочной перспективе, когда надо быстро решить задачу, а не разводить мысью по древу· но в долгосрочной, это не работает наилучшим образом — потому что, внезапно, такие модельки (если они там вообще были) получаются не composable·

и кому-то всё равно придётся такие composable модели делать, хоть в рамках хорошей, годной теории, хоть хорошей, годной модели (включающей в себя метамодель, то есть, копать надо таки глубже)·

как пример:

1· ну вот строители, того же моста· можно быстренько обмазаться СНиПами, наговнякать какой-то мост через речку вонючку, но когда по нему пройдёт рота солдат в ногу, и он от резонанса развалится, будет ясно, что сопромат-таки надо было изучать·

2· можно рассчитать правильный, годный мост· но что будет за пределами применений, когда выяснится что условия эксплуатации изменились? сносить и строить заново?

3· а можно взять какую-то более внятную метамодель типа той же BIM, построенной на основе системной инженерии, ЖЦ объекта (моста), включающей 2D-3D-4D-5D-6D модель проекта (подробности см· в ссылках выше): 4D: включает время, то есть жизненный цикл; 5D включает деньги, 6D — и т·д·

то есть, системная инженерия, общеотраслевые стандарты типа ISO 15926, модель и метамодель жизненного цикла, и только как частный случай применения всех этих мета — конкретный мостик·

или взять более практичную метанауку, то есть какую-то более общую «теорию всего», опять же построив более composable модель-решение·

чисто наука — это например нахождение и доказательство соотношение aᵖ ≡ a (mod p) без всякой цели его использовать где-то в development

опять таки, кто сказал что те же диофантовы уравнения потом когда-нибудь где нибудь в development не пригодятся?

эвристики вполне могут быть в науке и не делают ее инженерщиной

могут, в чём вопрос· собственно речь о том, что настоящая, годная инженерия — это например системная инженерия, и понятие о системе, о модели и метамодели, о жизненном цикле всего этого·

а инженерщина негодная — это когда инженеришко-образованщина краем уха что-то там слышало и говнокодит свои эвристики, рождая очередной технотрешъ· который не пером ни описать, ни топоромъ не вырубить, ибо not composable·

а вот то, что в современной науке часто ищут алгоритмы, опять же затрудняет различение ее от инженерщины

почему это? ищут то не только методом эвристического тыка· сколько замером, измерением, анализом чувствительности системы и её модели· чтобы знать куда копать, а не тыкать наобум·

для того и потребны всякие там автоматические выводы, чтобы искать направленным поиском·

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

это если по уму. касательно истории языков программирования имеем следующий анекдот:

яйцеголовые академики родили Algol-60, в котором есть такие прикольные W-грамматики. с ними можно долго дро играться, но тот факт что даже грамматику этого алгола толком не описали, реализацией это не закончилось — как бы намекает нам о практичности всего этого.

и вот среди них затесался инженер-электронщик. который сказал, ребята, да вы фигней страдаете. если вы например будете строить теорию эл. схемы вместо сборки её из хороших, годных кубиков, то вы так ничего не родите. и почему собственно, если подход работает с эл. схемами, подход с software circuits должен как-то сильно отличаться?

взял и упростил всё это. и зафигачил Algol-W, с простой однозначной грамматикой. звали его Никлаус Вирт.

опять же, где эти исследования того, как язык будет применяться, и что туда надо проектировать?

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

уж по логике вещей, могли бы провести такое, прежде чем чего-либо там изобретать? и где они, эти исследования?

но нет, вещи так не растут. вырастает что-то из того, что было, а потом скачут на этой лошади, пока она того, не околеет окончательно в технотрешъ.

вообще язык программирования это есть святая троица собственно языка и его способностей выражать парадигмы, стандартной библиотеки и тулчейна-инструментария, то, что делает его платформой.

так почему же эта платформа ОБЫЧНО не проектируется правильным, системным образом, чтобы из этих запчастей появилась какая-нибудь эмерждментность?

яйцеголовые академики родили Algol-60, в котором есть такие прикольные W-грамматики. с ними можно долго дро играться

Вообще-то это был Algol-68.

парадокс доказательства

это офигенно, вообще-то. он им такой shut up and show them the code а они ему типа линус трольвальдс нвидия

«интер-универсальный геометр» офигенен.
просто ходячий Boost.

как я понимаю эту сложившуюся ситуацию:

1. Математик Синъити Мотидзуки придумал свой метаязык, адекватно описывающий эти 50+4 работ (объёмом 1050.00 страниц) на своём метаязыке. На нём самом. На своём понятийном языке, который применятся также в его предыдущих работах из списка литературы (50 работ на 1000 страниц).

2. Применил для доказательства. Говорит, что доказал, вывалил скомпилированный бинарник и сорцы на метаязыке.

3. Остальные недотыкомки от математики ниасиливают его терминологию, понятийный аппарат, ибо неспособны держать голове более N разнородных понятий (вращать, жонглируя тарелочками количестве >N штук одновременно).

Чего именно они ниасиливают? и почему?
a) MAD SKILLZ жонглировать одновременно >N разных понятий за один раз ( сидя на кресле крутим левой рукой по часовой стрелке, правой ногой против, левой ногой сверху вниз наружу, правой рукой снизу вверх вовнутрь. Слабо? А теперь в каждую руку/ногу берём палочку, крутим, и на ней Ni тарелок. А теперь то же самое, танцуя ).

man Fitts Law, 7+-2 ATTENTION SPAN

его знание НЕЭРГОНОМИЧНО

б) не владеют терминологией

в) не владеют аппаратом, другой парадигмой

г) не видят новых возможностей другой парадигмы, которые видит автор метаязыка/нотации/теории

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

4) Ниасилияторы начинают и бросают, не доходя до конца. Потому что его знание не эргономично для помещения в голову, а доказательство -- быдлокод, который возможно, всё-таки как-то работает, но нираспарсивается джуниорами, потому что они не владеют «кластером метапарадигм» ну и не могут крутить столько тарелочек одновременно, как этот японский сумрачный гений.

ИТОГО, Жизненный Цикл НЕОСИЛЯТОРА выглядит примерно так:

яННП => ой, как всё сложно => ( в список литературы )чем дальше в лес, тем толще партизаны => goto 1:яННП => FUD, да ну его нафиг => голосуем ногами

Теперь это доказательство надо ДЕКОМПИЛИРОВАТЬ, для этого сначала надо бы расшифровать (отреверсить) его сумрачного гения (мета)язык, чтобы хоть распарсить о чём там вообще и как именно и куда ещё так можно, и к чему это вообще или лучше бы водки выпили.

Интересно, это доказательство как-то можно формализовать и проверить на компьютере?

Интересно, это доказательство как-то можно формализовать и проверить на компьютере?

ИМХО, не ту задачу ДЕЙСТВИТЕЛЬНО НУЖНО решать, что в топике  — нужно не «автоматическое доказательство теорем», и нечитаемый быдлокод в прувере, на 10500 страниц. ну наговнякает вам робот 10500 страниц НЕЭРГОНОМИЧНОГО знания, и какая от всего этого польза? чему нас это сможет научить новому?

нужно хотя бы для начала когнитивно разгрузить «автоматизированное человеко-машинное понимание/верификация/применение уже кем-то доказанной теоремы», и составить базу знаний для теорем типа как OpenCyC и IBM Watson, Wolphram Alpha для фактов.

вот например, смотри чему научились в настоящей, системной инженерии:

(описание) презентация продукта

настоящие, системные инженеры научились из текстого описания инженерных объектов (документации) извлекать смыслы — пока самые базовые, то есть онтологию. заполнять автоматически справочники, при этом программа понимает отдельные объекты, их свойства, связи между ними (онтологию). да, онтология стандартая типовая ISO 15926, для которой есть стандарт с моделями и метамоделями типовыми же. да, тексты технические, регулярные.

но на базе этого можно было бы выстроить некий Человеко-Машинный Интеллект (ЧМИ): раз уж замахиваться на сильный ИИ это слишком пока сложно, не будем.

вместо ИИ, который должен сам догадаться, нужен ЧМИ, где каждый хорошо делает своё дело: машина кранчит данные, извлекает объекты из словесной руды, а человек — думает. то есть, организовывает эти объекты по смыслу в онтологии.

(дальше)

инженерам вполне хватает ISO 15926, но теоретикам копать надо глубже.

надо смотреть в сторону Reproducible research статьи вики, планета

чтобы такая ситуация как с Мотидзуки разруливалась по ходу написания его работы.

плюс, скрестить Reproducible Research с Semantic Wiki.

вот если бы Мотидзуки вывалил на-гора не только PDF, ну а хотя бы LaTeX исходники?

дальше:

1. Преобразуем их в WEB-подобную разметку для Reproducible Research. Наподобие Грамотного Программирования Д. Кнута. В итоге получаем, что можно в одном месте писать и текст работы, и сниппеты с кодом.

2. Пишем, что понятно в виде сниппетов с кодом. Для прувера, который проверит что все переходы корректны.

ДЕКОМПИЛИРУЕМ смыслы :

3. Преобразуем WEB-подобную разметку в Семантическую Вики. Семантическая позволяет задать типы ссылок: теперь вместо ссылки на объект будет запись объект-отношение. этим можно моделировать субъект-объект-отношение, с возможностью править в семантической вики онтологию объектов и отношений. Плюс, появлятся возможность в обсуждениях вики коллективным хайвмайндом порассуждать, что же имел в виду автор, обозначая эту сущность вот так. В идеале, все такие сущности должны быть распарсены из его 10500 страниц предыдущих работ до того места, где он их описал, определил.

4. в топике на хабре разумные вещи говорит Rational_Yurij , про связность и узлы этого графа. В итоге, аксиомы и невыводимые положения можно определить анализом графа.

5. В итоге, помимо обсуждения мы получаем также и код для прувера.

6. «Компилируем» вики в LaTeX + org-mode babel Reproducible Research исходник. Потом из него получаем

а) оригинальную работу (продукт1)

б) комментарии хайвмайнда к упанишадам (драфт к продукту 1, с комментариями)

в) сорцы кодов для прувера (продукт2)

Компилируем продукт2, и если всё сходится — автор многабукв очевидный гений

На будущее1, можно подумать как сделать такую ЧМИ работу в Асоциальной семантической-вики сети более ЭРГОНОМИЧНОЙ.

И бить палкой по жопе таких быдлокодеров, которые говнякают неЭРГОНОМИЧНОЕ ЗНАНИЕ, которое криэйтор нетлёнки мог бы и потрудиться переформулировать попонятнее.

хотя возможно, это должен делать не он, разделение труда всё-таки.

гений один, а хайвмайнда много.

На будущее2>будущее1 можно подумать про систему обучения, как сделать обучение этому пакету знания более удобным.

Я так понимаю, НУЖНО создать (полу)искусственный интеллект (ИИ/ЧМИ), в области автоматического доказательства теорем, но не Старого поколения, который может вывести доказательство из старых, породив write only 10500 строчек быдлокода прувера, которые никто не распарсит,

а Нового (трансгуманистического) пост-поколения, который сможет в 1ю очередь, ОБЪЯСНИТЬ, чего же придумал автор (и ДОГАДАТЬСЯ, в терминах его, автора, языка, где нетривияльные ходы, а где прав, где не прав, при нужде объяснив ниасилятору, что именно он пока ещё ниасиливает, и куда копать, чтобы дошло).

Это может быть не совсем ИИ, скорее ЧеловекоМашинный Интеллект (ЧМИ).

всё расскажет, объяснит добрый доктор «Алмазный Букварь Для Благородных Девиц»

Как такой ИИ может работать?

Нужен Иск.ин./ЧМИ/АсоциальнаяСеть- «ПОНИМАТЕЛЬ», который:

1) Проанализирует доказательство, совместив анализ с разбором ЕЯ

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

например в виде «Семантической вики», где у ссылок на URL-понятия есть тип, означающий отношение между понятиями.

RDF задаёт онтологию в виде Subject-Object-Relation, или (wikiitem,WIKITYPE)

набьёт рёбра и остов графа, и чего-то проанализирует про достижимость узлов.

В итоге можем получить список аксиом, и невыводимых утверждений.

Подробности см. /«Rational_Yurij,18 июня 2013 в 11:26#» из примера из «задачника по математике» Г. Остёра.

Сущности выделяются в пункте #1 анализом на ЕЯ, затем их можно аннотировать свойствами.

3) Странички онтологии можно править в вики, указывая (пополняя словарь онтологии), что можно с понятием делать. Как минимум вручную, как максимум, роботом, анализирующим ЕЯ.

4) ВАЛИДАТОР Анализатор-валидатор-верификатор должен проверять, имеет ли утверждение место, справедливо ли оно в рамках старой системы аксиом + онтологии. ВЫполняется: ДА/НЕТ/Множество-плотность-вероятности/категория

5) ПОНИМАТЕЛЬ должен проверять, имеет ли утверждение смысл.

6) ОСИЛЯТОР должен проверять, понятно ли утверждение.

5) - 6) могут быть роботами, но скорее всего, это будут люди в человеко-машинной системе. Типа семакнтической Википедии.

7) АННОТАТОР должен отмечать нетривиальные ходы, неочевидные, например, попытку применения нового инструмента и/или применения в новой области. Грубо говоря, он «выделяет макросы» и идиомы, паттерны из общего потока сознания.

8) ЭРГОНОМИК-конгитивист (ТОЛМАЧ) должен попытаться перетолмачить понятое на язык, понятный ОСИЛЯТОРУ. Для этого ТОЛМАЧ пользуется обратной связью от ОСИЛЯТОРа, и если тот ниасиливает, пытается переформулировать то же содержание другими словами. Иначе, он минимизирует количество и уровень сложности макросов и используемых в них спецформ, перекомбинирует своими тёплыми ламповыми комбинаторами вместо непонятных универсальных SKU.

Пример: ОСИЛЯТОР ниасиливает замыкания, продолжения, нелокальные выходы и монады, но осиливает императивщину, или конечные автоматы. Тогда ТОЛМАЧ избавляется от этих конструкций, показывает их в более простой форме, но прицепляет команды-замыкания АННОТАТОРу (макросы-аннотации в сема.вики), пометку на будущее «это упрощённое понимание», на самом деле требуется осилить вот то и вот это. Есть разные уровни понимания, на разных (не)ОСИЛЯТОРов.

9) см. про «Зону ближайшего развития» от Выготского. Из-за этой зоны мы имеем: утверждение будет ниасиливаться никаким ОСИЛЯТОРОМ, если оно надоступно из зоны.

10) ОБУЧАТОР должен делать следующее: моделировать ЗБР и ЗАР (зону актуального развития), и пытаться разложить один и тот же материал, понятие по уровням ЗБР.

11)Осилив одно объяснение ОБЪЯСНЯТОРа, индивид может повысить свою ЗАР (хотя для этого потребуется практика и применение знания).

12) Повысив, ЗБР переходит в ЗАР.

ЖЦ знания:

старая_привычная_картина_мира= > (когнитивный_диссонанс) => мотивированный_интерес => ЗБР => ЗАР

-= задача системы:=-

как можно сильнее облегчить эргономику перехода, «убирать барьеры»

???

PROFIT!!!

может быть. суть в том, что если

а) это яйцеголовое теоретизирование не ограничить, продукта на выходе и не будет

б) если «пускай растёт само», то получится очередной неэргономичный выкидыш — технотрешъ.