A General Approach to Define Binders Using Matching Logic
- A General Approach to Define Binders Using Matching Logic
- Xiaohong Chen and Grigore Rosu
- Technical Report http://hdl.handle.net/2142/106608, March 2020
- Abstract. We propose a novel shallow embedding of binders using matching logic, where the binding behavior of object-level binders is obtained for free from the behavior of the built-in exists-binder of matching logic. We show that binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, etc., can be defined in matching logic. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system iff it is provable in matching logic. An appealing aspect of our embedding of binders in matching logic is that it yields models to all binders, also for free.We show that models yielded by matching logic are deductively complete with respect to the formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete, a desired property that is not enjoyed by many existing lambda-calculus semantics.