Re: Несколько вопросов вразброс
05.07.2012 20:45, Artem Chuprina пишет:
> Артём Н. -> debian-russian@lists.debian.org @ Thu, 05 Jul 2012 19:56:29 +0400:
>
> >> >> АН> Да, кстати, Пролог я не понимаю. :-(
> >> >>
> >> >> [...]
> >> >>
> >> >> АН> И на практике: будь всё так хорошо, как вы пишите, все бы уже давно
> >> >> АН> писали на Прологе (по крайней мере, знали бы что это такое). :-)
> >> >> Ну ведь ты же сам написал, что ты его не понимаешь. Думаешь, ты один
> >> >> его не понимаешь?
> >> АН> Если был он был такой хороший, его бы понимали. Потому что, за это
> >> АН> бы платили. :-) И этому учили. C ничуть не проще, чем Пролог. Он
> >> АН> просто имеет другую парадигму. "Развёрнутую" на 180. У машины
> >> АН> вывода есть свои недостатки, ограничения и своя область
> >> АН> применения. По какой-то совокупности причин, Пролог не нашёл
> >> АН> широкого применения (хотя к нему интерес то падал, то
> >> АН> возобновлялся).
> >> Понятность среднему хомосапиенсу, как и всякое другое качество, не
> >> бывает бесплатной. И отнюдь не на всех задачах оно важно. Если средний
> >> хомосапиенс не может понять саму задачу, то понятность ему инструмента
> >> для ее решения ценности не имеет.
> АН> Хм... И про какие задачи, которые выше понимания среднего, идёт
> АН> речь? Т.е. где сейчас реально используются Пролог системы?
>
> Вот это уже не вполне ко мне вопрос, я сам на Прологе не работаю.
> Насколько я понимаю, целевая его ниша - это задачи аналитического типа.
> Ответ на вопросы "что из этих данных может следовать?"
>
> >> >> Потому что правила
> >> >> рассуждений с этими законами правильны настолько, насколько правильна
> >> >> математика (если ты знаешь, что именно формулируется в теореме Геделя,
> >> >> то ты понимаешь это условие).
> >> АН> Думаю, что частично понимаю.
> >> АН> Пролог - аксиоматическая система.
> >> АН> И, следовательно, любая система, построенная в нём, - такая же.
> >> АН> Т.е., если "И" - аксиома Пролог, которая задаёт истинность А и Б, при истинности
> >> АН> и А, и Б, все аксиомы, заданные на её основе будут истинны в границах данной
> >> АН> системы.
> >> АН> Доказательство истинности этой аксиомы и непротиворечивости правил её
> >> АН> взаимодействия с остальными относятся к доказательству истинности и
> >> АН> непротиворечивости Булевой алгебры.
> >> АН> В данном случае, математика правильна априори.
> >> АН> Так?
> >> Последнее предложение неверно. Скажем так, мы верим, что математика
> >> правильна (в том смысле, что доказанный в ней результат о некоторой
> >> модели можно в рамках ограничения этой модели применить к реальности).
> >> Гедель нам доказал, что ни на что, кроме веры, мы не можем тут
> >> положиться даже на предмет ее внутренней непротиворечивости, не говоря
> >> уж о применениях к реальности.
> АН> Я понимаю, что Гедель показал это для формальной системы, которой
> АН> является математика. Но, если используется Пролог, то решается
> АН> практическая задача. В таком случае, математика используется
> АН> потому, что она работает. Т.е. предполагается, что она верна? Это
> АН> аксиома. :-)
>
> Очень полезно все же помнить, что предположение о правильности
> математики - это тоже предположение. Такое же, как предположение о том,
> что выполняется закон сохранения импульса. Кстати, законы рассуждений,
> используемые в Прологе, не эквивалентны тем, которым нас учат в школе и
> даже в вузе.
В смысле? Там есть что-то новое? :-) Это же обычная "машина вывода", как и
логика самая "обычная.
> >> >> А вот как соотносится твоя модель,
> >> >> выраженная в нелогических аксиомах, с реальностью - это уже не к
> >> >> Прологу.
> >> АН> Но в точности тоже самое возможно сказать и о других языках. А
> >> АН> тесты нужны именно для того, чтобы проверить соответствие модели и
> >> АН> реальности. Там тоже самое, даже такие же побочные эффекты могут
> >> АН> быть. И программа, на нём написанная не является правильной только
> >> АН> потому, что она написана на Пролог. Просто тестами надо покрывать
> >> АН> факты и правила, а не функции и процедуры или я не прав?
> >>
> >> В выводе - да, прав. Но надо учитывать, что большинство наших тестов
> >> для других языков таки работают внутри модели, а не проверяют ее
> >> соответствие реальности. То есть для прологовской программы не имеют
> >> смысла. Природа тестов для прологовской программы должна быть
> >> существенно иной, нежели привычно.
> АН> Хм... А как тест может работать не внутри модели? Программа -
> АН> модель. Даже, если тест получает данные извне, он всё-равно
> АН> работает в данной модели.
>
> Не обязательно в данной. Это существенно. Скажем, тест, который
> получает сигнал с реального датчика, сует его в программу, получает из
> программы команду на управление реальным железом, выдает ее в железо, и
> потом измеряет угол его поворота, например, другим датчиком, таки
> выходит за пределы той же модели.
Ну да. Разве что так. Но причём здесь Пролог?
> И его работа уже существенно ближе к реальности, чем модель, в которой
> написана программа.
Но, кажется, это две стадии тестирования?
И нельзя тестированием с реальным датчиком заменить тестирование с "эмулятором".
> АН> Чем тут отличается Пролог от императивного языка, например? Здесь
> АН> я просто вижу те же самые ошибки человека: неверное задание правил
> АН> (неполнота, неточность или ошибочность) и неверное задание фактов.
> АН> Что и должны покрывать тесты. Ведь так?
> Так. А теперь внимание: что значит словосочетание "верное задание
> фактов"? Скорее всего, тестировать соответствие этого задания опять же
> модели не очень практично - дешевле доказать, что оно соответствует.
> Потому что от модели до фактов - это всего лишь перевод с одного языка
> на другой, причем перевод весьма формальный, тут доказательство
> оказывается довольно простым. Интересно проверять соответствие задания
> фактов реальности, считая, что набор фактов - это и есть модель. А это
> уже формулируется не "написать тест", а "построить тест". В железе,
> ага.
Но, обычно, не всегда это возможно. Да и чем отличается "железный" генератор (не
датчик, а именно генератор состояний датчика) от программного?
Reply to: