SMT-LIB 2.5 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf のシンボルとS式の構文の定義はまずいんじゃなかろうか。というか、頭おかしい。

詳細は省略するが、シンボルの構文はabcのようなシンプルシンボルと呼ばれるものと、|" can occur too| のような Common Lisp 的にクオートされたシンボルの二種類の構文があり、予約語はシンプルシンボルでは表せないことになっている。そして、このシンボルの構文に基づいてS式の構文が定義され、SMT-LIBの各構文(syntactic category)はS式の構文の特殊化(specialization)だと言っている。

が、ちょっと待て！　お前おかしいだろ！　各構文の実際の定義の方では、予約語を直接書く構文になっているが、上記のS式の構文に従うと予約語はクオートしないとシンボルとして書くことが出来ないはずなのだから。

通常の構文をパース・表示する場合には、それぞれの構文の規則に従ってパース・表示するのであまり問題ないのだけれど、まだ標準化されていない部分に関してはS式としてしか規定されていない部分があって問題になることがある。

https://github.com/msakai/Smtlib/issues/1 で問題になった証明項の表現もその１つで、証明項の表現はSMT-LIBではまだ標準化されておらずソルバ依存のため、SMT-LIB上は単にS式としてしか規定されていない。 で、各ソルバはそれぞれ独自のS式を返してくるのだけれど、ソルバによっては証明項の一部として通常の項を含んでいて、その帰結としてlet等の予約語を含んでいることがあったのが問題となった。 SMT-LIB的なS式の定義に従ってこれをパースしようとすると、クオートされていない予約語をシンプルシンボルとしてパースできないのでエラーになるが、これはあまりにも変だ。

SMT-LIBの構文定義は方針をミスっている気がする。 現状では予約語はシンプルなシンボルとしては許容されないけれど、クオートすればシンボルとして書くことができ、識別子としても許容されるけれど、そうするために上記のような変なことが起こってしまっている。 多分、予約語は「シンプルであるかクオートされているかを問わず、シンボルとしては許容する」としたうえで、その上で識別子の概念を定義する際に「予約語は識別子として許容しない」という扱いにするのがシンプルだったのではないかなぁ。

ちなみに、こういう話で思い出すのは、シンボルの扱いについての Common Lisp と Scheme の違いについての https://practical-scheme.net/wiliki/wiliki.cgi?Scheme%3A%E3%83%9E%E3%82%AF%E3%83%AD%3ACommonLisp%E3%81%A8%E3%81%AE%E6%AF%94%E8%BC%83 の話。