WFFの再帰的定義

WFF（well-formed formula）は、ある形式言語の形成規則に従って正しく構成された式である。意味が真か偽かを評価する前に、まず構文として受理できるかを判定する。

仕組みと確認

原子式と結合子・量化子の形成規則を再帰的に定め、パーサで構文木を作る。エラーメッセージでは、最初に規則から外れた位置と期待される構成要素を示す。

限界と注意点

WFFであることは真であることや有用な仕様であることを保証しない。構文検査、型検査、意味検証を別段階として扱う。