# 2022 Project-onda (仮)

# 2022/5/9

- CC'21 artifact を Docker で動かしてみよう
- うごいた
- https://github.com/STScript-2020/cc21-artifact
- Naughts and Crosses のサンプル
- https://github.com/STScript-2020/cc21-artifact/blob/main/protocols/NoughtsAndCrosses.scr

- MacBook側のファイルシステムを docker コンテナ内でマウントしてみよう
　- 参考: https://qiita.com/karadaharu/items/0fdd9b4b373a8de656ab
　- `docker run -it` に オプション `-v /Users/owner/for_docker:/for_docker` を付ける
　- ここでは `-v /Users/onda/cc21_artifact:/macbook` とか？

- 論文を読もう

# 2022/4/26
* 論文紹介和訳
## Abstract（要約）

　現代のプログラミングはブラウザクライエントとサーバー間の相互作用の調整に関与している。

> Typically, the interactions in web-based distributed systems are informally described, making it hard to ensure correctness, especially communication safety, i.e. all endpoints progress without type errors or deadlocks, conforming to a specified protocol.

一般的に、ウェブベースの分散システムにおける通信は非形式的に記述され、正しさ(特に通信の安定性、つまり全てのエンドポイントが、型エラーやデットロックする事なく進行し、指定されたプロトコルに適合する)を確かめる事が困難である。

> We present STScript, a toolchain that generates TypeScript　APIs for communication-safe web development over WebSockets, and RouST, a new session type theory that supports　multiparty communications with routing mechanisms.

我々はSTScriptという、websocketを使用した安全に通信するweb開発のためにTypeScript APIs(ソフトウェアの機能や管理データを外部のプログラムから呼び出して利用する規約)を生成するツールチェーン(プログラムの集合みたいなもの)と、RouSTという、ルーティングメカニズムで多者間の通信をサポートする新しいセッション型の理論を提案する。

※webアプリのルーティングの例:
- http://www.example.com/search -> search() を呼び出す
- http://www.example.com/register -> register() を呼び出す
- …など、URLのパス文字列/クエリ文字列に、webアプリの特定の機能 (関数) を対応づける仕組みのことをいう。

> STScript provides developers with TypeScript APIs generated from a communication protocol specification based on RouST. The generated APIs (1)build upon TypeScript concurrency practices, (2)complement the event-driven style of programming in full-stack web development, (3)and are compatible with the Node.js runtime for server-side endpoints and the React.js framework for browser-side endpoints.

STScriptはRouSTに基づいた通信プロトコルの仕様から生成されたTypeScript APIsを開発者に提供する。生成されたAPIsはTypeScriptの並行プログラミングの実践の基づいて構築されており、フルスタックのweb開発におけるプログラミングのイベント駆動スタイルを補い、サーバー側のエンドポイントのNode.jsのランタイムと、ブラウザ側のエンドポイントのReact.jsのフレームワークに互換性がある。

- ランタイム：アプリの開発・実行の機能を備えたソフトウェアから、実行機能のみを取り出したプログラム、または開発ツールの実行ファイル群。単に実行時という意味もある。

>RouST can express multiparty interactions routed via an intermediate participant. It supports peer-to-peer communication between browser-side endpoints by routing communication via the server in a way that avoids excessive serialisation. RouST guarantees communication safety for endpoint web applications written using STScript APIs.

RouSTは中間の参加者を経由した多者間の相互関係を表現できる。RouSTは過度の(serialize)連続化を避ける方法によりサーバー経由で通信をルーティングすることで、ブラウザ側のエンドポイント間のpeer-to-peer通信をサポートする。RouSTはSTScript APIsで記述されたエンドポイントウェブアプリケーションの通信安全性を保障する。

>We evaluate the expressiveness of STScript for modern web programming using several production-ready case studies deployed as web applications.

　我々はwebアプリケーションとして活用された、いくつかのリリース可能な事例研究を使って現代のwebプログラミングにとっての、STScriptの表現力を評価していく。

- STScript
* TypeScript APIsのツールチェーン。
* web開発におけるプログラミングのイベント駆動スタイルを使う（？）
* Node.jsランタイム（サーバー側）とReact.jsのフレームワーク（ブラウザ側）に互換性がある。

- RouST(routed multiparty session types theory)
* 多者間通信をサポートする新たなセッション型理論。
* 中間の参加者を経由した多者間の相互関係を表現できる。
* 過度のシリアライズを避けてサーバー経由で通信をルーティングする
* ブラウザ側のエンドポイント間のp2p通信をサポートする。
* STScript APIsで記述されたエンドポイントウェブアプリケーションの通信安全性を保障する。

## 1.Introduction （序論）

>Web technology advancements have changed the way people use computers. Many services that required standalone applications, such as email, chat, video conferences, or even games, are now provided in a browser.

web技術の進化は人々のコンピュータの使い方を変えた。email、チャット、ビデオ会議、ゲームなどネットとは独立していたアプリケーションを必要としていた多くのサービスが、今ではブラウザで提供されるようになった。

>While the Hypertext Transfer Protocol (HTTP) is widely used for serving web pages, its Request-Response model limits the communication patterns — the server may not send data to a client without the client first making a request.

HTTPはWebページを提供することに使われているが、そのRequest-Responseモデルによって通信パターンが制限される。HTTPでは、クライアントが初めにサーバーにリクエストを送らなければ、データを送信することができない。

>The WebSocket Protocol [12] addresses this limitation by providing a bi-directional channel between the client and the server, akin to a Unix socket. Managing the correct usage of WebSockets (1)introduces an additional concern in the development process, due to a lack of WebSocket testing tools, (2)requiring an (often ad-hoc) specification of the communication protocol between server and clients.

　WebSocketプロトコルは、Unixソケットに類似した、クライアントとサーバー間の双方向チャネルを提供することでHTTPにあった制限を対処する。Websocketの正しい使い方を管理することは、WebSocketの試験ツールがないため、開発プロセスにおいて更なる懸念が発生する。これにより、サーバーとクライアント間の通信プロトコルの(しばしばアドホックな)仕様作成を要求する。


>Consider the scenario in Fig. 1, where an online travel agency operates a “travelling with a friend” scheme (ignoring the blue dashed arrows). It starts when a traveller (B) suggests a trip destination to their friend (A), who then queries the travel agency (S) if the trip is available. If so, the friends discuss among themselves whether to accept or reject the quoted price. If the trip was unavailable, the friends start again with a new destination.

図1のシナリオで、あるオンライン旅行会社が「友達と一緒に旅行する」事業計画を運営する場合を考えてみる（青い矢印は無視）。この計画は、旅行者（B）が友人（A）に旅行先を提案し、友人が旅行できるかを旅行会社（S）に問い合わせるところから始まる。旅行できる場合は、友人同士で見積もり金額を受け入れるか拒否するかを話し合う。もしその旅行が現実的でなかった場合は、友人たちは新しい旅行先でやり直す。

>An implementation of the travel agency protocol may contain programming errors, risking communication safety. For example, the following implementation of the client-side endpoint for traveller A sending a quote to traveller B.

旅行会社規約の実施には、プログラミングエラーが含まれている場合があり、通信の安全性が損なわれる危険性がある。例えば、旅行者Aが旅行者Bに見積もりを送るクライアント側エンドポイントの実装は以下の通りである。


>There are subtle errors that violate the communication protocol, but these bugs are unfortunately left for the developer to manually identify and test against:

通信プロトコルに違反する微妙なエラーもあるが、これらのバグは不幸ながら開発者が手作業で特定し、テストすることに委ねられる。

>**Communication Mismatch**
>Whilst the input field mandates a numerical value (Line 1) for the quote, the value from the input field is actually a string. If B expects a number and performs arithmetic operations on the received payload from A, the type mismatch may be left hidden due to implicit type coercion and cause unintended errors.

**通信の不一致**
入力欄では見積もりに数値（１行目）を指定することになっているが、入力欄の値は実際には文字列である。もしBが数値を期待し、Aから受け取ったペイロードに対して算術演算を実行した場合、暗黙の型強制によって型の不一致が隠され、意図しないエラーを引き起こす可能性がある。

>**Channel Usage Violation**
>As B may take time to respond, A can experience a delay between sending the quote and receiving a response. Notice that the button remains active after sending the quote — A could click on the button again, and send additional quotes (thus reusing the communication channel), but B may be unable to deal with extra messages.

**チャネル使用法の違反**
Bは返答に時間がかかる可能性があるため、Aは見積もりを送ってから返答を受け取るまで遅延が発生する可能性がある。見積もりを送った後もボタンはアクティブなままであることに気をつけるーAはもう一度ボタンをクリックすることができ、追加の見積もりを送ることができる（こうして通信を再利用する）が、Bは余分なメッセージに対応出来ないかもしれない。

>**Handling Session Cancellation**
>An additional concern is how to handle browser disconnections, as both travellers can freely close their browsers at any stage of the protocol. Suppose S temporarily reserves a seat on A’s query. If A closes their browser, the developer would need to make sure that A notifies S prior to disconnecting, and S needs to implement recovery logic (e.g. releasing the reserved seat) accordingly.

**セッションのキャンセルに対応**
更なる問題は、旅行者がプロトコルのどの段階でも自由にブラウザを閉じることができるため、ブラウザの切断をどのように処理するかである。SがAの問い合わせに対して一度席を確保したとする。もしAがブラウザを閉じたら、開発者はAが通信を切断する前にSに通知することを確かめる必要があり、Sはそれに対してリカバリーロジック（例えば予約席の解放）を実行する必要がある。

* webの進化は人々のコンピュータの使い方を変えてきた
* WebSocketのプロトコルはHTTPでは出来なかったサーバーとクライアントとの双方向通信を可能にした。ただ、WebSocketの試験ツールがないため、開発プロセスで懸念点が残る。よってサーバーとクライアント間の通信でアドホックな仕様の構築が必要となる。
* 通信プロトコルに反する微妙なエラーはプログラマーが手作業で直す必要がある。
* エラー例、対応例　　通信の不一致、チャネル使用法の違反、セッションのキャンセルに対応

>To prevent these errors and ensure deadlock-freedom, we propose to apply session types [14, 15] into practical interactive web programming. The scenario described in Fig. 1 can be precisely described with a global type using the typing discipline of multiparty session types (MPST) [15]. Well-typed implementations conform to the given global protocol, are guaranteed free from communication errors by construction.

これらのエラーを防ぎ、デッドロックのない状態を確保するために、我々は実用的な相互作用のあるWebプログラミングにセッション型を適用することを提案する。図1で表されたシナリオは、マルチパーティセッション型（MPST）の型付けの規律を用いてグローバル型で正しく記述できる。型付けされた実装は、グローバルプロトコルに従い、構造による通信エラーがないことを保証する。

>Whereas session type programming is well-studied [1], its application on web programming, in particular, interactive web applications, remains relatively unexplored. Integrating session types with web programming has been piloted by recent work [13, 20, 24], yet none are able to seamlessly　implement the previous application scenario: Fowler [13] uses binary (2- party) session types; and King et al. [20] require each non-server role to only communicate to the server, hence preventing interactions between non-server roles (cf.talking to a friend in the scenario).

