Automated Ambiguity Detection in Layout-Sensitive Grammars
summary
Extends bounded-ambiguity SAT methods to layout-sensitive grammars by replacing SAT with SMT+Z3 and adding a reachability condition to fix a discovered unsoundness in the direct encoding; defines local ambiguity equivalent to bounded ambiguity, encodes it to SMT, and mechanizes soundness and completeness proofs in Coq. Implements a Python checker that returns the shortest nonempty ambiguous sentence when one exists and evaluates on language manuals including YAML and Python with reusable artifacts.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:41Layout-sensitive grammars
- 2:48Ambiguity in grammar design
- 3:54Ambiguous grammar example
- 5:43Bounded ambiguity checking
- 7:53Strengthening local ambiguity
- 11:26Reachability for layout constraints
- 13:56Key takeaways
- 14:59Q&A
related talks
32mA Survey of Weak Reasoning Assistants
07mTooling and Sharing Traceability Discussion
29mDiagrammatic notations for interactive theorem proving
27mProduction Language Specification - Requirements for Multiple Usages
20mNon-Linear Editing of Text-Based Screencasts
20mLooking towards safety
32mPRETTY LITTLE COMPILERS
29mLegalese: Software Eats Contract Drafting