AI 中文总结
本文针对编排式编程中端点投影定理证明困难的问题，通过设计基于进程局部视图的编排新语义及相关预序关系，给出了端点投影定理的模块化证明，使其更简单并增进了对编排式编程理论的理解。
AI 中文摘要
端点投影（EPP）定理是编排式编程的基石，它表明每个编排都可投影到正确实现它的进程网络。证明EPP非常困难，现有证明复杂且非模块化。本文通过为编排设计基于进程局部视图的新语义，以及编排与网络间扩展双模拟以处理分布式进程中选择知识传播的新预序关系，调和这种不匹配，给出EPP的模块化证明，比现有证明更简单且对编排式编程理论有更好见解。
英文摘要
The Endpoint Projection (EPP) theorem is a cornerstone of choreographic programming. It states that every choreography can be projected to a network of processes that correctly implements it. Proving EPP is notoriously difficult, and existing proofs are complex and non-modular because of the mismatch between the global view of choreographies and the local view of processes. In this article, we show how to reconcile this mismatch by designing a new semantics for choreographies that is built on the local view of processes, as well as a new preorder relation between choreographies and networks that extends bisimulation to deal with the propagation of knowledge of choice among distributed processes. As a result, we can give a modular proof of EPP, which is conceptually simpler than existing ones and also provides better insights on the theory of choreographic programming.
