ในสาขาวิทยาการคอมพิวเตอร์เชิงทฤษฎีทฤษฎีแบบจำลองนักแสดง (Actor model theory ) เกี่ยวข้องกับประเด็นเชิงทฤษฎีสำหรับแบบจำลองนักแสดง

แอคเตอร์ (Actor) คือหน่วยพื้นฐานที่เป็นรากฐานของแบบจำลองแอคเตอร์ (Actor model) สำหรับการคำนวณดิจิทัลแบบขนาน เมื่อได้รับข้อความ แอคเตอร์สามารถตัดสินใจในระดับท้องถิ่น สร้างแอคเตอร์เพิ่มเติม ส่งข้อความเพิ่มเติม และกำหนดวิธีการตอบสนองต่อข้อความถัดไปที่ได้รับ ทฤษฎีแบบจำลองแอคเตอร์ประกอบด้วยทฤษฎีเกี่ยวกับเหตุการณ์และโครงสร้างของการคำนวณแบบแอคเตอร์ทฤษฎีการพิสูจน์และแบบจำลองเชิงความหมาย

จากนิยามของ Actor จะเห็นได้ว่ามีเหตุการณ์มากมายเกิดขึ้น ได้แก่ การตัดสินใจในระดับท้องถิ่น การสร้าง Actor การส่งข้อความ การรับข้อความ และการกำหนดวิธีการตอบสนองต่อข้อความถัดไปที่ได้รับ

อย่างไรก็ตาม บทความนี้จะเน้นเฉพาะเหตุการณ์ที่เกี่ยวข้องกับการมาถึงของข้อความที่ส่งไปยังผู้แสดงเท่านั้น

บทความนี้รายงานผลลัพธ์ที่ตีพิมพ์ใน Hewitt [2006]

กฎการนับได้ : จำนวนเหตุการณ์มีได้มากที่สุดเพียงจำนวนนับได้

ลำดับการเปิดใช้งาน ( -≈→) เป็นลำดับพื้นฐานที่จำลองเหตุการณ์หนึ่งที่กระตุ้นอีกเหตุการณ์หนึ่ง (ต้องมีการไหลของพลังงานในข้อความที่ส่งผ่านจากเหตุการณ์หนึ่งไปยังเหตุการณ์ที่มันกระตุ้น)

• เนื่องจากการส่งผ่านพลังงาน ลำดับการกระตุ้นจึงไม่เปลี่ยนแปลงในเชิงสัม พัทธภาพ กล่าวคือ สำหรับเหตุการณ์ทั้งหมดถ้าแล้วเวลาของจะเกิดขึ้นก่อนเวลาของ ในกรอบอ้างอิง เชิงสัมพัทธภาพ ของผู้สังเกตการณ์ทั้งหมดe1e2e1 -≈→ e2e1e2
• กฎแห่งความเป็นเหตุเป็นผลอย่างเคร่งครัดสำหรับการเรียงลำดับการกระตุ้น : เพราะไม่มีเหตุการณ์ใดe -≈→ e...
• กฎการเรียงลำดับเหตุการณ์แบบจำกัด : สำหรับเหตุการณ์ทั้งหมดเซตจะมีจำนวนจำกัดe1{e|e -≈→ e1}

ลำดับการมาถึงของ Actor x( -x→ ) จำลองลำดับ (ทั้งหมด) ของเหตุการณ์ที่ข้อความมาถึงxลำดับการมาถึงถูกกำหนดโดยการตัดสินใจในการประมวลผลข้อความ (มักใช้วงจรดิจิทัลที่เรียกว่าตัวตัดสินใจ ) เหตุการณ์การมาถึงของ Actor อยู่บนเส้นโลก ของมัน ลำดับการมาถึงหมายความว่าแบบจำลอง Actor มีความไม่แน่นอนโดยเนื้อแท้ (ดูความไม่แน่นอนในการคำนวณพร้อมกัน )

