Принцип работы акторной логической машины

Принцип работы акторной логической машины основан на следующих пяти базовых идеях:
  1. стандартная стратегия управления чистого Пролога с поиском в глубину;
  2. разделение И-дерева программы на акторы;
  3. локализация данных в акторах;
  4. задержка восстановления состояния акторов;
  5. нейтрализация и повторное доказательство акторов.
Стандартная стратегия управления чистого Пролога с поиском в глубину является частным случаем стратегии управления Акторного Пролога. При этом логические акторы - до тех пор, пока не используются специальные возможности, предоставляемые акторной логической машиной, - являются всего лишь "декоративной раскраской" И-дерева, не влияющей на стратегию управления.

Согласно операционной семантике акторной логической машины, актор может находиться в одном из трех состояний (см.рис.2):

Figure 1.

Рис.2. Состояния логического актора.
  1. Актор является "активным", если доказательство этой подцели еще не окончено и продолжается в данный момент времени.
  2. В том случае, если его доказательство благополучно завершилось успехом, актор становится "доказанным".
  3. Актор, предыдущее доказательство которого отменено, а повторное еще не началось, является "нейтральным".

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

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

Таким образом, процесс доказательства каждого отдельного актора программы включает следующие фазы:
  1. автономное доказательство актора;
  2. взаимодействие с другими акторами программы:
    1. проверка согласованности акторов;
    2. нейтрализация акторов;
    3. повторное доказательство нейтральных акторов.

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

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

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

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

Кроме того, в случае отката программы восстановление состояния некоторых ее акторов может быть отложено до тех пор, пока не возникнут реальные противоречия между их текущим состоянием и новыми результатами логического вывода (эта идея является основой для логической интерпретации необратимых процессов).
Back to Auto Abstract
Back to Research Divisions
IRE RAS Homepage