セッション型プログラミングはよく研究されているが、Webプログラミング、特に相互作用のあるwebアプリケーションは比較的開拓されていないままである。セッション型とwebプログラミングの統合は最近の研究で試されているが、まだ以前のアプリケーションのシナリオをシームレスに実装できるものは何もない。Fowlerはバイナリセッション型を使用し、Kingらは、それぞれの非サーバーの役割はサーバーに通信することのみを要求し、非サーバーの役割間の相互作用（例：シナリオにおける友人との会話）を防ぐ。

>The programming languages used in these works are, respectively, Links [8] and PureScript [28], both not usually considered mainstream in the context of modern web programming. The Jolie language [24] focuses more on the server side, with limited support for an interactive front end of web applications.

これらの研究で使われているプログラミング言語は、それぞれ、LinksとPureScriptで、どちらも現代のWebプログラミングの文脈では通常主流とは考えられていない。Jolie言語は、サーバー側により重点をおき、Webアプリケーションのインタラクティブなフロントエンドを限定的にサポートする。

- 上のエラーを防ぐために、相互作用のあるWebプログラミングにセッション型を適用する。
- 通信のシナリオはグローバル型で記述でき、型付けされたプログラムはグローバルプロトコルに従い、通信エラーがないことが保証されている。
- セッション型プログラミングはよく研究されている（Fowler、King）が、Webプログラミング、特に相互作用のあるwebアプリケーションは比較的開拓されていない。これらの研究で使われている言語は現代は主流ではない。

>This paper presents a novel toolchain, Session TypeScript (STScript), for implementing multiparty protocols safely in web programming. STScript integrates with modern tools and practices, utilising the popular programming language TypeScript, front end framework React.js and back end runtime Node.js.

本論文では、Webプログラミングにおけるマルチパーティプロトコルを安全に実装するための新しいツールチェーン、セッション型 TypeScript（STScript）を提案する。STScriptは、人気のプログラミング言語TypeScript、フロントエンドフレームワークReact.js、バックエンドランタイムNode.JSを利用し,現代のツールとプラクティス（事例？）を統合する。

>Developers first specify a multiparty protocol and we generate correct-by-construction APIs for developers to implement the protocol. The generated APIs use WebSocket to establish communication between participants, utilising its flexibility over the traditional HTTP model.

開発者は初めにマルチパーティプロトコルを指定し、我々は開発者がそのプロトコルを実装するためのcorrect-by-construction　APIを生成する。生成されたAPIは、参加者間の通信を確立するためにWebSocketを使用し、伝統的なHTTPモデルに対する柔軟性を利用している。

- correct-by-construction
建設による修正
コードを生成する前に、設計の数学的モデルを構築する。このモデルは、提案されたソリューションについて推論するために使用され、必要なすべての機能が提供され、正しい動作が示されることを保証する。

>When developers use our generated APIs to correctly implement the protocol endpoints, STScript guarantees the freedom from communication errors, including deadlocks, communication mismatches, channel usage violation or cancellation errors.

開発者が、我々が生成したAPIを使用してプロトコルのエンドポイントを正しく実装する場合、STScriptはデッドロック、通信の不一致、チャネルの使用違反、キャンセルエラーなどを含む通信エラーからの自由を保証する。

>Our toolchain is backed by a new session theory, a routed multiparty session types theory (RouST), to endow servers with the capacity to route messages between web clients. The new theory addresses a practical limitation that WebSocket connections still require clients to connect to a prescribed server, constraining the ability for inter-client communication.

我々のツールチェーンは、新しいセッション理論であるrouted multiparty session types theory (RouST)によって支えられ、webクライアント間のメッセージをルーティングする能力をサーバーに与える。この新しい理論では、WebSocket接続はクライアントに所定のサーバーに接続することを要求し、クライアント間の通信に制約がある、という事実上の制限を処理する。

>To overcome this, our API routes inter-client messages through the server, improving the expressiveness over previous work and enabling developers to correctly implement multiparty protocols, as we show with blue dashed arrows in Fig. 1. In our travel agency scenario, the agency plays the server role: it will establish WebSocket channels with each participant, and be tasked with routing all the messages between the friends.

これを克服するために、我々のAPIはクライアント間のメッセージをサーバー経由でルーティングし、以前の研究よりも表現力が向上し、図１の青色の破線矢印で示しているように、開発者が正しくマルチパーティプロトコルを実装できるようになった。旅行代理店のシナリオでは、代理店がサーバーの役割を果たす。代理店は各参加者のWebSocketチャネルを確立し、友人間の全てのメッセージをルーティングすることを仕事とする。

>We formalise this routing mechanism as RouST and prove deadlock-freedom of RouST and show a behaviour-preserving encoding from the original MPST to RouST. The formalism and results in RouST directly guide a deadlock-free protocol implementation in Node.js via the router, preserving communication structures of the original protocol written by a developer.

我々はこのルーティングメカニズムをRouSTとして定式化し、RouSTのデッドロックフリーを証明し、元のMPSTからRouSTへの振舞い保存（behaviour-preserving）符号化を示す。RouSTの形式論と結果は、開発者が記述した元のプロトコルの通信構造を維持したまま、ルーターを介したNode.jsでデッドロックフリーなプロトコルの実装を直接的に導く。

>Finally, we evaluate our toolchain (STScript) by case studies. We evaluate the expressiveness by implementing a number of web applications, such as interactive multiplayer games (Noughts and Crosses, Battleship) and web services (Travel Agency) that require routed communication.

最後に、研究事例によって我々のツールチェーン（STScript）を評価する。多人数参加型で相互関係のあるゲーム（Noughts and Crosses, Battleship）や、ルーティング通信を必要とするWebサービス(Travel Agency)など、いくつかのWebアプリケーションを実装し、その表現力を評価する。

- WebプログラミングでMPSTを安全に実装するためのツールチェーンとしてSTScriptを提案。
- マルチパーティプロトコルを指定して、それを実装するためにcorrect-by-construction　APIを生成する
- STScriptは、新しいセッション理論であるRouSTによって支えられ、webクライアント間のメッセージをルーティングする能力をサーバーに与える。

>*Contributions and Structure of the Paper. *
>§ 2 presents an overview of our toolchain STScript, which generates APIs for communication-safe web applications in TypeScript from multiparty protocol descriptions. § 3 motivates how the generated code executes the multiparty protocol descriptions,and present how STScript prevents common errors in the context of web applications. § 4 presents RouST, multiparty session types (MPST) extended with routing, and define a trace-preserving encoding of the original MPST into RouST. § 5 evaluates our toolchain STScript via a case study of Noughts and Crosses and performance experiments. § 6 gives related and future work.

*論文の貢献度と構成*
2章では、マルチパーティプロトコルの記述からTypeScriptで通信の安全なWebアプリケーションのAPIを生成するツールチェーンSTScriptの概要を紹介する。3章では、生成されたコードがどのようにマルチパーティプロトコルの記述を実行するかを説明し、STScriptがWebアプリケーションの文脈でよくあるエラーをどのように防いでいるかを紹介する。4章では、MPSTをルーティングで拡張したRouSTを紹介し、オリジナルのMPSTをRouSTに追跡可能に符号化することを定義する。5章では、Noughts and Crossesのケーススタディと性能実験によって我々のツールチェーンであるSTScriptを評価する。6章では、関連および今後の課題について述べる。

## 2.Overview（概論）
>In this section, we give an overview of our code generation toolchain STScript (Fig. 2), demonstrate how to implement the travel agency scenario (Fig. 1) as a TypeScript web application, and explain how STScript prevents those errors.

この節では、コード生成ツールチェーンであるSTScriptの概要（図２）を与え、旅行会社のシナリオ（図１）をTypeScriptのwebアプリケーションとして実装する方法を示し、STScriptがそれらのエラーを防ぐ方法について説明する。

>**Multiparty Session Type Design Workflow.**
>Multiparty　session types (MPST) [15] use a top-down design methodology (Fig. 3). Developers begin with specifying the global　communication pattern of all participants in a global type　or a global protocol. The protocol is described in the Scribble protocol　description language [16, 31, 34]. We show the　global protocol of the travel agency scenario (in § 1) in Fig. 4.

**マルチパーティセッション型の設計ワークフロー**
MPSTはトップダウン型の設計手法を採用している（図３）。開発者はまず、グローバル型やグローバルプロトコルで参加者全員のグローバルな通信パターンを指定することから始める。そのプロトコルはプロトコル記述言語Scribbleで記述されている。図４に旅行代理店のシナリオのグローバルプロトコルを示す。


>The Scribble language provides a user-friendly way to describe the global protocol in terms of a sequence of message exchanges between roles. A message is identified by its label (e.g. Suggest, Query, etc), and carries payloads (e.g. number, string, etc). The choice syntax (e.g. Line 4) describes possible branches of the protocol – in this case, the Server may respond to the query either with Available, so the customer continues booking, or with Full, so the customer retries by restarting the protocol via the do syntax (Line 13).

Scribble言語は、ロール間のメッセージ交換の順序（sequence）の観点からグローバルプロトコルを記述するための使いやすい方法を提供する。メッセージはラベル（例：Suggest、Query）で識別され、ペイロード（例：数値、文字列）を運ぶ。選択構文（例：図４の4行目）は、プロトコルの可能な分岐を記述するものであるーこの場合、サーバーは問い合わせに対してAvailableと応答し、顧客は予約を続行するか、Fullと応答し、顧客はdo構文（13行目）でプロトコルを再開することで予約を再試行する。

>In this scenario, we designate the roles A and B as client roles, and role S as a server role. Participating endpoints can obtain their local views of the communication protocol, known as local types, via projection from the specified global type (Fig. 3). The local type of an endpoint can be then used in the code generation process, to generate APIs that are correct by construction [17, 20, 35].

このシナリオでは、ロールA,Bをクライアントロール、ロールSをサーバーロールと名付ける。参加するエンドポイントは、指定されたグローバル型の射影によって、ローカル型と呼ばれる通信プロトコルのローカルビューを得ることができる（図３）。エンドポイントのローカル型は、コード生成のプロセスに使われ、構成上正しいAPIを生成することができる。

>The code generation toolchain STScript (Fig. 2) follows the MPST design philosophy. In STScript, we take the global protocol as inputs, and generate endpoint code for a given role as outputs, depending on the nature of the role. We use the Scribble toolchain for initial processing, and use an endpoint finite state machine (EFSM) based code generation technique targeting the TypeScript Language.

コード生成ツールチェーンSTScript（図２）は、MPSTの設計思想を引き継いでいる。STScriptでは、グローバルプロトコルを入力とし、与えられた役割に応じたエンドポイントコードを出力として生成する。初期処理にはScribbleツールチェーンを使用し、TypeScript Languageをターゲットとしたエンドポイント有限オートマトン（EFSM）ベースのコード生成技術を使用している。

- MPSTのワークフロー
- MPSTはトップダウン型の設計手法
- グローバル型やグローバルプロトコルを記述して参加者全員の通信パターンを指定する
- 参加するエンドポイントは、指定されたグローバル型の射影によって、ローカル型を得る
- STScriptはMPSTの設計を引き継いでおり、グローバルプロトコルを入力として、それに従ったエンドポイントコードを出力とする

>**Targeting Web Programming.**
>The TypeScript [2] programming language is used for web programming, with a static type system and a compiler to JavaScript. TypeScript programs follow a similar syntax to JavaScript, but may contain type annotations that are checked statically by the TypeScript type-checker. After type-checking, the compiler converts TypeScript programs into JavaScript programs, so they can be run in browsers and other hosts (e.g. Node.js).