• เนื่องจากเหตุการณ์ทั้งหมดของการเรียงลำดับการมาถึงของตัวแสดงxเกิดขึ้นบนเส้นโลกของxดังนั้นการเรียงลำดับการมาถึงของตัวแสดงจึงไม่เปลี่ยนแปลงตามสัมพัทธภาพกล่าวคือสำหรับตัวแสดงxและเหตุการณ์ทั้งหมดถ้าแล้วเวลาของ จะ เกิดขึ้นก่อนเวลาของในกรอบอ้างอิงสัมพัทธภาพของผู้สังเกตการณ์ทั้งหมดe1e2e1 -x→ e2e1e2
• กฎแห่งการมาก่อนอย่างจำกัดในลำดับการมาถึง : สำหรับเหตุการณ์และผู้กระทำ ทั้งหมด เซตนั้นมีจำนวนจำกัดe1x{e|e -x→ e1}

ลำดับการรวม (แทนด้วย→) ถูกกำหนดให้เป็นการปิดแบบส่งผ่านของลำดับการเปิดใช้งานและลำดับการมาถึงของ Actor ทั้งหมด

• ลำดับที่รวมกันนั้นไม่เปลี่ยนแปลงภายใต้สัมพัทธภาพ เพราะมันคือการปิดแบบถ่ายทอดของลำดับที่ไม่เปลี่ยนแปลงภายใต้สัมพัทธภาพกล่าวคือสำหรับเหตุการณ์ทั้งหมดถ้าแล้วเวลาของจะเกิดขึ้นก่อนเวลาของในกรอบอ้างอิงสัมพัทธภาพของผู้สังเกตการณ์ทั้งหมดe1e2e1→e2e1e2
• กฎแห่งความเป็นเหตุเป็นผลอย่างเคร่งครัดสำหรับการเรียงลำดับแบบผสม : เพราะไม่มีเหตุการณ์ใดที่e→e...

ลำดับที่รวมกันนั้นเห็นได้ชัดว่ามีคุณสมบัติถ่ายทอดได้ตามนิยาม

ใน [Baker and Hewitt 197?] มีการตั้งข้อสันนิษฐานว่ากฎข้างต้นอาจนำไปสู่กฎต่อไปนี้:

กฎของสายโซ่จำกัดระหว่างเหตุการณ์ในลำดับแบบผสม : ไม่มีสายโซ่ที่ไม่มีที่สิ้นสุด ( เช่นชุดเหตุการณ์ที่เรียงลำดับเชิงเส้น) ระหว่างสองเหตุการณ์ในลำดับแบบผสม →

อย่างไรก็ตาม [Clinger 1981] ได้พิสูจน์อย่างน่าประหลาดใจว่ากฎของห่วงโซ่จำกัดระหว่างเหตุการณ์ในลำดับแบบผสมนั้นเป็นอิสระจากกฎก่อนหน้านี้กล่าว คือ

ทฤษฎีบท. กฎของสายโซ่จำกัดระหว่างเหตุการณ์ในลำดับแบบผสม ไม่ได้เป็นผลมาจากกฎที่กล่าวไว้ก่อนหน้านี้

บทพิสูจน์ เป็นการเพียงพอที่จะแสดงให้เห็นว่ามีการคำนวณ Actor ที่สอดคล้องกับกฎที่กล่าวไว้ก่อนหน้านี้ แต่ละเมิดกฎของห่วงโซ่จำกัดระหว่างเหตุการณ์ในลำดับแบบผสม

ลองพิจารณาการคำนวณที่เริ่มต้นเมื่อตัวแสดงInitialได้รับStartข้อความ ซึ่งทำให้ตัวแสดงนั้นดำเนินการดังต่อไปนี้

1. สร้างตัวละครใหม่ชื่อGreeter ₁ซึ่งจะได้รับข้อความSayHelloToที่มีที่อยู่ของGreeter ₁
2. ส่งข้อความเริ่มต้นAgainพร้อมที่อยู่ของผู้ทักทายคน_{ที่ 1}

หลังจากนั้น พฤติกรรมของInitialจะเป็นดังนี้เมื่อได้รับAgainข้อความที่มีที่อยู่Greeter _i (ซึ่งเราจะเรียกว่าเหตุการณ์): Againi

1. สร้างแอคเตอร์ใหม่ชื่อGreeter _i+1ซึ่งจะได้รับข้อความSayHelloToที่มีที่อยู่Greeter _i
2. ส่งข้อความเริ่มต้นAgainพร้อมที่อยู่ของGreeter _i+1

เห็นได้ชัดว่าการคำนวณการส่ง ข้อความของ InitialAgain นั้น ไม่มีวันสิ้นสุด

