演算子の優先順位というものは小学校で習うわけである。足し算よりも掛け算を優先するとかそういう感じで。
しかし、厳密な定義は、といわれると習った覚えがない。
yacc とかのパーサージェネレータには優先順位を指定する機能があるが、 これは LR構文解析の shift/reduce 競合の解決法を指定するもので、 結局のところどんな状況を目指しているのかというのはわかっていなかった。 優先順位というものは左右対称だと思うのだが、パーサの動作は左右対称じゃないからこれが本質という気もしない。
ところが、最近、演算子の優先順位をちゃんと定義する論文を見つけた。
Precedences in specifications and implementations of programming languages
二項演算子だけなら小学校で習う知識をすこし一般化すればなんとかなるが、単項演算子（前置演算子と後置演算子）を扱うとなるとあまり自明ではない。 とくに、優先順位の低い単項演算子は難しい。 それがちゃんと定義されていてすばらしい。 左右対称だし。
なかなかよいと思うのだが、これは yacc の優先順位と同じものなのだろうか。 それが疑問である。
しばらく自分で考えて、（二項演算子については）ちょっとわかった。 項が作られるのは reduce のときで、shift/reduce conflict が reduce に解決されるのは LR スタックに積まれている規則 (演算子) と lookahead symbol の優先順位を比較して前者の優先順位が高いときなので、 reduce が何回か行われて作られた項 (木構造) の右端に並んでいる演算子はすべて lookahead の演算子よりも優先順位が高いのだ。 (ここで優先順位が同じ場合、左結合と右結合でそれぞれ左右どちらかが高いとみなす)
しかし、これと左右対称な性質 (木構造の左側に並んでいる演算子はその項の左側にある演算子よりも優先順位が高い) は頭の中で考えていても納得できない。 しかたないので AI に相談すると、なぜそうなるかを説明してくれて、（しばらく考えて）納得できた。 shift/reduce conflict で shift が選ばれるのは lookahead のほうが優先順位が高い場合で、そうやって shift したものが後から reduce されることで左にある演算子の下位に入っていくのだな。 上の reduce が連続して起こるのと違って、もうちょっと大きな単位で動作を理解しないと納得できない話であった。
あと、ここまでは二項演算子だけの話だが、単項演算子は前置と後置それぞれでまた考える必要がある。 でも LR 構文解析の動作を頭のなかでイメージできればなんとかわかる。
前置演算子が出現するのは項の先頭で、ここでは shift/reduce conflict がないので、即座に shift される。 その後で、前置演算子の優先順位よりも高い演算子で構成された塊がひとつの項としてまとまり、その後で前置演算子とその項が reduce される。 この塊の中の演算子は、前置演算子と優先順位が比較されることはあるが、前置演算子よりも前に出現した演算子との比較は起きない。 だから、高い優先順位の二項演算子の右引数に低い優先順位の前置単項演算子があると、その内部にはかっこなしで二項演算子よりも低い優先順位の演算子が出現することがある。 たとえば、OCaml の if 式が（単項演算子じゃなくて 3項演算子だけど）そういう性質を持っている。 2 * if b then 3 else 4 + 5 という式は 2 * (if b then 3 else (4 + 5)) と解釈される。 OCaml では、乗算、加算、if 式、という順番の優先順位になっている。 乗算の優先順位よりも if 式の優先順位が低いため、if 式の (else 節) 内部の加算は if 式と優先順位が比べられ、加算の優先順位が高いので、 if 式の内部の式と解釈される。 乗算と加算の優先順位の比較は行われない。
後置演算子も、LR構文解析の動作は違うのだが、結局は似たような結果になる。 後置演算子が lookahead になったときに、それよりも優先順位の高い塊はその後置演算子の引数として reduce され、後置演算子よりも後で出現する演算子の優先順位は関知されない。
さて、こうやって納得したのはいいのだが、ふと思いついて、 Claude Code に Rocq (と mathcomp) でこのことを証明するように指示してみた。 そうすると、たいしてかからずに（測らなかったけど10分くらい?）で証明を作ってきた。
出来上がったものは以下にある。
<URL:https://gist.github.com/akr/50d9c2ac265b0ec9b1dac6e84dda7381>
出来上がったはいいが、これが本当に期待した性質を証明しているかどうかは自分で確認する必要がある。 証明の本体は読まなくても、命題の部分は読まないといけない。
ということで、命題の部分（およびその内部で参照している部分）だけを取り出してきた。 証明ぜんぶだと 450行くらいあるが、命題だけだと160行くらいなので、ずいぶんと短くなっている。
(** * Aasa (1995) の precedence correct と yacc 流 shift/reduce 競合解決の一致
A. Aasa, "Precedences in specifications and implementations of
programming languages", TCS 142 (1995) 3-26.
曖昧な文法
<<
E ::= E inl E | E inr E | pre E | E post | atom
>>
に対し、
- 論文 Definition 3/4 の Lw, Rw, Pc (ここでは [pc]) を定義し、
- yacc/bison が生成する LR 構文解析器 (shift/reduce 競合を
%left/%right と優先順位で解決したもの) をスタック機械 [parse] として
モデル化し、
- [parse ts = Some t <-> pc t /\ flatten t = ts] を証明する。
副産物として論文の Theorem 12 (各文にちょうど一つの precedence correct
な木が存在する) も得られる。
優先順位の向きは論文に従い「数が大きいほど結合が弱い」。
yacc では後に宣言した行ほど結合が強いので、数は宣言順の逆になる。 *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(** 演算子の種類 (論文の Left, Right, Pre, Post) *)
Inductive kind := InL | InR | Pre | Post.
Section Prec.
Variables atom op : Type.
Variable P : op -> nat. (* 優先順位 *)
Variable kind_of : op -> kind.
(** 論文の仮定: 種類の異なる演算子は同じ優先順位を持たない。
(yacc でも一つの %left/%right 行は一つの結合性しか持たない。)
原子式の重み 0 と区別するため優先順位は正とする。 *)
Hypothesis P_pos : forall o, 0 < P o.
Hypothesis P_kind : forall a b, P a = P b -> kind_of a = kind_of b.
Definition is_infix o := if kind_of o is (InL | InR) then true else false.
Definition is_prefix o := if kind_of o is Pre then true else false.
Definition is_postfix o := if kind_of o is Post then true else false.
Definition is_left o := if kind_of o is InL then true else false.
(** ** 構文木と字句列 *)
Inductive tree :=
| Leaf of atom
| Inf of tree & op & tree
| Pref of op & tree
| Postf of tree & op.
Inductive token := Atom of atom | Op of op.
Fixpoint flatten t :=
match t with
| Leaf a => [:: Atom a]
| Inf l o r => flatten l ++ Op o :: flatten r
| Pref o t => Op o :: flatten t
| Postf t o => flatten t ++ [:: Op o]
end.
(** ** 論文の定義 (Definition 3, 4) *)
Fixpoint Lw t :=
match t with
| Leaf _ => 0
| Inf l o _ => maxn (P o) (Lw l)
| Pref _ _ => 0
| Postf t o => maxn (P o) (Lw t)
end.
(** 論文では Rw(lt op rt) = max(P(op), Lw(rt)) と印刷されているが、
本文の説明どおり Rw(rt) とする。 *)
Fixpoint Rw t :=
match t with
| Leaf _ => 0
| Inf _ o r => maxn (P o) (Rw r)
| Pref o t => maxn (P o) (Rw t)
| Postf _ _ => 0
end.
(** [lbound o w]: 右重み w の木が o の左オペランドになれる。
[rbound o w]: 左重み w の木が o の右オペランドになれる。 *)
Definition lbound o w :=
match kind_of o with InL => w <= P o | InR | Post => w < P o | Pre => false end.
Definition rbound o w :=
match kind_of o with InR => w <= P o | InL | Pre => w < P o | Post => false end.
Fixpoint pc t :=
match t with
| Leaf _ => true
| Inf l o r => [&& is_infix o, pc l, pc r, lbound o (Rw l) & rbound o (Lw r)]
| Pref o t => [&& is_prefix o, pc t & rbound o (Lw t)]
| Postf t o => [&& is_postfix o, pc t & lbound o (Rw t)]
end.
(** ** yacc の LR 構文解析器のモデル
この文法の LR オートマトンの状態はスタックの形で決まる:
- [SA fs] : オペランドを待っている (直前が演算子か先頭)
- [SB fs t] : オペランド [t] を還元し終えた
[fs] は未完了の規則 [E inl . E] / [pre . E] の列 (先頭がスタック最上部)。
競合が起こるのは [SB] で、スタック最上部が [E o E .] または [o E .]、
先読みが中置/後置演算子 [l] の場合だけである。yacc の規則
(規則の優先順位 = 規則中の演算子 [o] の優先順位) により:
- [o] が [l] より強ければ reduce、弱ければ shift
- 同じ優先順位なら %left は reduce、%right は shift
入力終端では常に reduce。原子式 [atom] と後置規則 [E post] は
shift 直後に競合なしで reduce される。 *)
Inductive frame := FInf of tree & op | FPre of op.
Definition fop f := match f with FInf _ o => o | FPre o => o end.
Definition combine f t :=
match f with FInf l o => Inf l o t | FPre o => Pref o t end.
Definition should_reduce o (la : option op) :=
match la with
| None => true
| Some l => (P o < P l) || ((P o == P l) && is_left l)
end.
Arguments should_reduce : simpl never.
Fixpoint reduce fs t la :=
match fs with
| [::] => ([::], t)
| f :: fs' =>
if should_reduce (fop f) la then reduce fs' (combine f t) la else (fs, t)
end.
Inductive state := SA of seq frame | SB of seq frame & tree.
Fixpoint run st ts :=
match ts with
| [::] => if st is SB fs t then Some (reduce fs t None).2 else None
| tk :: ts' =>
match st, tk with
| SA fs, Atom a => run (SB fs (Leaf a)) ts'
| SA fs, Op o => if is_prefix o then run (SA (FPre o :: fs)) ts' else None
| SB _ _, Atom _ => None
| SB fs t, Op o =>
match kind_of o with
| Pre => None
| Post => let: (fs', t') := reduce fs t (Some o) in
run (SB fs' (Postf t' o)) ts'
| _ => let: (fs', t') := reduce fs t (Some o) in
run (SA (FInf t' o :: fs')) ts'
end
end
end.
Definition parse ts := run (SA [::]) ts.
(** ** 主定理: yacc 流の競合解決で得られる木 = 論文の precedence correct な木 *)
Theorem yacc_iff_pc ts t : parse ts = Some t <-> pc t /\ flatten t = ts.
Admitted.
End Prec.
読んでみると、だいたいは論文の定義のままで（論文の間違いの修正はされている）、読むのが面倒なのは LR parser の実行の run 関数あたりくらいだな。 この形式化だと、二項演算子と単項演算子専用になっているので、一般的な LR parser ではない。 でも、run を読んで、頭の中にある LR parser の動作と整合していることを確認すれば、最終的な定理 yacc_iff_pc ts t : parse ts = Some t <-> pc t /\ flatten t = ts を信じることができる。 トークン列 ts を yacc 流に parse した結果、(syntax error がなく) 成功して木構造 t が得られるのと、 論文の pc (precedence correct) という性質が成り立つ木 t の葉を並べたトークン列が ts であることは等価である、という。
というわけで、演算子の優先順位についての長年の疑問が解決してちょっとすっきりした。 もちろんこれはひとつの定義であって、異なる定義がまちがっているというわけではないが、すくなくともひとつ納得できる定義があるということはわかった。
[latest]