**webプログラミングをターゲットにする**
プログラミング言語TypeScriptは、静的な型システムとJavaScriptへのコンパイラを備え、Webプログラミングに使用されている。TypeScriptのプログラムはJavaScriptに似た構文に従うが、TypeScriptの型検査によって静的にチェックされる型注釈を含むかもしれない。型検査の後、コンパイラはTypeScriptプログラムをJavaScriptプログラムに変換するため、ブラウザや他のホスト（例：Node.js）で実行できるようになる。

>To implement a wide variety of communication patterns, we use the WebSocket protocol [12], enabling bi-directional communication between the client and the server after connection. This contrasts with the traditional request-response model of HTTP, where the client needs to send a request and the server may only send a response after receiving the request.

多様な通信パターンを実現するためにWebSocketプロトコルを使い、接続後のクライアントとサーバー間の双方向通信を可能にしている。これは、クライアントがリクエストを送信する必要があり、サーバーはリクエストを受信した後にレスポンスを送信することができるという、HTTPの伝統的なリクエスト-レスポンスモデルと対照的である。

>WebSockets require an endpoint to listen for connections and the other endpoint connecting. Moreover, clients, using the web application in a browser, may only start a connection to a WebSocket, and servers may only listen for new connections. The design of WebSocket limits the ability for two clients to communicate directly via a WebSocket (e.g. Line 2 in Fig. 4). STScript uses the server to route messages between client roles, enabling communication between all participants via a star network topology.

WebSocketはエンドポイントが接続を待ち、他のエンドポイントが接続する必要がある。さらに、ブラウザでWebアプリケーションを使用するクライアントは、WebSocketへの接続を開始するだけでよく、サーバーは新たな接続を待つだけで良い。WebSocketの設計では、2つのクライアントがWebSocketを介して直接通信する機能が制限されている（例：図４の2行目）。STScriptでは、クライアントのロール間のメッセージをルーティングするためにサーバーを使用し、スター型ネットワークトポロジーを介した全ての参加者間の通信を可能にする。
- ネットワークトポロジー・・・ネットワークを構成する機器（ノード）同士がどのような規則性に基づいて繋がれているかを模式的に表したもの。

>An important aspect of web programming is the interactivity of the user interface (UI). Viewed in a browser, the web application interacts with the user via UI events, e.g. mouse clicks on buttons. The handling of UI events may be implemented to send messages to the client (e.g. when the “Submit”
button on the form is clicked), which may lead to practical problems. For instance, would clicking “Submit” button twice create two bookings for the customer? We use the popular React.js UI framework for generating client endpoints, and generate APIs that prevent such errors from happening.

Webプログラミングの重要な側面は、ユーザーインターフェース（UI）のインタラクティブ性である。ブラウザで見ると、webアプリケーションはUIイベント、例えばボタンのマウスクリックなどを通じてユーザーと対話することができる。UIイベントの処理は、クライアントにメッセージを送信するように実装される場合があり（例えば、フォームの「送信」ボタンがクリックされた時など）、実用上問題が生じる可能性がある。例えば、「送信」ボタンを２回クリックすると、顧客の予約が2つ作成されてしまうのではないか？我々は、クライアントエンドポイントの生成に人気の「React.js」 UIフレームワークを使用し、そのようなエラーが起こらないようなAPIを生成している。

- Webプログラミングをターゲットする
- TypeScriptは静的な型システムとJavaScriptへのコンパイラを備えている
- 多様な通信パターンを実現するためにWebScoketプロトコルを使用してサーバーとクライアントとの双方向通信を可能にする
- STScriptはサーバーを使用して、スター型ネットワークトポロジーを介した全ての参加者間の通信を可能にする
- Webプログラミングの重要な側面として、UIのインタラクティブ性がある

>**Callback-Style API for Clients and Servers.**
>Our code generation toolchain STScript produces TypeScript APIs in a callback style [35] to statically guarantee channel linearity. The input global protocol is analysed by the toolchain for well-formedness, and an endpoint finite state machine (EFSM) is produced for each endpoint. We show the EFSM for role A in Fig. 5. The states in the EFSM represent local types (subject to reductions) and transitions represent communication actions (Symbol ! stands for sending actions, ? for receiving).

**クライアントとサーバーのコールバックスタイルAPI**
コード生成ツールチェーンであるSTSctriptはコールバックスタイルでTypeScript APIを生成し、チャネルの線形性を静的に保証している。入力されたグローバルプロトコルは、ツールチェーンによって形式的に分析され、有限オートマトン（EFSM）が各エンドポイントで生成される。図５にロールAのEFSMを示す。EFSMの状態はローカルタイプ（削減対象）を表し、遷移は通信の動きを表す（記号！は送信動作、？は受信動作を表す）。

>In the callback API style, type signatures of callbacks are generated for transitions in the EFSM. Developers implement the callbacks to complete the program logic part of the application, whilst a generated runtime takes care of the communication aspects.

コールバックAPIスタイルでは、EFSMの遷移に対してコールバックのタイプシグネチャ（type signatures）が生成される。開発者はアプリケーションのプログラムロジック部分を完成させるためにコールバックを実装し、生成されたランタイムを通信面を保護する。

> For callbacks, sending actions correspond to callbacks prompting the payload type as a return type, so that the returned value can be sent by the runtime. Dually, receiving actions correspond to callbacks taking the payload type as an argument, so that the runtime invokes the callback with the received value.

コールバックの場合、送信動作は戻り値の型としてペイロード型を要求するコールバックに対応し、戻り値はランタイムによって送信されることができる。一方、受信動作はペイロード型を引数として取るコールバックに対応し、ランタイムは受信した値でコールバックを呼び出す。


- クライアントとサーバーのコールバックスタイルAPI
- STScriptはコールバックスタイルでTypeScript APIを生成し、チャネルの線形性を静的に保証している。
- グローバルプロトコルはツールチェーンによって分析され、各エンドポイントでEFSMが生成される。
- 送信動作は戻り値の型としてペイロード型を要求するコールバックに対応し、戻り値はランタイムによって送信される。
- 受信動作はペイロード型を引数として取るコールバックに対応し、ランタイムは受信した値でコールバックを呼び出す。
- コールバック：非同期処理
同期処理：コードを上から順に処理していき、一つの処理が終わるまでは次の処理をしない。

// 指定した`timeout`ミリ秒経過するまで同期的にブロックする関数
function blockTime(timeout) {
    const startTime = Date.now();
    // `timeout`ミリ秒経過するまで無限ループをする
    while (true) {
        const diffTime = Date.now() - startTime;
        if (diffTime >= timeout) {
            return; // 指定時間経過したら関数の実行を終了
        }
    }
}
console.log("処理を開始");
blockTime(1000); // 他の処理を1000ミリ秒（1秒間）ブロックする
console.log("この行が呼ばれるまで処理が1秒間ブロックされる");

//result
処理を開始
この行が呼ばれるまで処理が1秒間ブロックされる

非同期処理：コードを順に処理していくのだが、一つの非同期処理が終わるのを待たずに次の処理を評価する。JavaScriptの非同期処理の代表例として`setTimeout`がある。
`setTimeout(コールバック関数, delay);`
`setTimeout`関数は`delay`ミリ秒後に`コールバック関数`を呼び出すようにタイマーへ登録する非同期処理である。

//blockTime関数は上と同じ

console.log("1. setTimeoutのコールバック関数を10ミリ秒後に実行します");
setTimeout(() => {
    console.log("3. ブロックする処理を開始します");
    blockTime(1000); // 他の処理を1秒間ブロックする
    console.log("4. ブロックする処理が完了しました");
}, 10);
// ブロックする処理は非同期なタイミングで呼び出されるので、次の行が先に実行される
console.log("2. 同期的な処理を実行します");

//result
1. setTimeoutのコールバック関数を10ミリ秒後に実行します
2. 同期的な処理を実行します
3. ブロックする処理を開始します
4. ブロックする処理が完了しました

>**Implementing the Server Role.**
> In the travel agency protocol, as shown in Fig. 4, we designate role S as the server role. The server role does not only interact with the two clients, but also routes messages for the two clients.

**サーバーの役割を実装する**
旅行会社プロトコルでは図４に示すように、ロールSをサーバーロールとする。サーバーの役割は2つのクライアントと相互に関与するだけでなく、2つのクライアントのメッセージをルーティングする。

>The routing will be handled automatically by the runtime, saving the need for developers to specify manually. As a result, the developer only handles the program logic regarding the server, in this use case, namely providing quotes for holiday bookings and handling booking confirmations

ルーティングはランタイムによって自動的に処理されるため、開発者が手動で指定する必要はない。その結果、開発者はこの使用事例において、サーバーに関するプログラムロジック、すなわち休日の予約の見積もりを提供し、予約の確認をすることだけを処理する。


>All callbacks carry an extra parameter, Next, which acts as a factory function for constructing the successor state. This empowers IDEs to provide auto-completion for developers. For example, the factory function provided by the callback for handling a Query message (Line 4) prompts the permitted labels in the successor send state, as illustrated in Fig. 6.

全てのコールバックはNextという追加パラメータを持ち、これは後続の状態を構築するためのファクトリ関数として機能する。これはIDE（統合開発環境）が開発者に自動保管を提供する権利を与える。例えば、Queryメッセージを処理するコールバック関数が提供するファクトリ関数（4行目）は、図６に示すように、後続の送信状態で許可されたラベルをプロンプト表示する。


- サーバーの役割を実装する
- サーバーの役割は2つのクライアントと相互に関与するだけでなく、2つのクライアントのメッセージをルーティングする。
- ルーティングはランタイムによって自動的に処理されるため、開発者が手動で指定する必要はない。
- 全てのコールバックはNextという追加パラメータを持ち、これは後続の状態を構築するためのファクトリ関数として機能する。

>**Implementing the Client Roles.**
>To implement client roles, merely implementing the callbacks for the program logic is not sufficient — unlike servers, web applications have interactive user interfaces, additional to program logic. As mentioned previously, our code generation toolchain targets React.js for client roles.

**クライアントの役割を実装する**
クライアントの役割を実装するためには、プログラム論理のコールバックを実装するだけでは満足できない。サーバーとは異なり、webアプリケーションはプログラム論理に加えて相互作用を持つUIがある。前に述べたように、我々のコード生成ツールチェーンはクライアントの役割を果たすReact.JSをターゲットにしている。

> For background, the smallest building blocks in React.js are components, which can carry properties (immutable upon construction) and states (mutable). Components are rendered into HTML elements, and they are re-rendered when the component state mutates.

背景として、React.jsの最小の構成要素はコンポーネントであり、プロパティ（構築時に不変）と状態（変異可能）にすることができる。コンポーネントはHTML要素にレンダリングされ、コンポーネントの状態が変化した時に再レンダリングされる。

- 状態とプロパティとの違い
- 状態（State）
コンポーネント自体によって保持され、コンポーネント間での移行はできない。
Stateの値は`this.setState()`をコンポーネント内で呼び出すことで更新できる。
- プロパティ（Props）
親から渡される値。不変のデータとして扱われる。

>To bind the program logic with an interactive user interface, we provide component factories that allow the UI component to be interposed with the current state of the EFSM. Developers can provide the UI event handler to the component factory, and obtain a component for rendering. The generate code structure enforces that the state transition strictly follows the EFSM, so programmer errors (such as the double “submit” problem) are prevented by design.

