WebAssembly Specification Text Formatにおける関数定義の読み方

Question

WebAssembly Specificationの読み方に関する質問です。

WATで以下のmoduleを定義しました。

(module
    (func (export "addInt")
    (param $value_1 i32) (param $value_2 i32)
    (result i32)

    local.get $value_1
    local.get $value_2
    i32.add
    )
)

このコードはWASMに変換して正しく実行することができました。
次にどうして関数定義はこのように定義するのだろうと考えたところ
仕様でそう決まっているから(WATからWASMに変換するツールが仕様にそって実装されているから)だと思いました。

そこで、WATの関数定義の仕様を参照したのですが、読み方が理解できませんでした。
具体的にはText Format > Functionsの箇所です。(MathJaxをteratailに書く方法がわからなかったので画像で失礼します)

TextFormatの仕様に関する読み方はConventionsに定義されていると思うのですが、そこを読んでみてもこの仕様の書き方から上記の具体的なコードが書けるという理解に至れませんでした。

特にわからなかったのが、=>の意味です。
Grammarによりますと

とあり、Productionってなに?となってしまいました。
WASM Specificationを読むにあたり前提となっている知識がたりないのかなとも考えており、もし本仕様を読むにあたりこれを知っておくとよいというようなものがあれば併せて教えていただけると助かります。

Answer 1

遅ればせながら、can110さんの回答に補足致します。

Conventionsの冒頭にある通り、WATの構文はattribute grammar（日本語では属性文法）という、構文定義が表す意味を「属性」として形式的に定義する手法が用いられています。

そして、件の「Productions」の解説

における => の左辺はsymを構成するシンボル（の列）Tを、右辺はTによって生成される合成属性（synthesized attribute）を表します。この合成属性が表すものはcan110さんの仰るとおり大本の抽象構文を指しているようです。

Comments

[ymgyt]

補足ありがとうございます。背景の解説、非常に参考になります。

Answer 2

まずProductionは生成規則、ルールといった意味であり、形式文法といった分野での用語です。

なのでかんたんに言えば::=の左側は右側のルールで生成（構成）されているといった意味になります。

次に=>の意味ですが、これは説明読んでもよく分かりませんね。
なので推測ですが、左側はテキスト形式、右側はそれに対応する大元の文法を指していると思います。
つまり提示のfuncでいえば、右側はFunctionsに対応していると解釈すればよいと思います。

Comments

[ymgyt]

回答ありがとうございます。理解を進められるように形式文法について調べてみます。