A Term Matching Algorithm and Substitution Generality
summary
Presents a decision procedure that reduces substitution-generality to term matching and implements a deterministic, one-pass matcher adapted from a textbook rewrite algorithm; it builds substitutions in a relaxed core representation that permits passive (fixed-point) bindings and accumulates them on the fly. Uses a TM one-pass matcher plus a triangular witness tableau to prove non-generality by producing divergent bindings; confirms renamings are maximal and explains a classic SLD-completeness counterexample.
AI-written summary · about
chapters (8)
- 0:00Term matching algorithm intro
- 3:59Substitution generality defined
- 6:34Method and results
- 11:10Term matching explained
- 17:29Decision procedure
- 21:56Logic programming importance
- 26:17Conclusions
- 27:22Q&A
related talks
23mType-Level Programming with Match Types
14mRelational Synthesis for Pattern Matching
30mNominal Matching Logic With Fixpoints
29mUnification Modulo Isomorphisms between Dependent Types for Type-based Library Search
23mBetter Defunctionalization through Lambda Set Specialization
56mOn Type-Based Techniques for Program Manipulation
26mAlgorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
20mGenerating Well-Typed Terms that are not "Useless"