プログラム論理とインタラクティブなUIを結びつけるために、我々はEFSMの現在の状態にUIコンポーネントの介在を許可するコンポーネントファクトリを提供する。開発者は、コンポーネントファクトリにUIイベントハンドラを提供し、レンダリングのためのコンポーネントを得ることができる。生成コードの構造は状態遷移がEFSMに精密に従うことを強制するため、プログラマーのエラー（２重の「Submit」問題など）を設計によって防ぐことができる。


>Using the send state component in the FSM for the endpoint B as an example, Line 2 reads, “generate a React component that sends the OK message with `this.state.split` as payload on a click event”. It is used on Line 6 as a wrapper for a stylised `<Button>` component. The runtime invokes the handler and performs the state transition, which prevents the double “submit” problem by design.

エンドポイントBのFSMにおける送信状態コンポーネントを例とし、2行目を読むと、クリックイベントで`this.state.split`をペイロードとするOKメッセージを送信するReactコンポーネントを生成している。これは6行目で様式化された`<Button>`コンポーネントのラッパーとして使われている。ランタイムがハンドラを呼び出して遷移状態を行うため、設計上、二重の「submit」問題を防ぐことができる。

- クライアントの役割を実装する
- クライアントの役割はReact.jsが果たす
- React.jsの最小構成要素はコンポーネントであり、コンポーネントには状態とプロパティがある
- プログラム論理とインタラクティブなUIを結びつけるために、EFSMの現在の状態にUIコンポーネントの介在を許可するコンポーネントファクトリを提供する

>**Guaranteeing Communication Safety.**
Returning to the implementation in § 1, we outline how STScript prevents common errors to enable type-safe web programming.

**通信の安全性を保証する**
1章の実装に戻り、型安全なwebアプリケーションを実現可能にするためにSTScriptがどのように一般的なエラーを防具化について概説する。

>**Communication Mismatch**
All generated callbacks are typed according to the permitted payload data type specified in the protocol, making it impossible for traveller A to send the quote as a string by accident.

**通信の不一致**
生成された全てのコールバックはプロトコルで指定された許容ペイロードデータ型に従って型付けされているため、旅行者Aが誤って見積もりを文字列として送信することは不可能である。

>**Channel Usage Violation**
The generated client-side runtime requires the developer to provide different UI components for each EFSM state – once traveller A submits a quote, the runtime will transition to, thus render the component of,
a different EFSM state. This guarantees that, whilst waiting for a response from traveller B, it is impossible for traveller A to submit another quote and violate channel linearity.

**チャネル使用の違反**
生成されたクライアント側のランタイムでは、開発者はESFMの状態ごとに異なるUIコンポーネントを提供する必要がある-旅行者Aが見積もりを提出すると、ランタイムは異なるEFSMの状態に移行し、そのコンポーネントをレンダリングする。これにより、旅行者Bからの回答を待っている間、旅行者Aが別の見積もりを提出し、チャネルの線形性に違反することは不可能であるということが保証されている。

>**Handling Session Cancellation**
If either traveller closes their browser before the protocol runs to completion, the generated runtimes leverage the events available on their WebSocket connections to notify (via the server) other roles
about the session cancellation. The travel agency can implement the error handler callback (generated by STScript) to perform clean-up logic in response to cancellations.

- leverage = utilize

**セッションのキャンセルに対応**
プロトコルが完了する前にどちらかの旅行者がブラウザを閉じた場合、生成されたランタイムはWebSocket接続で利用可能なイベントを利用して、セッションのキャンセルについて他のロールに（サーバー経由で）通知する。旅行会社は、エラーハンドラーコールバック（STScriptで生成）を実装することで、キャンセルに対応したクリーンアップ論理を実行することができる。

## 3.Implementation

>In this section, we explain how the generated code executes the EFSM for Node.js and React.js targets. We also present how STScript APIs handle errors in a dynamic web-based environment (for complete code, see Appendix E).

この節では、生成されたコードがNode.jsおよびReact.jsのターゲットに対してEFSMを実行する方法を説明する。また、STScript APIが動的なウェブベース環境でどのようにエラーを処理するかも紹介する（完全なコードは付録Eを参照）。

>**Session Runtime.**
>The session runtime executes the EFSM in a manner permitted by the multiparty protocol description. The runtime keeps track of the current state, performs the required communication action (i.e. send or receive a message), and transitions to the successor state.

**セッションランタイム**
セッションランタイムは、マルチパーティプロトコル記述で許可された方法でEFSMを実行する。ランタイムは現在の状態を追跡し、必要な通信動作（例えばメッセージの送受信など）を行い、後続の状態に遷移する。

>The runtime provides seams for the developer to inject the callback implementations, which define application-specific concerns for the EFSM, such as what message payload to send (and dually, how to process a received message). This design conceals the WebSocket APIs from the developer and entails that the developer cannot trigger a send or receive action, so STScript can statically guarantee protocol conformance.

ランタイムは、開発者がコールバック実装を投入するための継ぎ目を提供し、そのコールバック実装は送信するメッセージのペイロード（および、受信したメッセージの処理方法）など、EFSMに対するアプリケーション固有の物事を定義する。この設計では、WebSocket APIを開発者から隠し、開発者が送受信動作を起こせないようにすることで、STScriptはプロトコル適合性を静的に保証できる。

>**Executing the EFSM in Node.js.**
>Each state of the EFSM is characterised by a (generated) State class and a type describing the shape of the callback (supplied by the developer). To allow the server to correctly manage concurrent sessions, the developer can access a (generated) session ID when implementing the callbacks.

**Node.jsでEFSMを実行する。**
EFSMの各状態は、（開発者によって提供される）Stateクラスとコールバックの形状を記述する型によって特徴付けられる。サーバーが正しく共存セッションを管理できるように、開発者はコールバックを実装するときにセッションIDにアクセスすることができる。

>STScript also generates IO interfaces for each kind of EFSM state – send, receive, or terminal. The generated State class implements the interface corresponding to the type of communication action it performs.

また、STScriptはEFSM状態-送信、受信、端末の種類に応じたIOインターフェースを生成する。生成されたStateクラスは、実行する通信動作の種類に対応したインターフェースを実装している。


>The session runtime for Node.js is a class that executes the EFSM using a state transition function parameterised by the State class of the current EFSM state. As the IO interfaces constitute a discriminated union, the runtime can parse the type of the current EFSM state and propagate the appropriate IO functions (for sending or receiving) to the State class.

Node.jsのセッションランタイムは、現在のEFSMの状態のStateクラスによってパラメータ化した状態遷移関数を用いてEFSMを実行するクラスである。IOインターフェースは区別可能な結合を構成しているので、ランタイムは現在のEFSMの状態を解析し、適切なIO関数（送信または受信のため）をStateクラスに伝搬させることができる。

>In turn, the State class invokes the callback supplied by the developer to inject program logic into the EFSM, perform the communication action (using this.send or this.registerMessageHandler), and invoke the state transition function (this.next) with the successor state.

順番に、Stateクラスは、開発者によって提供されたコールバックを呼び出してEFSMにプログラム論理を付け加え、通信動作を行い（this.sendまたはthis.registerMessageHandlerを使って）、後続の状態で状態遷移関数(this.next)を呼び出す、という流れになっている。

>Notably, the routed messages are completely absent because the generated code transparently routes messages without exposing any details. As messages specify their intended recipient, the runtime identifies messages not intended for the server by inspecting the metadata, and forwards them to the WebSocket connected to the intended recipient.

特に注目すべきは、ルーティングされたメッセージは、生成されたコードが詳細を公開することなく透過的にメッセージをルーティングするため、全く存在しないことである。メッセージが意図する受信者を指定すると、ランタイムはメタデータを検査することによってサーバーを意図しないメッセージを特定し、意図する受信者に接続されているWebSocketに転送する。

>**Executing the EFSM in React.js.**
>Each state in the EFSM is encoded as an abstract React component. The developer implements the EFSM by extending the abstract classes to
provide their own implementation – namely, to build their user interface. Components for send states can access component factories to generate React components that perform a send action when a UI event (e.g. onClick, onMouseOver) is triggered. Components for receive states must implement abstract methods to handle all possible incoming messages.

**React.jsでEFSMを実行する**
EFSMの各状態は、抽象的なReactコンポーネントとして符号化されている。開発者は独自の実装を提供するために、抽象クラスを拡張することによってEFSMを実装する。すなわち、ユーザーインターフェースを構築する。送信状態のコンポーネントは、コンポーネントファクトリにアクセスして、UIイベント（onClickやonMouseOver）が起こった時に送信動作を実行するReactコンポーネントを生成することができる。受信状態のコンポーネントは、来る可能性のある全てのメッセージを処理するための抽象メソッドを実装しなければならない。

>The session runtime for React.js is a React component, instantiated using the developer’s implementation of each EFSM state. Channel communications are managed by the runtime, so the developer’s implementations cannot access the WebSocket APIs, which prevents channel reuse by construction. The runtime renders the component of the current EFSM state and binds the permitted communication action through supplying component properties.

React.jsのセッションランタイムはReactコンポーネントで、EFSMの各状態を開発者の実装によってインスタンス化する。チャネルの通信はランタイムによって管理されているため、開発者の実装はWebSocket APIにアクセスできず、構造によるチャネルの再利用を防ぐことができる。ランタイムは、現在のEFSM状態のコンポーネントをレンダリングし、コンポーネントプロパティを供給することで許可された通信動作を結びつける。

>**Error Handling.**
>An error handling mechanism is critical for web applications. Clients can disconnect from the session due to network connectivity issues or simply by closing the browser. Similarly, servers may also face connectivity issues.

**エラー処理**
エラー処理の仕組みはWebアプリケーションにとって重要である。クライアントはネットワーク接続の問題や、単にブラウザを閉じることによってセッションから切断することができる。同様に、サーバーも接続の問題に直面する可能性がある。

>Upon instantiating the session runtime, STScript requires developers to supply a cancellation handler to handle local exceptions (e.g. errors thrown by application logic) and global session cancellations (e.g. disconnection events by another endpoint).

セッションランタイムのインスタンスを作成する際、STScriptは開発者にローカル例外(アプリケーション論理によるスローエラー)やグローバルセッションのキャンセル（別のエンドポイントによる切断イベント）を処理するためのキャンセルハンドラを提供するように要求する。

- throw文・・・ユーザー定義の例外を発生させる。throw new Error('Required');でRequiredというメッセージを持ったエラーオブジェクトを返すという意味

>The session runtime detects cancellation by listening to the close event on the WebSocket connection, and invokes the cancellation handler with appropriate arguments on a premature close event. We parameterise the cancellation handlers with additional information (e.g. which role disconnected from the session, the reason for the disconnection) to let developers be more specific in their error handling logic.

セッションランタイムは、WebSocket接続の終了イベントを聞くことでキャンセルを検知し、早期終了イベントで適切な引数を指定してキャンセルハンドラを起動する。開発者がより具体的にエラー処理の論理を明確にできるように、キャンセルハンドラに追加情報（どのロールがセッションから切断したか、切断の理由）をパラメータ化する。

>**Cancellation Handlers for Servers.**
>Server endpoints define cancellation handlers through a function, parameterised by the session ID, the role which initiated the cancellation, and (optionally) the reason for the cancellation — if the server-side logic throws an exception, the handler can access the thrown error through the reason parameter.

