ふと、3つのコンストラクタをもつ帰納型を有限型 (finType) として扱いたくなったのだが、どうやればいいのか調べるのにけっこう苦労した。
結局、以下のようにすれば可能なようだ。
From mathcomp Require Import all_ssreflect.
From HB Require Import structures.
Inductive mytype :=
| C1 : bool -> mytype
| C2 : bool -> mytype
| C3 : bool -> mytype.
Lemma sum_of_mytypeK : cancel
(fun (v : mytype) =>
match v with
| C1 b => inl (inl b)
| C2 b => inl (inr b)
| C3 b => inr b
end)
(fun (v : bool + bool + bool) =>
match v with
| inl (inl b) => C1 b
| inl (inr b) => C2 b
| inr b => C3 b
end).
Proof. by case; case. Qed.
HB.instance Definition _ := Finite.copy mytype (can_type sum_of_mytypeK).
Check mytype : choiceType.
Check mytype : countType.
Check mytype : eqType.
Check mytype : finType.
ここでは、bool + bool + bool 型 (つまり sum (sum bool bool) bool 型) と mytype が同型であることを証明して、それにより mytype が有限型であることを登録している。
これをやると、finType の継承元 (choiceType, countType, eqType) としても mytype が自動的に登録されるようだ。 (登録されるので、mytype : choiceType のようなキャストが通る。このキャストは型を、登録された choiceType の値からその型を取り出す式に変換している。)
もちろん、mytype などというものは定義せずに、bool + bool + bool 型を使うという方法もあるが、 そうすると inl (inr b) みたいなわかりにくい表現を使わないといけない。 (inl (inr b) を呼び出す関数として C1 を定義して、Arguments C1 : simpl never. とすればかなり inl (inr b) という内部表現を隠せるが、それでも出てきてしまうことはあって、change で修正しなければいけないので面倒くさい )
まぁ、Notation で inl (inr b) を C1 b にみせかければよかったのかもしれない。 でも、sum 型を他の用途でも使っているとそっちにも影響するし、分解を [a|b|c] と書きたいところを [[a|b]|c] と書かなければならない問題は残る。
なお、環境は Rocq 9.0.0 と rocq-mathcomp-ssreflect 2.4.0 である。
演算子の優先順位というのは、式の中に ... op1 e op2 ... という部分があったとき、つまり式 e が演算子 op1 と演算子 op2 ではさまれていたときに、 その式 e が優先順位の高い方の演算子の引数となるということである。 綱引きみたいな感じ。
ここでいう演算子は二項演算子や単項演算子だけとはかぎらない。 一般には、式の導出規則で式が左右の端に出現するものは、その端に出現する式を他の演算子とではさむことができるので、その式がどちらに属するかを優先順位によって指定することができる。
yacc とかの優先順位は、衝突があったときに shift と reduce のどちらかを選ぶ、と実装される。 SDF では (SGLR により曖昧なものも含めてすべての構文木を生成する仕掛けなので) 導出の抑制を指定するという話になっている。
ただ、SDF の導出抑制は抑制しすぎて受け付ける言語が小さくなってしまう場合があるようで、よろしくない。
ということで、そういうことが起きない (受け付ける言語が変わらない) ように、 文法を優先順位を反映するように変形する、という話がある。
前者の著者の D論が後者で、Chapter 4 に前者の Safe Specification of Operator Precedence Rules が入っている。 (D論のほうが後で書かれているだろうから、修正がおこなわれているかもしれない)
ここであげられているアルゴリズムで以下のように文法を変形できるという例が記述されている。
入力として以下の文法が与えられる。 (E + E が左結合というのが (left) という記述で指定され、E + E よりも i E と a のほうが優先順位が低いというのが不等号 > で指定されている。 )
E ::= E + E (left)
> i E
| a
出力として以下の文法が生成される。
E ::= E1 + E2 | i E | a E1 ::= E1 + E3 | a E2 ::= i E | a E3 ::= a
この文法は、以下のような足し算と OCaml スタイルの if 式を表現している。 (区別しやすくするため、トークンを double quote でくくってある)
E ::= E "+" E
| "if" E "then" E "else" E
| "a"
i E というのは i と E の連結で、i は "if" E "then" E "else" に対応している。 OCaml スタイルの if 式は "if" E "then" E "else" E だが、"if" から "else" までは両端がトークンなので、かっこみたいなものとみなせる。 そのため優先順位には関係しないので、i としてまとめている。 こうやってまとめると、i は前置単項演算子とみなせる。
ということで、二項演算子 + と、前置単項演算子 i からなる式で、後者のほうが優先順位が低いという文法を考えていることになる。 (二項演算子よりも前置単項演算子の優先順位が高いなら、単項演算子のプラスやマイナスと同じになるので、単項演算子の優先順位が低いというのがこの例の面白く難しい点である。)
さて、変形された文法を少し展開して単純にすると、以下のようになる。
E ::= E1 + E2 | i E | a E1 ::= E1 + a | a E2 ::= i E | a
これを眺めてしばらく考える。
まぁ、なんとかわかった気がする。 ... i a + ... という列があったときに、a は (優先順位が i よりも高い) + の引数になるようになっていると思う。
でも、この文法はわかりやすくはないよな。+ が 2箇所、i が 2箇所、a が 4箇所出現していて、(優先順位で記述されていた文法と違って) 重複があるし。
優先順位を使った文法のほうが、意図を素直に表現できていると思う。
なお、件のD論の Chapter 5 Operator Precedence for Data-dependent Grammars では、 (Chapter 3 で説明されている) data-dependent grammar というものを使って、そういう重複を起こさずに優先順位を実装する方法を述べている。 これは GLL ベースで、attributed grammar ぽいことをやって、優先順位に反する構文木を除去していくというものだと思う。 ただ、これって決定的な動作をするかどうかいまいち確信できないような気がする。
GLL parsing をちょっと調べたのだが、 これは Earley parsing に近いと思った。
まぁ、lookahead で枝刈りするのは Earley にはないから、ちょっと違うか。
RubyKaigi 2025 follow up でちょっと質問した話を自分で試してみた。 (質問のときは canonical LR と言った気がするけど、試すのは IELR だよな)
parse.y を LALR じゃなくて IELR で処理することによって、 キーワード do の衝突をどうにかできるのではないかという話なのだが、 bison では IELR を使えるので、bison を使っていた頃の Ruby を使えばすぐに試せるのではないか。
lrama が入ったのは Ruby 3.3.0 のようなので、Ruy 3.2.9 で試してみよう。
parse.c の生成を観察すると、まず parse.y から parse.tmp.y を作り、 parse.tmp.y から bison で y.tab.c を作っている。
なので、parse.tmp.y をいじって、keyword_do_cond, keyword_do_block, keyword_do_LAMBDA を消して keyword_do にしてしまう。 また、%define lr.type ielr を追加する。 これで、conflict した文法を IELR で処理することになる。
% diff -u parse.tmp.y- parse.tmp.y
--- parse.tmp.y- 2025-08-30 22:43:42.024243269 +0900
+++ parse.tmp.y 2025-08-30 22:49:29.173601547 +0900
@@ -11,6 +11,8 @@
%require "3.0"
+%define lr.type ielr
+
%{
#if !YYPURE
@@ -519,9 +521,6 @@
TOKEN2ID(keyword_retry);
TOKEN2ID(keyword_in);
TOKEN2ID(keyword_do);
- TOKEN2ID(keyword_do_cond);
- TOKEN2ID(keyword_do_block);
- TOKEN2ID(keyword_do_LAMBDA);
TOKEN2ID(keyword_return);
TOKEN2ID(keyword_yield);
TOKEN2ID(keyword_super);
@@ -1416,9 +1415,6 @@
keyword_retry "`retry'"
keyword_in "`in'"
keyword_do "`do'"
- keyword_do_cond "`do' for condition"
- keyword_do_block "`do' for block"
- keyword_do_LAMBDA "`do' for lambda"
keyword_return "`return'"
keyword_yield "`yield'"
keyword_super "`super'"
@@ -3748,7 +3744,7 @@
}
;
-k_do_block : keyword_do_block
+k_do_block : keyword_do
{
token_info_push(p, "do", &@$);
/*%%%*/
@@ -3823,7 +3819,7 @@
;
do : term
- | keyword_do_cond
+ | keyword_do
;
if_tail : opt_else
@@ -4172,7 +4168,7 @@
token_info_pop(p, "}", &@3);
$$ = $2;
}
- | keyword_do_LAMBDA
+ | keyword_do
{
/*%%%*/
push_end_expect_token_locations(p, &@1.beg_pos);
@@ -9771,11 +9767,11 @@
if (kw->id[0] == keyword_do) {
if (lambda_beginning_p()) {
p->lex.lpar_beg = -1; /* make lambda_beginning_p() == FALSE in the body of "-> do ... end" */
- return keyword_do_LAMBDA;
+ return keyword_do;
}
- if (COND_P()) return keyword_do_cond;
+ if (COND_P()) return keyword_do;
if (CMDARG_P() && !IS_lex_state_for(state, EXPR_CMDARG))
- return keyword_do_block;
+ return keyword_do;
return keyword_do;
}
if (IS_lex_state_for(state, (EXPR_BEG | EXPR_LABELED | EXPR_CLASS)))
さて、このパッチでは %define lr.type ielr をつけているが、これをつければ IELR でつけなければ LALR である。 (LALR をしてするのに lalr と書いてもよい。また、canonical LR を指定するには canonical-lr と書く。)
Bison Manual - 5.8.1 LR Table Construction
で、LALR と IELR (と、ついでに Canonical LR) で bison を動かしてみた。
LALR の場合:
% bison -d -o y.tab.c parse.tmp.y parse.tmp.y: エラー: シフト/還元衝突: 4 個が見つかりました, 0 個は期待通りです parse.tmp.y: エラー: 還元/還元衝突: 3 個が見つかりました, 0 個は期待通りです parse.tmp.y: ノート: '-Wcounterexamples' オプションをつけて競合の反例を生成するために再実行
IELR の場合:
% bison -d -o y.tab.c parse.tmp.y parse.tmp.y: エラー: シフト/還元衝突: 4 個が見つかりました, 0 個は期待通りです parse.tmp.y: エラー: 還元/還元衝突: 3 個が見つかりました, 0 個は期待通りです parse.tmp.y: ノート: '-Wcounterexamples' オプションをつけて競合の反例を生成するために再実行
Canonical LR の場合:
% bison -d -o y.tab.c parse.tmp.y parse.tmp.y: エラー: シフト/還元衝突: 199 個が見つかりました, 0 個は期待通りです parse.tmp.y: エラー: 還元/還元衝突: 759 個が見つかりました, 0 個は期待通りです parse.tmp.y: ノート: '-Wcounterexamples' オプションをつけて競合の反例を生成するために再実行 ...数分待っても終了しない...
これを見るかぎり、LALR から IELR に買えても衝突の数は変化しない。 (シフト/還元衝突が4個、還元/還元衝突が3個)
(ついでに、Canonical LR は遅すぎて使い物にならなさそうなことがわかる。)
というわけで、少なくとも IELR にするだけですぐに問題が解決する、というわけではない。
IELR でなにか変化が起こるかもしれないけれど、それが役に立つかどうかはここからはわからない。
構文解析の論文を探していて、以下のふたりがいろいろ書いているのに気がついた。
気になる文献がいくつかある。
まず、lexer が token の並びではなく、TWE (Token With Extents) の集合を生成する、というアイデアの話があった。 extents というのは token の開始位置と終了位置なので、字句解析があいまいでなければ位置でソートすれば token の並びと同じになる。 でも字句解析がそこまで決定的にするのが難しければ、複数の可能性を残して構文解析のほうでどうにかするという話のようだ。
あと、以下のふたつも気になった。
やはり DSL を埋め込むというのはいちばん典型的なモチベーションなのか、 文法をモジュール化して import するという話。 import するときに導出規則を削るとかの話もある。
Safe Specification of Operator Precedence Rules
SDF の演算子優先順位規則は不完全で、まともにしよう、という話。
まず SDF の演算子優先順位規則の定義がちゃんと書いてあるのがよい。
論文だと全部は説明できないのはしょうがないので、マニュアルはないか探すと、以下がそうなのかなぁ。
しかし、SDF で記述されていて、自然言語による説明はあまりない感じ?
気がついたのだが、GLR を使って Ruby のパーサを書いた例があるようだ。
The ruby intermediate language [著者ページ]
これは dypgen という parser generator を使っている。
dypgen -- Self-extensible parsers and lexers for OCaml
選択肢の刈り込みは OCaml のコードで行うみたいだな。
parser の理解のしやすさについて考えていてふと思ったのだが、LR parser の動作は非決定的な処理を並行に進めるというものなので、 並列プログラミング同様に、人間の理解を越えがちという問題はあるかもしれない。
そう考えると、 並列プログラミングにおいてモデルチェッカで到達可能な状態をすべて確認するのと、 LR parser generator が決定的オートマトンを作って conflict を検出するのは対応しているのかもしれない。 それらによって、到達可能なすべての状態においてなにが起こるかを確認し、変な事が起きないことを静的に保証できる。
GLR で CFG をなんでもパースするというのは、そういう静的解析を使わない並行プログラミングなのかもな。
あと、手書きでパーザを書くのは素直には並行処理になるものをがんばって逐次処理で書くことになるのかもしれない。
SDF3 や Silver を眺めながら考えると、結局、lexer と parser を分けるのはモジュール化なので、一般のモジュール化の利点欠点がここでも成り立つのかもしれないと思いついた。
SDF3 が SGLR で parser と lexer をいっしょくたにして扱うといっても、人間は parser と lexer を分けて記述するわけだし、 モジュール化には利点があるのだろう。
Grok にモジュール化の利点欠点を尋ねたところ、以下の回答が返ってきた。 まぁそれっぽい。
利点
欠点
これを lexer と parser のモジュール分割について考えてみる。
利点
欠点
こんなもんかなぁ。 parser と lexer の話に限定した話を取り出すと、以下くらいかな。
利点
欠点
なんにせよ、lexer と parser の間のよいインターフェースのデザインが問題と思う。
Silver: An extensible attribute grammar system を眺めると、 これは lexer と parser の厄介な関係にはほとんど触れられていない。 この論文では属性文法をどう使っているかという話が主題。
Context-Aware Scanning for Parsing Extensible Languages [PDF] とかで 説明されている Context-aware scanner のままということだろう。
属性文法については、煩雑だけど、ここで扱おうとしている言語の組み合わせ (ホスト言語に DSL を埋め込むとか) をシステムが支援するにはそういうのもひとつの方法かな、というくらいの感想をもった。
なおこの論文においては、属性文法は lexer の動作には影響しないと思う。 Context-aware scanner は LR parser の lookahead 集合を lexer に渡すというだけで、属性文法から lexer に影響を与える方法は述べられていないと思う。 あと、Silver において属性の計算はパース時に行うと限定されておらず、一般には属性の計算結果を使って lexer に影響を与えるのは無理。 (属性文法をつかって lexer に影響を与えるなら、パース時に属性計算を行って lexer に情報を提供する必要がある)
Multi-purpose Syntax Definition with SDF3 を眺めると、 SGLR を前提とした文法記述だが、parser と lexer に相当する記述は分かれている。
これは、トークン間の空白 (およびコメント) を文法としてぜんぶ書くのは面倒くさいので、 自動的に規則に空白の記述を挿入するためのようだ。 (なお、空白のことをレイアウトと呼んでいる。Python などのように indent 依存な文法を記述する方法もあって面白い)
ところで、lex などの lexer generator には最長一致といった規則があって、これは曖昧なパターンを解決する規則とみなせる。 これをそのまま SGLR で扱うと、曖昧なパターンから曖昧な構文木が生成されてしまうが、それを防ぐ方法がある。
まず、通常 lexer は最長一致で動作する。 たとえば、識別子が英数字として、foobar という入力を先頭から読む場合、識別子として f, fo, foo, foob, fooba, foobar のいずれかを認識可能である。 最長一致では foobar だけが認識される。ここではこの foobar がユーザが欲しいトークンだとしよう。
あと、最長一致したパターンが複数ある場合、(旧来的な lexer では) どれかひとつを選ばなければならない。 たとえば、if は IF というトークンとし、[a-zA-Z][a-zA-Z0-9]* は ID というトークンとする場合、 入力が if ならば、IF と ID のどちらが生成されてもおかしくない。 旧来的には (lex とかでは)、先に書いておいたほうが生成される。 また、if を常に ID にしてほしいなら IF の規則は不要なので、おそらく IF を優先してほしいというのが意図だろう。 (ここでは Ruby のように文脈に応じて変化するというのは考えない)
このように最長一致とキーワードの認識を SGLR ベースで実現するために、SDF3 は follow restriction と reject production という記述が可能になっていて、以下のように書けば実現できるようだ。
ID = [a-zA-Z] [a-zA-Z0-9]*
ID -/- [a-zA-Z0-9]
ID = "if" {reject}
最初の ID = [a-zA-Z] [a-zA-Z0-9]* が基本的な識別子の規則で、 ID -/- [a-zA-Z0-9] が follow restriction, ID = "if" {reject} が reject production である。
follow restriction により、ID が認識された直後に [a-zA-Z0-9] が出現した場合にはそのように認識する選択肢は除去する。 reject production により、"if" という 2文字が ID として認識された場合にはその選択肢は除去する。
これらにより、旧来的な lexer が行う最長一致とキーワードの認識を実現している。 (もちろん、if を IF にする規則は別に記述する必要がある)
follow restriction と reject production では済まない場合にどうしたらいいかというと、 複数の選択肢が残っている曖昧な構文木が生成されるので、後からどうにかする、という手段はある。
これで、最長一致とキーワードの認識が実現できることはわかったが、他の問題に対応することは可能だろうか。 (たとえば、Ruby の lexer を実現できるだろうか。)
そういうことを考えると、SGLR で、曖昧な木が生成されたときにそれを刈り込むコードを記述できればもっとも一般的だろうと思う。 でも、SDF3 でパースの最中に、なにかコードを実行して選択肢を刈り込むことが可能かというと、 そういう方法はこの論文では説明されていない (と思う)。 ただ、SDF3 では文法の記述をパースだけじゃなくていろいろな用途に使う。 なので、そういうなにが起こるかわからないコードを動かすのはパース以外の処理でどう扱っていいか分からないので、導入困難だと思う。 というわけで、そういう方法は存在しないか、あったとしても使ってほしくない機能になるだろう。 あと、SDF3 はプログラミング言語ではないので、そういうコードをどんな言語で記述するか、という問題もあるか。
でもそうだとすると、lexer と parser の難しいインタラクションは曖昧な構文木が生成されるから、パースが終わったあとで処理する、という形になるのだろうな。
SGLR と CAS+LR に性質の違いがあるとして、それぞれを使ってどういうツールが作られたのか調べてみた。
parser と lexer の関係が単純でない言語はそういうツールでどう扱われることになるのだろうか。
Multi-purpose Syntax Definition with SDF3
SGLR については、SDF3 という syntax definition formalism (文法を定義する形式) になったようだ。
Silver: An extensible attribute grammar system
CAS+LR は Silver という属性文法のシステムになったようだ。