Правдивая абстрактная мера для стоимости выполнения цели Пролога

Question

Далее я рассматриваю только программы на чистом прологе. Это означает, что я не говорю о побочных эффектах и ​​вызовах ОС, которые оставляют сферу логики, чтобы делать что-то, что не может наблюдаться изнутри Пролога.

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

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

Для любой заданной цели Пролога G обозначим через t(G): T→ R фактическое время выполнения G в данной системе Пролога на конкретном оборудовании, то есть функцию от термов Хербранда до действительных чисел. Будем называть меру α: T→ R истинной тогда и только тогда, когда t(G) ≈ α (G) для всех G, в том смысле, что значения отличаются коэффициентом, ограниченным константой для всех целей G и всеми "реалистичными" типы аппаратного обеспечения (я должен оставить этот последний пункт слегка недоопределенным, но для простоты я предполагаю, что та же реализация Prolog работает примерно так же на "типичном" оборудовании. Я знаю, что это на самом деле не так, и то же самое Реализация может демонстрировать резко отличающиеся характеристики на разных типах аппаратного обеспечения. Если это так, ограничьте определение подмножеством типов аппаратного обеспечения, где реализация выполняется "примерно" одинаково.)

Насколько я знаю, число логических выводов, как правило, не является истинной мерой фактического времени выполнения цели Пролога, в частности потому, что время, которое требуется для выполнения объединений, не измеряется им. Можно построить случаи, когда разница между этой мерой и фактическим временем выполнения больше не ограничена константой.

Поэтому мой вопрос: есть ли правдивая абстрактная мера для времени выполнения цели Пролога? Если он вообще не существует, пожалуйста, укажите значимое подмножество программ Prolog, где можно определить такую ​​меру. Например, путем ограничения типов объединений, которые могут произойти.

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

Answer 1

Проблема мер сложности видна здесь в полном расцвете. Но губы - все еще полезное измерение. Вы не получаете:

LIPS ~ TIME

Но вы получаете:

LIPS * DEPTH * COUNT ~ TIME

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

Это такая же абстракция, как если бы вы сказали, что сложение занимает один временной шаг, но на самом деле мы знаем, что время для добавления двух больших чисел зависит от размера больших чисел. Здесь термины и положения играют роль bignums.

Это полезно? Определенно да! Например, если у вас есть два алгоритма, и вы видите, что и глубина, и количество одинаковы, вы можете пойти по губам, чтобы сравнить их.