Source-linked AI summary
Complete Heyting Algebra Semantics for an Intuitionistic Version of Matching Logic (Extended Abstract)
Horaţiu Cheval
TL;DR
The paper asks how to formulate intuitionistic Matching Logic, whose classical form supports language-independent reasoning about program executions. It introduces complete-Heyting-algebra semantics and a proof system, and proves that system sound relative to the semantics. Completeness and practical validation remain open.
Problem
The paper addresses how to formulate an intuitionistic version of Matching Logic, a logic designed for language-independent reasoning about program executions.
Source: §1 · p. 1Method
The paper interprets iML patterns as maps from a domain into a complete Heyting algebra and proposes a Hilbert-style intuitionistic proof system.
Source: §2.1 · pp. 2–3, §2.2 · p. 3Results
Theorem 2 establishes that derivability in the proposed system implies semantic entailment.
Source: §3 · p. 5Takeaways & Limitations
The authors present this first attempt at intuitionistic Matching Logic as a starting point for further research.
Source: §4 · p. 7Completeness remains open, and the authors have not yet validated practical expressivity or ruled out missing proof rules in practice.
Source: §4 · p. 7
Abstract
from arXiv · showhide
We present work in progress towards an intuitionistic version of Applicative Matching Logic. We introduce a semantics based on complete Heyting algebras, and propose a proof system which we prove to be sound relative to this semantics.
1 Introduction
Matching Logic is designed for language-independent reasoning about program executions, and this paper proposes an intuitionistic version. It treats patterns as both terms and formulas, with their interpretations grounded in a model and valuation.
1 Introduction
- Matching Logic is a minimal, expressive logic for language-independent reasoning about program executions and underlies the K program verification framework.The paper focuses on its recent Applicative Matching Logic version.Source: §1 · p. 1
- The paper proposes an intuitionistic version of Matching Logic, whose single kind of pattern serves as both terms and first-order formulas.Source: §1 · p. 1
- A model fixes a domain, symbol interpretations, and application, while valuations assign domain elements or subsets to variables.Source: §1 · pp. 1–2
- Positivity for a fixed-point variable makes its interpretation monotone, ensuring a least fixed point exists.The paper invokes the Knaster–Tarski theorem.Source: §1 · pp. 1–2
- Classical Matching Logic has a sound and conditionally complete proof system.Source: §1 · p. 2
2 Intuitionistic ML
The paper introduces iML by extending Matching Logic's pattern syntax and interpreting patterns with values in a complete Heyting algebra. It also proposes an intuitionistic Hilbert-style proof system with separate least- and greatest-fixed-point rules.
2 Intuitionistic ML
- iML explicitly includes conjunction, disjunction, universal quantification, and greatest fixed points; bottom is defined as µX.X, negation as implication to bottom, and fixed-point bodies must be positive.Source: §2 · p. 2
2.1 Semantics
- Instead of subsets, iML patterns denote maps M→H, where H is a complete Heyting algebra and M is a set.Element variables range over M and set variables over H-valued maps on M.Source: §2.1 · pp. 2–3
- Positivity makes the interpretation map monotone, so Knaster–Tarski supplies least and greatest fixed points for the µ and ν constructors.Source: §2.1 · p. 3
2.2 Proof system
- The proof system uses standard intuitionistic propositional and first-order rules, splits least- and greatest-fixed-point rules, and retains the classical application rules as intuitionistically valid.The split reflects that classical inter-derivability appears to require double negation elimination.Source: §2.2 · pp. 3–4
- Application contexts are nested applications with a hole, and the system derives ex falso from the definition of bottom rather than including it as a rule.The paper also omits PROPAGATION⊥, noting it can be derived with FRAMING and SINGLETON.Source: §2.2 · p. 4
3 Soundness
The paper proves that derivability in its iML proof system implies semantic entailment. The soundness proof is sketched by induction on derivations and was developed alongside a Lean formalization that helped rule out early unsound or degenerate systems.
3 Soundness
- The Lean formalization was developed in sync with the theory and helped rule out early unsound or degenerate versions of the system.The authors say this was not an autoformalization of a result already fully written on paper.Source: §3 · p. 4
- Γ ⊢ ϕ implies Γ |= ϕ: the proposed iML proof system is sound with respect to the semantics.The proof is sketched by induction on derivations.Source: §3 · p. 5
- The proof treats propositional and first-order rules as standard, sketches the EXISTENCE case, and focuses on selected FRAMING and PROPAGATION cases.The other sides of the selected FRAMING, PROPAGATION∨, and PROPAGATION∃ cases are handled analogously.Source: §3 · p. 5
- For SINGLETON, the proof reduces to the case where both elements equal ρEV(x), then uses h⊓(h⇒⊥)=⊥.The proof first uses the bound in Lemma 3 and frame distributivity.Source: §3 · p. 6
- The PREFIXPOINT and KNASTER-TARSKI cases use the least fixed point of F(A)=|ϕ|ρ[X↦A]; the ν cases are analogous.The prefixpoint argument uses that lfp(F) is a fixed point, while the Knaster-Tarski argument bounds it by any prefixpoint.Source: §3 · pp. 6–7
4 Conclusions and future work
The paper presents an initial intuitionistic semantics for Matching Logic, while leaving completeness and practical expressivity open. It identifies equality and several metatheoretical questions as directions for future work.
4 Conclusions and future work
- Completeness remains open, and practical expressivity and the possibility of missing proof rules—especially at the interaction of logical and applicative fragments—remain to be assessed.The authors describe the axiomatization as a natural adaptation but cannot rule out missing rules in practice.Source: §4 · p. 7
- A first proposed step is to study the intuitionistic setting's ML-specific derived equality, introduced using the theory of definedness.Source: §4 · p. 7
- Further proposed investigations include disjunction properties, realizability semantics, negative translations, and whether Kripke models suffice for completeness.In this setting, Kripke models arise when H is the algebra of upper sets of a preorder.Source: §4 · p. 7
A Proof system for iML
The iML proof-system material includes a SINGLETON axiom and existential propagation rules. Figure 1 is identified as the proof system for iML.
A Proof system for iML
- The SINGLETON rule states ¬(C1[x∧ϕ]∧C2[x∧¬ϕ]), where C1 and C2 are application contexts.Source: A Proof system for iML · p. 8
- The PROPAGATION∃ rules distribute application across an existential in either position, with x not free in χ.Source: A Proof system for iML · p. 8
- Figure 1 is captioned as the proof system for iML.Source: Figure 1 · p. 8