พฤติกรรมของ Actor Greeter _i แต่ละตัว มีดังนี้:

• เมื่อได้รับข้อความSayHelloToที่มีที่อยู่Greeter _i-1 (ซึ่งเราจะเรียกว่าเหตุการณ์) ระบบจะส่งข้อความไปยังGreeter _i-1SayHelloToiHello
• เมื่อได้รับHelloข้อความ (ซึ่งเราจะเรียกว่าเหตุการณ์) มันจะไม่ทำอะไรเลยHelloi

ตอนนี้เป็นไปได้ว่าทุกครั้งและด้วยเหตุนี้Helloi -Greeteri→ SayHelloToiHelloi→SayHelloToi

และ ทุกครั้งเช่นกันดังนั้นAgaini -≈→ Againi+1Againi → Againi+1

นอกจากนี้ กฎทุกข้อที่กล่าวไว้ก่อนหน้านี้เกี่ยวกับกฎแห่งเหตุและผลอย่างเคร่งครัดสำหรับการจัดลำดับแบบผสมผสานนั้นก็ได้รับการปฏิบัติตามแล้ว

อย่างไรก็ตาม อาจมีเหตุการณ์จำนวนอนันต์เกิดขึ้นในลำดับที่รวมกันระหว่างและดังต่อไปนี้:Again1SayHelloTo1

Again1→...→Againi→...${\displaystyle \infty }$...→Helloi→SayHelloToi→...→Hello1→SayHelloTo1

อย่างไรก็ตาม เรารู้จากหลักฟิสิกส์ว่าพลังงานอนันต์ไม่สามารถใช้ไปตามเส้นทางที่จำกัดได้ ดังนั้น เนื่องจากแบบจำลอง Actor นั้นมีพื้นฐานมาจากฟิสิกส์ กฎของห่วงโซ่ที่จำกัดระหว่างเหตุการณ์ในลำดับแบบผสมจึงถูกนำมาใช้เป็นสัจพจน์ของแบบจำลอง Actor

กฎของห่วงโซ่จำกัดระหว่างเหตุการณ์ในลำดับแบบผสมนั้นมีความเกี่ยวข้องอย่างใกล้ชิดกับกฎต่อไปนี้:

กฎแห่งความไม่ต่อเนื่อง : สำหรับเหตุการณ์ทั้งหมดและเซตจะเป็นเซตจำกัดe1e2{e|e1→e→e2}

ในความเป็นจริงแล้ว กฎสองข้อก่อนหน้านี้ได้รับการพิสูจน์แล้วว่ามีความเทียบเท่ากัน:

ทฤษฎีบท [Clinger 1981] กฎแห่งความไม่ต่อเนื่องเทียบเท่ากับกฎแห่งสายโซ่จำกัดระหว่างเหตุการณ์ในลำดับแบบผสม (โดยไม่ต้องใช้สัจพจน์ของการเลือก )

กฎของความไม่ต่อเนื่องตัดความเป็นไปได้ของเครื่องจักร Zeno ออกไป และมีความเกี่ยวข้องกับผลลัพธ์บนเครือข่าย Petri [Best et al. 1984, 1987]

กฎแห่งความไม่ต่อเนื่องบ่งบอกถึงคุณสมบัติของความไม่แน่นอนที่ไร้ขอบเขตการจัดลำดับแบบผสมผสานนี้ถูกใช้โดย [Clinger 1981] ในการสร้างแบบจำลองเชิงความหมายของ Actors (ดูความหมายเชิงความหมาย )

Clinger [1981] ใช้แบบจำลองเหตุการณ์ Actor ที่อธิบายไว้ข้างต้นเพื่อสร้างแบบจำลองเชิงความหมายสำหรับ Actor โดยใช้โดเมนอำนาจต่อมา Hewitt [2006] ได้เพิ่มเวลาการมาถึงลงในแผนภาพเพื่อสร้างแบบจำลองเชิงความหมายที่ง่ายกว่าในทางเทคนิคและเข้าใจได้ง่ายกว่า

• ประวัติช่วงแรกของนักแสดงและนางแบบ
• แบบจำลองนักแสดงและแคลคูลัสกระบวนการ
• การนำโมเดล Actor มาใช้