05.07.2012 20:45, Artem Chuprina пишет: > Артём Н. -> debian-russian@lists.debian.org @ Thu, 05 Jul 2012 19:56:29 > +0400: > > >> >> АН> Да, кстати, Пролог я не понимаю. :-( > >> >> > >> >> [...] > >> >> > >> >> АН> И на практике: будь всё так хорошо, как вы пишите, все бы уже > давно > >> >> АН> писали на Прологе (по крайней мере, знали бы что это такое). :-) > >> >> Ну ведь ты же сам написал, что ты его не понимаешь. Думаешь, ты один > >> >> его не понимаешь? > >> АН> Если был он был такой хороший, его бы понимали. Потому что, за это > >> АН> бы платили. :-) И этому учили. C ничуть не проще, чем Пролог. Он > >> АН> просто имеет другую парадигму. "Развёрнутую" на 180. У машины > >> АН> вывода есть свои недостатки, ограничения и своя область > >> АН> применения. По какой-то совокупности причин, Пролог не нашёл > >> АН> широкого применения (хотя к нему интерес то падал, то > >> АН> возобновлялся). > >> Понятность среднему хомосапиенсу, как и всякое другое качество, не > >> бывает бесплатной. И отнюдь не на всех задачах оно важно. Если средний > >> хомосапиенс не может понять саму задачу, то понятность ему инструмента > >> для ее решения ценности не имеет. > АН> Хм... И про какие задачи, которые выше понимания среднего, идёт > АН> речь? Т.е. где сейчас реально используются Пролог системы? > > Вот это уже не вполне ко мне вопрос, я сам на Прологе не работаю. > Насколько я понимаю, целевая его ниша - это задачи аналитического типа. > Ответ на вопросы "что из этих данных может следовать?" > > >> >> Потому что правила > >> >> рассуждений с этими законами правильны настолько, насколько правильна > >> >> математика (если ты знаешь, что именно формулируется в теореме Геделя, > >> >> то ты понимаешь это условие). > >> АН> Думаю, что частично понимаю. > >> АН> Пролог - аксиоматическая система. > >> АН> И, следовательно, любая система, построенная в нём, - такая же. > >> АН> Т.е., если "И" - аксиома Пролог, которая задаёт истинность А и Б, > при истинности > >> АН> и А, и Б, все аксиомы, заданные на её основе будут истинны в > границах данной > >> АН> системы. > >> АН> Доказательство истинности этой аксиомы и непротиворечивости правил её > >> АН> взаимодействия с остальными относятся к доказательству истинности и > >> АН> непротиворечивости Булевой алгебры. > >> АН> В данном случае, математика правильна априори. > >> АН> Так? > >> Последнее предложение неверно. Скажем так, мы верим, что математика > >> правильна (в том смысле, что доказанный в ней результат о некоторой > >> модели можно в рамках ограничения этой модели применить к реальности). > >> Гедель нам доказал, что ни на что, кроме веры, мы не можем тут > >> положиться даже на предмет ее внутренней непротиворечивости, не говоря > >> уж о применениях к реальности. > АН> Я понимаю, что Гедель показал это для формальной системы, которой > АН> является математика. Но, если используется Пролог, то решается > АН> практическая задача. В таком случае, математика используется > АН> потому, что она работает. Т.е. предполагается, что она верна? Это > АН> аксиома. :-) > > Очень полезно все же помнить, что предположение о правильности > математики - это тоже предположение. Такое же, как предположение о том, > что выполняется закон сохранения импульса. Кстати, законы рассуждений, > используемые в Прологе, не эквивалентны тем, которым нас учат в школе и > даже в вузе. В смысле? Там есть что-то новое? :-) Это же обычная "машина вывода", как и логика самая "обычная.
> >> >> А вот как соотносится твоя модель, > >> >> выраженная в нелогических аксиомах, с реальностью - это уже не к > >> >> Прологу. > >> АН> Но в точности тоже самое возможно сказать и о других языках. А > >> АН> тесты нужны именно для того, чтобы проверить соответствие модели и > >> АН> реальности. Там тоже самое, даже такие же побочные эффекты могут > >> АН> быть. И программа, на нём написанная не является правильной только > >> АН> потому, что она написана на Пролог. Просто тестами надо покрывать > >> АН> факты и правила, а не функции и процедуры или я не прав? > >> > >> В выводе - да, прав. Но надо учитывать, что большинство наших тестов > >> для других языков таки работают внутри модели, а не проверяют ее > >> соответствие реальности. То есть для прологовской программы не имеют > >> смысла. Природа тестов для прологовской программы должна быть > >> существенно иной, нежели привычно. > АН> Хм... А как тест может работать не внутри модели? Программа - > АН> модель. Даже, если тест получает данные извне, он всё-равно > АН> работает в данной модели. > > Не обязательно в данной. Это существенно. Скажем, тест, который > получает сигнал с реального датчика, сует его в программу, получает из > программы команду на управление реальным железом, выдает ее в железо, и > потом измеряет угол его поворота, например, другим датчиком, таки > выходит за пределы той же модели. Ну да. Разве что так. Но причём здесь Пролог? > И его работа уже существенно ближе к реальности, чем модель, в которой > написана программа. Но, кажется, это две стадии тестирования? И нельзя тестированием с реальным датчиком заменить тестирование с "эмулятором". > АН> Чем тут отличается Пролог от императивного языка, например? Здесь > АН> я просто вижу те же самые ошибки человека: неверное задание правил > АН> (неполнота, неточность или ошибочность) и неверное задание фактов. > АН> Что и должны покрывать тесты. Ведь так? > Так. А теперь внимание: что значит словосочетание "верное задание > фактов"? Скорее всего, тестировать соответствие этого задания опять же > модели не очень практично - дешевле доказать, что оно соответствует. > Потому что от модели до фактов - это всего лишь перевод с одного языка > на другой, причем перевод весьма формальный, тут доказательство > оказывается довольно простым. Интересно проверять соответствие задания > фактов реальности, считая, что набор фактов - это и есть модель. А это > уже формулируется не "написать тест", а "построить тест". В железе, > ага. Но, обычно, не всегда это возможно. Да и чем отличается "железный" генератор (не датчик, а именно генератор состояний датчика) от программного? -- To UNSUBSCRIBE, email to debian-russian-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org Archive: http://lists.debian.org/4ff5ca76.7080...@yandex.ru