**サーバーのキャンセルハンドラ**
サーバーのエンドポイントは、セッションID、キャンセルを開始したロール、（オプションで）キャンセルの理由によってパラメータ化された関数（下のでいうとacync）を通じて、キャンセルハンドラを定義する。もし、サーバー側の論理が例外をスローした場合、ハンドラはreasonパラメータを通じてスローされたエラーにアクセスできる。


>Using the Travel Agency scenario introduced in § 1, if the customer prematurely closes their browser before responding to a Quote, the server can detect this (Line 4) and release the reservation to preserve data integrity.

1で紹介した旅行会社のシナリオを使用すると、顧客がQuoteに応答する前にブラウザを早期に閉じた場合、サーバーはこれを検出し（4行目）、データの整合性を維持するために予約を解除できる。

>**Cancellation Handlers for Clients.**
>Browser-side endpoints also define cancellation handlers through a　function parameterised in the same way as those in Node.js, but must　return a React component to be rendered by the session runtime.

**クライアントのキャンセルハンドラ**
ブラウザ側のエンドポイントも、Node.jsのものと同じようにパラメータ化された関数を通じてキャンセルハンドラを定義するが、セッションランタイムによってレンダリングされるReactコンポーネントを返す必要がある。

>In the context of the Travel Agency scenario, the customer can render a different UI depending on whether the server disconnected or their　friend closed their web browser prematurely. Browser endpoints can also respond　to cancellations emitted by other client-side roles: when a browser　endpoint disconnects, the server detects this and propagates the　cancellation to the other client-side roles.

旅行会社のシナリオでは、サーバーが切断されたか友人がウェブブラウザを早期に閉じたかによって顧客が異なるUIをレンダリングすることができる。ブラウザのエンドポイントは、その他のクライアント側のロールから発信されたキャンセルにも対応できる。ブラウザのエンドポイントが切断されると、サーバーはこれを検出し、他のクライアント側のロールにキャンセルを伝搬させる。

## 4.RouST:Routed Session Types
>This section defines the syntax and semantics of RouST and proves some important properties. We show the sound and complete trace correspondence between a global type and a collection of endpoint types projected from the global type (Theorem 4.6). Using this result, we prove deadlock freedom (Theorem 4.7).

本節では、RouSTの構文と意味論を定義し、いくつかの重要な特性を証明する。グローバル型と、グローバル型から射影されたエンドポイント型の集合との間にある、正当性があり完全なトレース対応関係を示す（定理4.6）。この結果を用いて、デッドロックがないことを証明する（定理4.７）。

>We then show that, in spite of the added routed communications, RouST does not over-serialise communications by proving communication preservations between the original MPST and RouST (Theorem 4.11). These three theorems ensure that STScript endpoint programs are communication-safe, always make progress, and correctly conforms to the user-specified protocol.

次に、ルーティング通信が追加されたのにも関わらず、オリジナルのMPSTとRouSTとの間にある通信保存性を証明することによりRouSTが通信を過剰に連続化しないことを示す（定理4.１１）。これら3つの定理により、STScriptのエンドポイントプログラムは通信安全であり、常に進行し、ユーザーが指定したプロトコルに正しく準拠することが保証される。

### 4.1 Syntax of Routed Multiparty Session Types

>We define the syntax of global types $𝐺$ and local types (or endpoint types) $𝑇$ in Definition 4.1. Global types are also known as protocols and describe the communication behaviour between all participating roles (participants), while local types describe the behaviour of a single participating role. We shade additions to the original (or canonical) multiparty session type (MPST) [9, 11, 15, 30] in this colour .

定義４．１において、グローバル型$G$とローカル型(またはエンドポイント側)$T$の構文を定義する。グローバル型はプロトコルとも呼ばれ、全ての参加ロール（参加者）間の通信動作を記述し、ローカル型は1つの参加ロールの動作を記述する。この色（下の式の黄緑っぽい色）では、元のマルチパーティセッション型（MPST）への追加を影で表現している。

>**Definition 4.1** (Global and Local Types). The syntax of global and local types are defined below:

**定義 4.1** （グローバル型とローカル型）
グローバル型とローカル型の構文は以下のように定義される：


>***Global Types.*** $p → q : \{𝑙_𝑖 :𝐺_𝑖 \}_{𝑖∈𝐼}$ describes a ***direct communication*** of a message $𝑙_𝑖$ from a role $p$ to $q$. We require that $p ≠ q$, that labels $𝑙_𝑖$ are pairwise distinct, and that the index set 𝐼 is not empty. The message in the communication can carry a label among a set of permitted labels $𝑙_𝑖$ and some payload.

***グローバル型.***　$p → q : \{𝑙_𝑖 :𝐺_𝑖 \}_{𝑖∈𝐼}$はロール$p$から$q$へのメッセージ$𝑙_𝑖$の**直接的な通信**を表している。ここでは、$p ≠ q$であること、ラベル$l_i$が対で区別されること、そしてインデックス集合$I$が空集合でないことを要求する。通信のメッセージは、許可されたラベル集合のうちのラベル$l_i$と、何らかのペイロードを運ぶことができる。

- インデックス集合・・・添字集合　　ラベルの集合のこと

>After a message with label $𝑙_𝑖$ is received by q, the communication continues with $𝐺_𝑖$, according to the chosen label. For simplicity, we do not include payload types (integers, strings, booleans, etc) in the syntax. We write $p → q : 𝑙 : 𝐺$ for single branches. For recursion, we adopt an equi-recursive view [27, §21], and use $𝜇t.𝐺$ and $t$ for a
***recursive protocol*** and a ***type variable***. We require that recursive types are contractive (guarded), i.e. the recursive type $𝜇t.𝐺$ progresses after the substitution $𝐺[𝜇t.𝐺/t]$, prohibiting types such as $𝜇t.t$. We use end to mark the ***termination*** of the protocol, and often omit the final end.

ラベル$l_i$を持つメッセージを$q$が受信した後は、選択されたラベルに従って$G_i$で通信を続ける。簡単にするため、ペイロードの型（int,string,booleanなど）は構文に含めない。分岐が一つの場合は$p → q : 𝑙 : 𝐺$と記述する。再帰については等再帰的な考え方を採用し、**再帰プロトコル**と**型変数**を、$𝜇t.𝐺$と$t$を用いて表す。再帰型はコントラクティブ（ガード型）である、すなわち
再帰型$𝜇t.𝐺$は$𝐺[𝜇t.𝐺/t]$の置換後に進行し、$𝜇t.t$のような型を禁止している。プロトコルの**終了**を示すためにendを使用し、最後のendは大抵省略される。

>To support routed communication, we allow messages to be sent through a router role. A ***routed communication*** $p-s→ q : \{𝑙_𝑖 :𝐺_𝑖\}_{𝑖∈𝐼}$ describes a router role $s$ coordinating the communication of a message from $p$ to $q$ : $q$ offers $p$ a choice in the index set $𝐼$, but $p$ sends the selected choice $𝑙_𝑖$ to the router $s$ instead.

ルーティング通信をサポートするために、ルーターの役割を通じてメッセージを送信することを許可する。**ルーティング通信**$p-s→ q : \{𝑙_𝑖 :𝐺_𝑖\}_{𝑖∈𝐼}$は$p$から$q$へのメッセージの通信を調整するルーターロール$s$を記述する。：$q$はインデック集合$I$の中の選択を$p$に提示するが、$p$は代わりに選ばれた選択肢$l_i$をルーター$s$へ送信する。

>The router forwards the selection from $p$ to $q$. After $q$ receives $p$’s selection, the communication continues with $𝐺_𝑖.s$ ranges over the set of roles $p, q,$ · · · , but we use $s$ by convention as the router is usually some server. The syntax for routed communication shares the same properties as direct communication, but we additionally
require that $p ≠ q ≠ s$. We use $pt (𝐺)$ to denote the set of participants in the global type $𝐺$.

ルーターは$p$から$q$に選択肢を転送する。$q$が$p$の選択を受信した後、通信はロールの集合$p, q,$ · · ·上の$𝐺_𝑖.s$の範囲で継続するが、ルーターは通常どこかのサーバーであるため、慣習的に$s$を使う。ルーティング通信の構文は直接通信と同じ性質を共有しているが、さらに$p ≠ q ≠ s$を要求する。グローバル型$G$の参加者の集合を表すためには$pt (G)$を使う。

>**Example 4.2** (Travel Agency). The travel agency protocol, as shown in Fig. 4, is described by the global type $𝐺_{travel}$ in the original MPST, and $𝐺_{travel}^𝑅$ in RouST.

**例4.２**（旅行代理店）
旅行代理店プロトコルは、図４で示すように、オリジナルのMPSTではグローバル型$𝐺_{travel}$、RouSTでは$𝐺_{travel}^𝑅$で記述される。


