Кіріспе

Теориялық компьютерлік ғылымда актерлік модель теориясы актерлік модельдің теориялық мәселелерін зерттейді. Актерлер – бір мезгілдегі цифрлық есептеудің актерлік моделіне негіз болатын бастауыш элементтер. Алған хабарламаға жауап ретінде актерлер жергілікті шешімдер қабылдай алады, жаңа актерлер құра алады, хабарламалар жібере алады және келесі хабарламаға қалай жауап беру керектігін анықтай алады. Актерлік модель теориясы актерлік есептеулердің оқиғалары мен құрылымдарының теорияларын, олардың дәлелдеу теориясын және денотациялық модельдерді қамтиды.

Оқиғалар және олардың реттелгендігі

Актердің анықтамасынан көптеген оқиғалардың болатынын көруге болады: жергілікті шешімдер қабылдау, Актерлерді құру, хабарлама жіберу, хабарламалар алу және келесі алынған хабарламаға қалай жауап беру керектігін анықтау. Дегенмен, бұл мақала тек Актерге жіберілген хабарламаның келуіне байланысты оқиғаларға назар аударады. Бұл мақалада Hewitt [2006] еңбегінде жарияланған нәтижелер келтірілген. Саналатындық заңы: Оқиғалардың саны санаулы ғана болуы мүмкін.

Белсенділеуді тапсыру

Активация тәртібі (≈→) – бір оқиғаның екіншісін іске қосатын негізгі тәртіп (бір оқиғадан оны іске қосатын оқиғаға хабар алмасу кезінде энергия ағыны болуы тиіс). Энергияның берілуіне байланысты, активация тәртібі релятивистік түрде өзгермейді; яғни, барлық оқиғалар e1, e2 үшін, егер e1 ≈→ e2 болса, онда e1 уақыты барлық бақылаушылардың релятивистік есептеу жүйелерінде e2 уақытынан бұрын болады. Активация тәртібі бойынша қатаң себеп-салдар заңы: Ешқандай оқиға үшін e ≈→ e болмайды. Активация тәртібі бойынша шекті алдын-ала тұру заңы: Барлық оқиғалар e1 үшін {e | e ≈→ e1} жиыны шекті.

Келу тәртібі

Actor x (x→ ) -тің келу реті x-ке хабардың келген оқиғалардың (жалпы) тізбегін көрсетеді. Келу реті хабарларды өңдеу кезіндегі арбитраж арқылы анықталады (көбінесе арбитр деп аталатын цифрлық тізбек қолданылады). Актердің келу оқиғалары оның әлемдік сызығында орналасады. Келу реті Актер моделінің ішкі белгісіздігін білдіреді (параллель есептеулердегі белгісіздікке қараңыз). x актердің келу ретімен байланысты барлық оқиғалар x-тің әлемдік сызығында болғандықтан, актердің келу реті релятивистік тұрақтылыққа ие. Яғни, барлық x актерлер мен e1, e2 оқиғалары үшін, егер e1 x→ e2 болса, онда e1 уақыты барлық бақылаушылардың салыстырмалы анықтамалық жүйелерінде e2 уақытынан ертерек болады. Келу ретіндегі шекті алдын алу заңы: барлық e1 оқиғалары және x актерлер үшін {e|e x→ e1} жиыны шекті.

Денотациялық семантика

Клингер [1981] жоғарыда сипатталған Актер оқиғасы моделін қуат домендерін қолдана отырып, Актерлерге арналған денотациялық модель құру үшін пайдаланды. Содан кейін Хьюитт [2006] диаграммаларды келу уақыттарымен толықтырып, түсінуге оңай, техникалық тұрғыдан қарапайым денотациялық модельді жасады.