>***Local Types.***
We first describe the local types in the original MPST theory. $q\&\{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$ stands for **branching** and $q \oplus \{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$ stands for **selection**. From the perspective of $p$, branching (resp. selection) offers (resp. selects) a choice among an index set $𝐼$ to (resp. from) $q$, and communication continues with the corresponding $𝑇_𝑖$. Local types $𝜇t.𝑇$ , $t$ and $end$ have the same meaning as their global type counterparts.

***ローカル型***
まず、オリジナルのMPST理論におけるローカル型について説明する。$q\&\{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$は**分岐**、$q \oplus \{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$は**選択**の略である。$p$から見て、分岐はインデックス集合$I$から$q$への選択肢を提供し、対応する$𝑇_𝑖$で通信が継続する。ローカル型$𝜇t.𝑇$、$t$、$end$はグローバル型に対応するものと同じ意味を持つ。

>We add new syntax to express routed communication from the perspective of each role involved. The local type $p\&⟨s⟩ \{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$ is a **routed branching**:the current role is offering a choice from an index set $𝐼$ to $p$ (the intended sender), but expects to receive $p$’s choice via the router role $s$; if the message received is labelled $𝑙_𝑖$, $q$ will continue with local type $𝑇_𝑖$.

ルーティングされた通信を、関係するロールの視点から表現するための新しい構文を追加する。ローカル型$p\&⟨s⟩ \{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$は**ルーティングされた分岐**である：現在のロールがインデックス集合$I$から$p$（送信者）に選択肢を提供しているが、ルーターロール$s$を介して$p$の選択を受け取ることを期待している。もし受け取ったメッセージが返って$l_i$というラベルであれば、その$q$はローカル型$T_i$で継続する。

>The local type $q \oplus ⟨s⟩ \{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$ is a routed selection: the current role makes a selection from an index set $𝐼$ to $q$ (the intended recipient), but sends the selection to the router role $s$; if the message sent is labelled $𝑙_𝑖$, $p$ will continue with local type $𝑇_𝑖$. The local type $p \hookrightarrow q : \{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$ is a **routing communication**.

ローカル型$q \oplus ⟨s⟩ \{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$はルーティングされた選択である：現在のロールはインデックス集合$I$から$q$（意図する受信者）への選択を行うが、ルーターロール$s$にその選択を送信する。もし送信されたメッセージが$l_i$というラベルであれば、$p$はローカル型$T_i$で継続される。ローカル型$p \hookrightarrow q : \{𝑙_𝑖:𝑇_𝑖\}_{𝑖∈𝐼}$は**ルーティング通信**である。

>The router role orchestrates the communication from $p$ to $q$, and continues with local type $𝑇_𝑖$ depending on the label of the forwarded message. We keep track of the router role to distinguish between routing communications from normal selection and branching interactions.

ルーターロールは$p$から$q$への通信を編成し、転送されたメッセージのラベルに応じてローカル型$T_i$で継続する。通常の選択と分岐の相互作用からルーティング通信を区別するために、ルーターロールを記録しておく。

>***Endpoint Projection.***
>The local type $𝑇$ of a participant $p$ in a global type $𝐺$ is obtained by the endpoint projection of $𝐺$ onto $p$, denoted by $𝐺$ as $𝐺↾p$.

グローバル型$G$の参加者$p$のローカル型$T$は$G$の$p$へのエンドポイント射影によって得られ、$𝐺↾p$と表記される。

>**Definition 4.3** (Projection). The projection of $𝐺$ onto $r$, written $𝐺↾r$ is defined as:

**定義4.3**射影。$G$の$r$への射影は$𝐺↾r$と書き、次のように定義される。


>The projection $(p → q : \{𝑙_𝑖:𝐺_𝑖\}_{𝑖∈𝐼}) ↾ r$ is defined similar to $(p−s→q:\{𝑙_𝑖:𝐺_𝑖\}_{𝑖∈𝐼})↾r$ dropping $s$ (in the resulting local type) and the third case.

射影$(p → q : \{𝑙_𝑖:𝐺_𝑖\}_{𝑖∈𝐼}) ↾ r$は$(p−s→q:\{𝑙_𝑖:𝐺_𝑖\}_{𝑖∈𝐼})↾r$が$s$を失った場合と同様に定義され、3番目のケースとする。

>A merge operator ($⊓$) is used when projecting a communication onto a non-participant. It checks that the projections of all continuations must be “compatible” (see Definition B.2).

マージ演算子($⊓$)は、通信をしていない参加者に射影するときに使用される。これは、全ての連続の射影が「互換」でなければならないことを確認する（定義B.2参照）。

- Definition B.2

>**Example 4.4** (Merging Local Types). Two branching types from the same role with disjoint labels can merged into a type carrying both labels, e.g. $A \& 𝐻𝑒𝑙𝑙𝑜.end ⊓ A \& 𝐵𝑦𝑒.end = A \& \{𝐻𝑒𝑙𝑙𝑜:end;𝐵𝑦𝑒:end\}$. The same is not true for selections, $A \oplus 𝐻𝑒𝑙𝑙𝑜.end ⊓ A \oplus 𝐵𝑦𝑒.end$ is undefined.
The global type $𝐺_1$ can be projected to role $C$, but not $𝐺_2$.

**例4.4**ローカル型をマージする。同じロールから2つの分岐型でラベルが不一致なものは、両方のラベルを持っている型にマージされる（例：$A \& 𝐻𝑒𝑙𝑙𝑜.end ⊓ A \& 𝐵𝑦𝑒.end = A \& \{𝐻𝑒𝑙𝑙𝑜:end;𝐵𝑦𝑒:end\}$）。同じことは選択では当てはまらず、$A \oplus 𝐻𝑒𝑙𝑙𝑜.end ⊓ A \oplus 𝐵𝑦𝑒.end$は未定義である。

>***Well-formedness.*** In the original theory, a global type $𝐺$ is well-formed (or realisable), denoted wellFormed ($𝐺$), if the projection is defined for all its participants.
We assume that the global type $𝐺$ is contractive (guarded).

**形式化可能**　原論では、グローバル型$G$は形式化可能（または実現可能）であり、もし射影が全ての参加者に対して定義されている場合、wellFormed ($𝐺$)と表記される。
グローバル型$G$は保守的である。

>In RouST, we say that a global type is well-formed with respect to the role $s$ acting as the router. We define the characteristics that $s$ must display in $𝐺$ to prove that it is a router, and formalise this as an inductive relation, $𝐺 \circledast s$ (Definition 4.5), which reads $s$ is a centroid in $𝐺$. The intuition is that $s$ is at the centre(=center) of all communication interactions.

RouSTでは、グローバル型がルーターとして動作するロール$s$に関して整形されているという。$s$がルーターであることを証明するために$G$において示さなければならない性質を定義し、これを$s$が$G$において重心であると読む帰納的関係$𝐺 \circledast s$（定義4.5）として形式化する。直感的には、$s$は全ての通信の相互作用の中心にあるということである。

>**Definition 4.5** (Centroid). The relation $𝐺 \circledast s$ ($s$ is the centroid of $𝐺$) is defined by the two axioms $end \circledast s$ and $t \circledast s$ and by the following rules:

**定義4.5**（重心）。　関係$𝐺 \circledast s$ ($s$は$𝐺$の重心)は、二つの公理 $end \circledast s$ と $t \circledast s$と次の規則によって定義される：


>For direct communication, $s$ must be a participant and a centroid of all continuations. For routed communication, $s$ must be the router and be a centroid of all continuations. Now we define of well-formedness of a global type $𝐺$ in RouST with respect to the router $s$ (denoted $wellFormed^𝑅 (𝐺, s)$):

直接通信の場合、$s$は参加者であり、全ての継続の重心でなければならない。ルーティング通信の場合、$s$はルーターであり、全ての継続の重心でなければならない。ここで、RouSTにおけるグローバル型$G$のルーター$s$に対する整形性を定義する。

### 4.2 Semantics of RouST

>This subsection defines the labelled transition system (LTS) over global types for RouST, building upon [11].

この小節では、[11]をもとに、RouSTのグローバル型に対するラベル付き遷移システム(LTS)を定義する。

>First, we define the labels (actions) in the LTS which distinguish the direct sending (and reception) of a message from the sending (and reception) of a message via an intermediate routing endpoint. Labels range over $𝑙,𝑙', · · ·$ are defined by:

まず、LTSにおいてメッセージの直接送信（および受信）と中間のルーティングエンドポイントを経由するメッセージの送信（および受信）を区別するラベル（動作）を定義する。$𝑙,𝑙', · · ·$上の範囲であるラベルは以下のように定義される。


>The label $via⟨s⟩ (pq!𝑗)$ represents the sending (performed by $p$) of a message labelled $𝑗$ to $q$ through the intermediate router $s$. The label $via⟨s⟩ (pq?𝑗)$ represents the reception (initiated by $q$) of a message labelled $𝑗$ send from $p$ through the intermediate router $s$. The subject of a label $𝑙$, denoted by subj($𝑙$), is defined as: subj$(via⟨s⟩ (pq!𝑗))$ = subj$(pq!𝑗)$ = $p$; and subj$(via⟨s⟩ (pq?𝑗))$ = subj$(pq?𝑗)$ = $q$.

ラベル$via⟨s⟩(pq!𝑗)$は、ラベル$j$が中間ルーター$s$を介して$q$に送信することを表す。ラベル$via⟨s⟩(pq?𝑗)$は$p$から中間ルーター$s$を通して送信された$𝑗$というメッセージの受信を表す。ラベル$l$の対象はsubj($𝑙$)と与えられ、subj$(via⟨s⟩ (pq!𝑗))$ = subj$(pq!𝑗)$ = $p$とsubj$(via⟨s⟩ (pq?𝑗))$ = subj$(pq?𝑗)$ = $q$として定義される。

>***LTS Semantics over Global Types.*** The LTS semantics model asynchronous communication to reflect our implementation. We introduce intermediate states (i.e. messages in transit) within the grammar of global types: the construct $p ⇝ q. 𝑗 : \{𝑙_𝑖:𝐺_𝑖\}_{𝑖∈𝐼}$ represents that the message $𝑙_𝑗$ has been sent by $p$ but not yet received by $q$; and the construct $p ⇝ s q. 𝑗 : \{𝑙_𝑖:𝐺_𝑖\}_{𝑖∈𝐼}$ represents that $𝑙_𝑗$ has been sent from $p$ to the router $s$ but not yet routed to $q$.

***グローバル型に対するLTS(labelled transition system)意味論。***　LTSの意味論は、我々の実装を反映するために、非同期処理をモデル化する。グローバル型の文法の内に中間状態(すなわち転送中のメッセージ)を導入している：構成要素 $p ⇝ q. 𝑗 : \{𝑙_𝑖:𝐺_𝑖\}_{𝑖∈𝐼}$ はメッセージ$l_i$が$p$によって送信されたが、まだ$q$によって受信されていないことを表し、構成要素 $p ⇝ s q. 𝑗 : \{𝑙_𝑖:𝐺_𝑖\}_{𝑖∈𝐼}$ はメッセージ$l_i$が$p$からルーター$s$に送信されたが、まだ$q$にルーティングされていないことを表す。

>We define the LTS semantics over global types, denoted by $𝐺 \xrightarrow{l} 𝐺′$, in Fig. 7. [Gr1] and [Gr2] model the emission and reception of a message; [Gr3] models recursions; [Gr4] and [Gr5] model causally unrelated transmissions — we only enforce the syntactic order of messages for the participants involved in the action $l$.

図７に、$𝐺 \xrightarrow{l} 𝐺′$で示されるグローバル型に対するLTS意味論を定義する。[Gr1]と[Gr2]はメッセージの送信と受信を、[Gr3]は再帰を、[Gr4]と[Gr5]は因果関係のない送信をモデルにしている-動作$l$に関与する参加者のメッセージの構文順序だけを強制している。


> [Gr6] and [Gr7] are analogous to [Gr1] and [Gr2] for describing routed communication, but uses the “routed in-transit” construct instead. [Gr8] and [Gr9] are analogous to [Gr4] and [Gr5]. An important observation from [Gr8] and [Gr9] is that, for the router, the syntactic　order of routed communication can be freely interleaved between the syntactic order of direct communication. This is crucial to ensure that the router does not over-serialise communication. See Example 4.13 for an LTS example.

[Gr6]と[Gr7]は、ルーティングされた通信を記述するための[Gr1]と[Gr2]に類似しているが、代わりに“routed in-transit”という構造を使用している。[Gr8]と[Gr9]は[Gr4]と[Gr5]に類似している。[Gr8]と[Gr9]の重要な観点は、ルーターにとって、ルーティングされた通信の構文順序は、直接通信の構文順序の間に自由に挟めることである。これは、ルーターが通信を過度に連続化しないことを保証するために重要である。LTSの例として例4.13を見よ。

>***Relating Semantics of Global and Local Types.*** We prove the soundness and completeness of our LTS semantics with respect to projection. We take three steps following [11]:

***グローバル型とローカル型の相対的意味論.***　我々は射影に関するLTS意味論の安全性と完全性を証明する。[11]に従って3つのステップを踏む。

>1. We extend the LTS semantics with configuration $(\vec{𝑇},\vec{w})$, a collection of local types $\vec{𝑇}$ with FIFO queues between each pair of participants $\vec{w}$.
>2. We extend the definition of projection, to obtain a configuration of a global type (a projected configuration), which expresses intermediate communication over FIFO queues.
>3. We prove the trace equivalence between the global type and its projected configuration (i.e. the initial configuration of $𝐺$, $(\vec{𝑇},\vec{𝜖})$, where $\vec{T}$ = $\{𝐺↾p\}_{p∈P}$ are a set of local types projected from $𝐺$ and $𝜖$ is an empty queue).

1.LTSの意味論を、参加者のペア$\vec{w}$の間にFIFOキューを持つローカル型$\vec{𝑇}$の集合である構成$(\vec{𝑇},\vec{w})$で拡張する。
2.射影の定義を拡張し、FIFOキュー上の中間通信を表現するグローバル型の構成（射影された構成）を得ることができる。
3.グローバル型と射影された構成（すなわち、$G$の初期構成、$(\vec{𝑇},\vec{𝜖})$、$\vec{T}$ = $\{𝐺↾p\}_{p∈P}$は$G$から射影されたローカル型の集合、$𝜖$は空キュー）とのトレース等価を証明する。

- FIFO：first in, first outの略

>The proof is non-trivial: due to space limitations, we omit the semantics of local types, configurations and global configurations, and only state the main result (see Appendices $B$ and $C$).

証明は自明ではない：紙面の都合上、ローカル型、構成、グローバル型の構成の意味論は省略し、主要な結果のみを述べる(付録B,Cを参照)。

>***Theorem 4.6*** (Sound and Complete Trace Equivalence). Let $G$ be a well-formed canonical global type. Then $G$ is trace equivalent to its initial configuration.

***定理4.6***　（安全かつ完全なトレース等価.）$G$を整形された基準のグローバル型とする。その時、$G$はその初期構成とトレース等価である。

>Theorem 4.7 proves traces specified by a well-formed global protocol are deadlock-free, i.e. the global type either completes all communications, or otherwise makes progress. Note that this theorem implies the deadlock-freedom of configurations by Theorem 4.6.

定理4.7は、整形されたグローバルプロトコルで指定されたトレースはデッドロックがないこと、すなわちグローバル型が全ての通信を完了するか、そうでなければ進行することを証明するものである。この定理は、定理4.6による構成のデッドロックフリー性を含意していることに注意。

>***Theorem 4.7*** (Deadlock Freedom). Let $𝐺$ be a global type. Suppose $𝐺$ is well-formed with respect to some router $s$, i.e. $wellFormed^𝑅 (𝐺, s)$

***定理4.7*** （デッドロックフリー）. $G$をグローバル型とする。$G$があるルーター$s$に関して整形式である、すなわち$wellFormed^𝑅 (𝐺, s)$であるとする。

### 4.3 From Canonical MPST to RouST　

- canonical・・・基準の、標準の

>We present an encoding from the canonical MPST theory (no routers) to RouST. This encoding is parameterised by the router role (conventionally denoted as $s$); the intuition is that we encode all communication interactions to involve $s$. If the encoding preserves the semantics of the canonical global type, then this encoding can guide a correct protocol implementation in Node.js via $s$, preserving communication structures of the original protocol without deadlock.

ルーターを持たない標準的なMPST理論からRouSTへの符号化を提案する。この符号化はルーターの役割（従来は$s$と表記される）によってパラメータ化される；直感的には全ての通信の相互作用を、$s$を含むように符号化することである。もし、符号化が標準的なグローバル型の意味論を保持するならば、この符号化は$s$を介してNode.jsで正しいプロトコル実装を導き、デッドロックすることなく元のプロトコルの通信構造を保持することができる。

>***Router-Parameterised Encoding.*** We define the routerparameterised encoding on global types, local types and LTS labels in the MPST theory. We start with global types, as presented in Definition 4.8. The main rule is the direct communication: if the communication did not go through $s$, then the encoded communication involves $s$ as the router.

***ルーターパラメーター化された符号化.*** MPST理論におけるグローバル型、ローカル型、LTSラベルのルーターパラメータ化された符号化を定義する。定義4.8で示されるように、グローバル型から始める。主な規則は、直接通信である：通信が$s$を経由しない場合、符号化された通信はルーターとして$s$が関与する。

>**Definition 4.8** (Encoding on Global Types). The encoding of global type $𝐺$ with respect to the router role $s$, denoted by $[[𝐺, s]]$, is defined as:

**定義4.8** （グローバル型に対する符号化.）ルーターロール$s$に関するグローバル型$G$の符号化は、$[[𝐺, s]]$と表記され、次のように定義される：


>Local types express communication from the perspective of a particular role, hence the encoding takes two roles.

ローカル型は特定のロールの視点から通信を表現するものであり、従って符号化は二つの役割を担う。

>**Definition 4.9** (Encoding on Local Types). The encoding of local type $𝑇$ (from the perspective of role $q$) with respect to the router role $s$, denoted by $[[𝑇 , q, s]]$, is defined as:

**定義4.9** （ローカル型に対する符号化）. ルーターロール$s$に関するローカル型$𝑇$の符号化は$[[𝑇 , q, s]]$で表記され、次のように定義される：


>**Lemma 4.10** (Correspondence between Encodings). The projection of an encoded global type $[[𝐺, s]]↾r$ is equal to the encoded local type after projection $[[𝐺↾r, r, s]]$, with respect to router $s$, i.e. $\forall r, s,𝐺. (r ≠ s =⇒ [[𝐺,s]]↾r = [[𝐺↾r, r, s]])$.

**補題4.10**　（符号化間の対応）. 符号化されたグローバル型$[[𝐺, s]]↾r$の射影は、ルーターに関して射影$[[𝐺↾r, r, s]]$後の符号化されたローカル型と等しい、すなわち、$\forall r, s,𝐺. (r ≠ s =⇒ [[𝐺,s]]↾r = [[𝐺↾r, r, s]])$である。

>The constraint $r ≠ s$ is necessary because we would otherwise lose information on the right-hand side of the equality: the projection of $s$ in the original communication does not contain the routed interactions, so applying the local type encoding cannot recover this information.

$r ≠ s$というという制限が必要なのは、そうしなければ等式の右辺の情報が失われるからである：元の通信における$s$の射影はルーティングされた相互作用を含まないため、ローカル型の符号化を適用してもこの情報を修復することはできない。

>**Theorem 4.11** (Encoding Preserves Well-Formedness). Let $𝐺$ be a global type, and $s$ be a role. Then we have:

**定理4.11** （符号化はwell-Formednessを保存する）. $G$をグローバル型とし、$s$をロールとする。すると以下のようになる：


>***Preserving Communication.*** We present a crucial result that directly addresses the pitfalls of naive definitions of routed communication — our encoding does not overserialise the original communication. We prove that our encoding preserves the LTS semantics over global types — or more precisely, we can use the encodings over global types and LTS actions to encode all possible transitions in the LTS for global types in the canonical MPST theory. We define the encoding of label 𝑙 in the original MPST as: $[[pq!𝑗, s]] = via⟨s⟩ (pq!𝑗)$ and $[[pq?𝑗, s]] = via⟨s⟩ (pq?𝑗)$ if $s ∉ \{p,q\}$ and otherwise $[[𝑙, s]] = l$.

***通信の維持.*** 我々はルーティングされた通信の素朴な定義の落とし穴に直接対処する重要な結果を提示する-我々の符号化は、元の通信を連続化しない。我々の符号化がグローバル型に対するLTS意味論を保持することを証明する-より正確には、グローバル型とLTS動作に対する符号化を用いて、標準的なMPST理論におけるグローバル型のLTSにおいて、全ての可能な遷移を符号化することができる。元のMPSTにおけるラベル$l$の符号化を次のように定義する：$s ∉ \{p,q\}$の場合は$[[pq!𝑗, s]] = via⟨s⟩ (pq!𝑗)$と$[[pq?𝑗, s]] = via⟨s⟩ (pq?𝑗)$、それ以外の場合は$[[𝑙, s]] = l$とする。

>**Theorem 4.12** (Encoding Preserves Semantics). Let $𝐺$,$𝐺′$ be well-formed global types such that $𝐺 \xrightarrow{l} 𝐺′$ for some label　$𝑙$. Then we have:

**定理4.12** （符号化は意味論を保持する）. あるラベル$l$に対して$𝐺 \xrightarrow{l} 𝐺′$となるような、$𝐺$,$𝐺′$を整形済みグローバル型とする。すると次のようになる：


>We conclude with an example which demonstrates global semantics in RouST and a use of the encoding.

最後に、RouSTにおけるグローバル意味論を示す例と、符号化の使用例を示す。

>**Example 4.13** (Encoding Preserves Semantics). Consider the global type
$G = p \rightarrow q : M1 . s \rightarrow q : M2 . end.$
We apply our encoding with respect to the router role $s$:
$[[G,s]] = p - s \rightarrow q : M1 . s \rightarrow q : M2 . end.$

**例4.13** （符号化は意味論を保持する）.
グローバル型 $G = p \rightarrow q : M1 . s \rightarrow q : M2 . end.$ を考える。

>We note that $𝑙 = sq!𝑀2$ can reduce $𝐺$ through [Gr1] (via one application of [Gr4]). After encoding, we have that $[[𝑙,s]] = 𝑙$. The encoded global type $[[𝐺,s]]$ can be reduced by $𝑙$ through [Gr1] (via one application of [Gr8]), as demonstrated by Theorem 4.12. The label $𝑙 = sq!𝑀2$ is a prefix of a valid execution trace for $𝐺$, given below.

$𝑙 = sq!𝑀2$は[Gr1]を通して([Gr4]の一回適用を介して)$G$を減らすことができることに注意する。符号化した後、$[[𝑙,s]] = 𝑙$を持つ。符号化されたグローバル型$[[𝐺,s]]$は定理4.12で示されているように、[Gr1]を通して$l$でまとめられる。ラベル$𝑙 = sq!𝑀2$は、以下に示す$G$の有効な実行トレースの接頭辞である。


>Interested readers can verify that the encoded trace (given below) is a valid execution trace for $[[𝐺,s]]$.

興味のある読者は、符号化されたトレース（以下の示す）が$[[𝐺,s]]$の有効な実行トレースであることを検証することができる。


### 5 Evaluation

>In this section, we demonstrate the expressiveness and applicability of STScript for modern web programming, and report on performance. We walk through how to implement Noughts and Crosses game with our toolchain, showing how the generated APIs prevent common errors.

このセクションでは、最近のWebプログラミングに対してSTScriptの表現力と適用性を示し、その性能について報告する。また、我々のツールチェーンを使ってNoughts and Crossesゲームを実装する方法を説明し、生成されるAPIが一般的なエラーをどの様に防いでいるかを示す。

>We choose this game since we can demonstrate the main features of STScript within the limited space. We also remark on performance implications of our toolchain. In Appendix D, we include larger cases studies: Battleship, a game with more complex program logic; and Travel Agency (Fig. 1), as shown in § 1.

限られたスペースでSTScriptの主な機能を示すことができるため、このゲームを選択した。また、我々のツールチェーンのパフォーマンスへの影響についても言及する。付録Dでは、より大規模なケーススタディを掲載している。より複雑なプログラム論理を持つ「バトルシップ」、そして§1に示した「旅行会社」（図１）である。

>***Noughts and Crosses.*** We present the classic two-player turn-based game of Noughts and Crosses here. We formalise the game interactions using a Scribble protocol: both players, identified by noughts (O’s) or crosses (X’s), take turns to place a mark on an unoccupied cell of a grid, until a player wins (when their markers form a straight line) or a stalemate is reached (when all cells are occupied and no one wins).

***Noughts and Crosses.*** ここでは、定番な２人用のターン制ゲーム「Noughts and Crosses」を紹介する。このゲームの相互作用は、Scribbleプロトコルを用いて定式化されている。ノット(O)またはクロス(X)で識別されているプレイヤーは、グリッドの上の空いているマスに順番にマークを置いていき、いずれかのプレイヤーが勝つ（両者のマーカーが直線になった時）または膠着状態に達する（全てのマスが占拠され誰も勝てない）まで続ける。


>***Game Server.*** We set up the game server as an Express.js application on top of the Node.js runtime. We define our own game logic in a Board class to keep track of the game state and expose methods to query the result. When the server receives a move, it notifies the game logic to update the game state asynchronously and return the game result caused by that move.

***ゲームサーバー.*** ゲームサーバーは、Node.jsランタイム上にExpress.jsアプリケーションとして設定する。Boardクラスに独自のゲーム論理を定義して、ゲームの状態を追跡し、結果を問い合わせるためにメソッドを公開する。サーバーは手を受け取ると、ゲーム論理に通知して非同期にゲーム状態を更新し、その手によって引き起こされたゲーム結果を返す。

>The expressiveness of STScript enable the developer to define the handlers as async functions to use the game logic API correctly – this is prevalent in modern web programming, but not directly addressed in [13, 20].
The generated session runtime for Node.js is given as:

STScriptの表現力により、ハンドラを非同期関数として定義し、ゲーム論理APIを正しく使用することができる。これは最新のWebプログラミングで一般的だが、[13,20]では直接対処していない。


>The runtime is initialised by a function parameterised by the session ID and returns the initial state. The developer can use the session ID as an identifier to keep track of concurrent sessions and update the board of the corresponding game.

ランタイムは、セッションIDをパラメータとする関数によって初期化され、初期状態を返す。開発者は、セッションIDを識別子として、同時進行中のセッションを把握し、対応するゲームの盤面を更新することができる。

>***Game Players.*** On the browser side, the main implementation detail for game players is to make moves. Intuitively, the developer implements a grid and binds a mouse click handler for each vacant cell to send its coordinates in a Pos(Point) message to the game server.

***ゲームプレイヤー*** ブラウザ側では、ゲームプレイヤーの主な実装内容は、移動を行うことである。直感的には、開発者はグリッドを実装し、空いたセルごとにマウスクリックのハンドラを束縛して、その座標をPos(Point)メッセージでゲームサーバーに送る。

>Without STScript, developers need to synchronise the UI with the progression of protocol manually — for instance, they need to guarantee that the game board is inactive after the player makes a move, and manual efforts are error-prone and unscalable.

STScriptがない場合、開発者はUIとプロトコルの行動を手動で同期させる必要がある--例えば、プレイヤーが手を打った後、ゲームボードが非アクティブになることを保証する必要があるが、手作業ではエラーが発生しやすく、拡張性もない。

>The generated APIs from STScript make this intuitive, and guarantees communication safety in the meantime. By providing React component factories for send states, the APIs let the developer trigger the same send action on multiple UI events with possibly different payloads.

STScriptから生成されたAPIは、これを直感的に理解できる様にし、その間の通信の安全性を保証する。送信状態のためのReactコンポーネントファクトリを提供することで、APIによって開発者は、おそらく違うペイロードを持つ複数のUIで同じ送信動作を引き起こすことができる。

>In Noughts and Crosses, for each vacant cell on the game board, we create a $<SelectCell>$ React component from the component factory function (Line 6). The factory builds a component that sends the Pos message with $x-y$ coordinate as payload when the user clicks on it. We bind the onClick event to the table cell by wrapping it with the $<SelectCell>$ component.

Noughts and Crossesでは、ゲームボードの空いているセルごとに、コンポーネントファクトリ関数から<SelectCell>というReactコンポーネントを作成している(6行目)。ファクトリはユーザーがクリックした時に$x-y$座標をペイロードとするPosメッセージを送信するコンポーネントを構築する。テーブルセルを<SelectCell>コンポーネントでラッピングして、onClickイベントを束縛している。


>The session cancellation handler allows the developer to render useful messages to the player by making applicationspecific interpretations of the cancellation event. For example, if the opponent disconnects, the event can be interpreted as a forfeiture and a winning message can be rendered.

セッションキャンセルハンドラは、開発者にキャンセルイベントをアプリケーション特有の解釈で、プレイヤーに有用なメッセージを表示させる。例えば、相手が接続を切った場合、そのイベントを没収と解釈し、勝利のメッセージをレンダリングすることが可能である。

>***Performance.*** To measure the performance impact of generated APIs (which handle the communication for developers), in contrast to a typical developer implementation without the APIs (interacting directly with WebSocket primitives), we compare the execution time of web-based implementations of the Ping Pong protocol (shown below) with (denoted mpst) and without (denoted bare) generated APIs.

APIを使用しない典型的な開発者の実装（WebSocketプリミティブと直接対話）と比較して、生成されたAPI（開発者のために通信を処理する）のパフォーマンスへの影響を測定するために、（以下に示す）Ping PongプロトコルのWebベースの実装について、生成された場合（mpstと表記）と、用いない場合（bareと表記）の実行時間を比較する。


>We parameterise an experiment run of the protocol by the number of round-trip messages 𝑛, fixated in the application logic across experiments. Upon establishing a connection, both endpoints repeatedly exchange 𝑛 messages of increasing integer values. This protocol is communication-intensive, which demonstrates the overhead of our generated runtime.

プロトコルの実験実行を、実験間でアプリケーションロジックに固定された往復メッセージの数𝑛でパラメータ化する。接続が確認されると、両エンドポイントは増加する整数値の𝑛個のメッセージを繰り返し交換する。このプロトコルは通信負荷があるため、我々の生成するランタイムのオーバーヘッドを示す。

>***Setup.*** To measure the overhead as accurately as possible, we specify that the implementations must follow:

***セットアップ*** 　オーバーヘッドをできるだけ正確に測定するために、実装が従うべきことを規定した：

>- Clients implement the same user interface, rendering a <$button$> which triggers the send, and a <$div$> captioned with the number of PONGs received.

クライアントは、送信のトリガーとなる<$button$>と、受信したPONGの数を示す<$div$>を表示する、同じユーザーインターフェースを実装している。

>- Clients use React Context API for application state management, keeping track of the number of PONGs received.

クライアントはアプリケーションの状態管理にReact Context APIを使用し、受信したPONGの数を記録している。

>- Both endpoints use the built-in console.time method to record the execution time. The timer starts on a WebSocket OpenEvent and stops on a CloseEvent.

どちらのエンドポイントでも、組み込みのconsole.timeメソッドを使用して実行時間を記録している。タイマーは、WebSocketのOpenEventで開始し、CloseEventで停止する。

>- To observe the execution pattern, both endpoints log the running elapsed time on every message receive event, and measure the time taken to receive a message and perform the successor IO action.

実行パターンを観察するために、両方のエンドポイントはメッセージ受信イベント毎に実行経過時間を記録し、メッセージを受信して孤族のIO動作を実行するのにかかった時間を測定する。

>- We use the compiled JavaScript production build for both Client and Server implementations.

クライアントとサーバーの両方の実装で、コンパイルされたJavaScriptのプロダクションビルドを使用する。

>We run the experiments under a network of latency 0.165ms (64 bytes ping), and repeat each experiment 20 times. Execution time measurements are taken using a machine equipped with Intel i7-4850HQ CPU (2.3 GHz, 4 cores, 8 threads), 16 GB RAM, macOS operating system version 10.15.4, Node.js runtime version 12.12.0, and TypeScript compiler version 3.7.4. We standardise all packages used in the front- and back-end implementations across experiments.

レイテンシ0.165ms (64バイトPing)のネットワークのもとで実験を行い、各実験を20回繰り返した。実行時間の測定は、Intel i7-4850HQ CPU (2.3 GHz, 4 cores, 8 threads),16 GB RAM,macOS operating system version 10.15.4, Node.js runtime version 12.12.0,TypeScript compiler version 3.7.4を搭載した機械で行なっている。

>***Benchmarks.*** A run begins with C connecting to S and completes after the specified number of round trips. Each round trip requires both endpoints to process the incoming message and perform the successor send action – we refer to this as the message processing time (Msg. Proc. Time). We compare the time for each endpoint (average of 20 runs) across both implementations, for $𝑛 \in \{10^2,10^3\}$ round trips.

***ベンチマーク*** 実行はC(クライアント)がS(サーバー)に接続するところから始まり、指定された複数回数で完了する。各往復では、両方のエンドポイントが受信メッセージを処理し、後続の送信アクションを実行する必要がある-これをメッセージ処理時間(Msg. Proc. Time)と呼ぶ。両実装のエンドポイントごとに、$𝑛 \in \{10^2,10^3\}$往復の時間を比較した(20回実行の平均)。

>We make two key observations from Table 1: **(1)** the round trip time is dominated by the browser-side, and **(2) mpst** introduces overhead dominated by the React.js session runtime. Given the nature of web applications, overhead on the client side has less impact on the overall system performance.

表１からは二つの重要な見解が得られる。**(1)** 往復の時間はブラウザ側で決まり、**(2) mpst**は、React.jsセッションランタイムによって支配されるオーバーヘッドを導入する。Webアプリケーションの性質上、クライアント側のオーバーヘッドがシステム全体の性能に与える影響は少ない。


>The overhead in **mpst** arises from increased state modifications by C, since component state is updated both when EFSM state transitions and when the Pong message count changes. The React.js session runtime for **mpst** re-renders on each state transition, even if there are no UI changes; these additional state changes are not incurred by **bare**.

**mpst** のオーバーヘッドは、EFSMの遷移状態とPongメッセージ数の変更時の両方でコンポーネントの状態が更新されるため、Cによる状態変更の増加によって発生する。**mpst** のReact.jsセッションランタイムは、UIの変更がない場合でも、状態遷移ごとに際レンダリングを行う；これらの追加的な状態変化は、**bare**では発生しない。

>We validate our hypothesis by running the Ping Pong micro-benchmark with UI requirements — we summarise the results in Table 2. By requiring additional text to be shown on send and terminal states, we observe a noticeable increase in the message processing time for **bare**, whereas relatively insignificant changes on **mpst**. The UI requirements demand **bare** to perform additional state updates and re-rendering, reducing the overhead relative to **mpst**.

この仮説を検証するために、UIを要件とするPingPongマイクロベンチマークを実行した-その結果を表２にまとめた。送信時と終了時に表示される追加のテキストを要求することで、**bare**ではメッセージ処理時間が著しく増加したが、**mpst**では比較的小さな変化しか見られなかった。UI用件では、追加の状態更新と再描画を実行するために**bare**が要求され、**mpst**と比較してオーバーヘッドが削減されている。


>***Scalability.*** As the generated APIs abstract away the details of the actual destination of a message, the effect of scaling the number of roles in a protocol is transparent to the developer. The number of states and transitions in the EFSM increases as the complexity of the protocol scales.

***可読性*** 生成されたAPIはメッセージの実際の宛先の詳細を抽象化するため、プロトコル内のロールの数を拡張する効果は開発者にとって透過的である。EFSMの状態と遷移の数は、プロトコルの複雑さが増大するにつれて増加する。

>The generated React.js runtime re-renders the UI on every state transition, so more complex protocols would trigger more re-renders, incurring performance penalties. However, this is less of a concern for STScript, as user-facing application protocols in interactive web settings tend not to be large in size (cf. distributed algorithms in large scale systems).

React.jsランタイムは状態遷移ごとにUIを再レンダリングするため、プロトコルが複雑になると再レンダリングが多くなり、パフォーマンスが低下してしまう。しかし、インタラクティブなWeb環境におけるユーザー向けのアプリケーションプロトコルは、サイズが大きくない傾向があるため、STScriptではこの懸念はあまりない（大規模システムにおける分散アルゴリズムを参照）。

# 2022/4/19

* Web開発の体験のため Wordpress を EC2 にインストールした。