PaperlayerView exact revision on arXiv

Source-linked AI summary

Dependently Typed Model Composition for Matching Logic

Ádám Kurucz, Péter Bereczky, Dániel Horpácsi

arXiv:2609.34892v1cs.LO

TL;DR

K theories are built from modules, motivating a compositional way to combine their signatures, theories, and models while preserving satisfaction. The paper defines gluing in a sorted, polyadic matching logic setting and establishes that gluable models satisfying their respective theories yield a model satisfying the merged theory.

  • Problem

    K theories combine modules, motivating a model-theoretic account of composing constituent theories and models while preserving satisfaction.

    Source: §1 · p. 1, §3 · p. 6

  • Method

    The paper defines signature and theory combination and gluing for compatible structures in a polyadic, many-sorted matching logic framework using dependent types.

    Source: §3 · p. 6, §3.4 · p. 12, §5 · p. 16

  • Results

    For gluable models, if each model satisfies its respective theory, the glued model satisfies the combined theory.

    Source: §3.4 · p. 12

  • Takeaways & Limitations

    Gluing preserves satisfaction proofs for the merged theory, providing a theoretical basis for composing validated models.

    Source: §3.4 · p. 12, §5 · p. 16

    The paper does not define syntactic proofs, so positivity of patterns is outside its definitions, although positivity matters for soundness proofs of a deduction system.

    Source: §2 · p. 4

Abstract

from arXiv · show

This paper investigates model composition—often referred to as "gluing"—within the framework of matching logic. Specifically, we examine the systematic combination of existing signatures, variable valuations, theories, and their corresponding models. Our primary objective is to ensure that this composition preserves satisfaction proofs; that is, any theory validated by the individual constituent models is also validated by the resulting composite model. Our definitions are based on a polyadic, sorted variant of matching logic, which has also been expressed in the Rocq proof assistant. Therefore, we outline our definitions with dependent types for this work to serve as a direct blueprint for the mechanization in the short-term future.

1 Introduction

Matching logic theories in K are assembled from reusable modules, making model composition central to compositional consistency verification. This paper defines gluing for compatible signatures, theories, and models in a sorted, polyadic setting, with satisfaction preserved.

1 Introduction

  • K theories combine modules for language subcomponents and reusable constructs, so their consistency can be verified compositionally from models of the constituent theories.Once standard-module theories are shown consistent, those arguments can be reused for larger theories that depend on them.Source: §1 · p. 1
  • The work targets consistency verification for K theories and presents matching µ-logic as capturing the essential challenges despite Kore being richer.The presentation is restricted to the original matching µ-logic formalism.Source: §1 · p. 1
  • Gluing combines compatible signatures, theories, and models while preserving satisfaction proofs, establishing consistency of the resulting theories.The definitions use dependent types as a blueprint for Rocq implementation based on existing formalization.Source: §1 · p. 1
  • The paper uses intrinsically sorted matching logic with polyadic symbol applications, unlike related work based on an applicative, unsorted variant.Sortedness avoids extending the logic for sorted quantification, while polyadic applications eliminate junk values from partial or ill-sorted applications.Source: §1 · p. 2

2 Matching logic

The section introduces matching logic syntax, semantics, and its dependently typed representation. It uses sorted patterns and locally nameless variables, then encodes sorts and binding environments in types to support mechanization.

2 Matching logic

  • Patterns combine term- and formula-like constructs, including variables, negation, conjunction, quantifiers, fixed points, and symbol applications.Patterns are sorted, and locally nameless representation uses names for free variables and de Bruijn indices for bound variables, avoiding reasoning about α-equivalence and simplifying capture-avoiding substitution.Source: §2 · p. 2
  • Capture-avoiding substitution replaces a variable with a same-sorted pattern; under binders, de Bruijn indices are adjusted to account for quantifier depth.Only dangling bound variables can be substituted.Source: §2 · p. 3
  • A model assigns a non-empty carrier to each sort and interprets each symbol as a function from its argument carriers to subsets of its result carrier.Element variables range over carrier elements, while set variables range over carrier subsets; pattern interpretations map patterns to subsets of carriers.Source: §2 · p. 3
  • Satisfaction means a pattern denotes the full carrier under every valuation, and a model satisfies a theory when every pattern in it holds.The semantics assigns the empty set to dangling bound variables for totality, although only closed patterns should be evaluated.Source: §2 · p. 4
  • The dependent encoding indexes patterns by sort and binding environments, so ill-sorted or ill-scoped patterns cannot be constructed.Heterogeneous lists represent arguments of polyadic symbols with different sorts; membership proofs serve as de Bruijn indices, and quantifiers extend the environments.Source: §2 · p. 5
  • Models and valuations are represented dependently, and theories use dependent pairs because patterns of distinct sorts have different types.The machine-checked semantics includes branches for element variables, conjunction, application, and existential quantification; the paper does not define syntactic proofs, so positivity is not relevant to its definitions.Source: §2 · pp. 5–6

3 Combining models

This section develops gluing to combine signatures, models, and theories while preserving satisfaction, distinguishing it from model extension and specifying how combined signatures and patterns are constructed. It illustrates the construction by identifying compatible sorts and symbols while keeping incompatible interpretations separate, and establishes satisfaction of the combined theory in the glued model, with model extension likewise reduced to gluing.

3.1 Combination of signatures

  • Signature combination generalizes disjoint union to allow shared sorts and symbols, requiring agreement on shared definitions while excluding junk values.Disjoint unions suit distinct concepts, but cannot express equality of shared carrier sets; a subsorting relation with antisymmetry can identify sorts.Source: §3.1 · pp. 7–8
  • Signature combination is commutative, associative when the required combinations exist, and idempotent up to equivalence, making signatures a semilattice under gluing.The resulting order places each constituent below its combination.Source: §3.1 · pp. 9–10

3.2 Syntax lifting

  • Pattern lifting recursively reconstructs patterns from lesser signatures in greater ones, resolving incompatibility between patterns indexed by different signatures.The paper also defines an inverse operation, unlift.Source: §3.2 · p. 10

3.3 Model gluing

  • Gluable models require combinable signatures and equivalent carriers and interpretations wherever sorts or symbols are shared; the glued model dispatches operations to its constituents.Agreement on the model field inh is omitted because its specific value is irrelevant to equivalence.Source: §3.3 · pp. 10–11

3.4 Satisfaction

  • Merged theories lift each constituent’s axioms into the combined signature, while valuation unlifting is total but lifting valuations cannot form a partial isomorphism.The merged theory is the proper union of the input axioms, although a combined signature could admit additional axioms; the satisfaction proof relies on merging adding only lifted axioms.Source: §3.4 · p. 12
  • If gluable models M1 and M2 satisfy Γ1 and Γ2, respectively, their glued model satisfies the merged theory combineT Γ1 Γ2.The paper states this as Proposition 5 and provides a proof sketch in Appendix E.Source: §3.4 · p. 12

3.5 Example

  • The example introduces two similar signatures and corresponding models, including outputs {true} and {1} when n is even.The supplied excerpt does not identify which output belongs to which model.Source: §3.5 · p. 13
  • The booleans cannot be identified: their carriers are non-isomorphic, so isEven, twice, and thrice must also remain separate where their sorts or interpretations differ.Although identifying the booleans could produce a signature useful for syntax or suitably interpreted semantics, it cannot glue these specific models.Source: §3.5 · p. 14
  • Isomorphic nat and pos carriers and agreeing plus and add interpretations allow a gluable model, while the shared number type and addition can be merged.The signature conditions also hold because sorts and symbols are mapped, variable types are strings, and the shared addition has matching argument and return sorts.Source: §3.5 · pp. 13–14
  • M1 and M2 each satisfy their constituent theories: the positive multiples axioms cover the positive integers or, with zero, the natural numbers, and the boolean-related axioms evaluate to their carriers.For M2, the second axiom uses that n is even exactly when 3·n is even, making its set of results N despite the natural-number carrier.Source: §3.5 · p. 14
  • The combined theory applies signature renaming, removes duplicate lifted patterns after simplification, and contains no new patterns despite permitting additional expressions.For example, isEven from Γ2 becomes c_isEven; the satisfiability of additional possible axioms can still be examined separately.Source: §3.5 · p. 15
  • Proposition 5 proves satisfaction of the combined theory in the glued model without additional reasoning.The accompanying diagram relates matching-logic constructs to the combination functions used at each step.Source: §3.5 · p. 15

Thoughts on model extension

  • Model extension can be defined by adapting gluing or reducing extension to gluing, assembling the needed signature, theory, and model from added axioms and required sorts and symbols.The paper refers to Appendix G for further discussion.Source: Thoughts on model extension · p. 15

4 Related work

Prior model-gluing approaches either require disjoint carriers or constrain patterns to an open fragment. This work instead gives a constructive framework for combining non-disjoint signatures and models in sorted, polyadic matching logic.

4 Related work

  • In prior LTL model checking work, preservation is ensured by restricting axioms to the open fragment, which bars quantification beyond the initial signature.That work uses applicative, unsorted matching logic and treats concepts such as definedness and injection through special axiomatic symbols.Source: §4 · p. 15
  • The sorted, polyadic variant handles sorted quantifiers natively and avoids auxiliary symbols and the open-fragment restriction, though its dependently typed syntax is harder to work with.The syntax uses heterogeneous lists.Source: §4 · p. 16
  • Earlier model gluing requires disjoint carrier sets, so overlapping elements cannot be directly combined by those approaches.Universal-logic and category-theory frameworks address logics sharing structural elements.Source: §4 · p. 16
  • Institution Theory relates signature pushouts to model amalgamation squares, connecting syntactic unions with models that satisfy theories translated into the combined signature.Model amalgamation embeds two models into one structure while preserving the behavior of their overlap.Source: §4 · p. 16
  • The proposed operational union handles overlaps with partial isomorphisms and lifts patterns through a partial order instead of variable substitution.It applies universal-algebraic tools to combine non-disjoint signatures and corresponding models.Source: §4 · p. 16

5 Conclusion and future work

The paper establishes a dependent-type foundation for composing signatures, valuations, and models in polyadic, many-sorted matching logic while preserving satisfaction proofs. The definitions provide a blueprint for formalization, but machine-checked verification remains future work.

5 Conclusion and future work

  • The paper establishes a theoretical foundation for composing signatures, variable valuations, and constituent models in polyadic, many-sorted matching logic.It argues that essential satisfaction proofs are preserved in the composite architecture.Source: §5 · p. 16
  • Dependent-type definitions provide a blueprint for machine-checked formalization and future automation.The mechanisms themselves do not yet have a machine-checked formalization; implementing and checking them is the immediate next step.Source: §5 · p. 16
  • Automation is envisioned as conditional on suitable infrastructure, such as a global collection of known isomorphic types.Such infrastructure could support instantiating type classes for systematic model definitions of composite theories, potentially from K.Source: §5 · p. 16

A A brief introduction to dependent types

The appendix introduces dependent-type constructions used by the paper, from inductive data types to indexed and dependent structures. These constructions encode membership, length, and element types in types themselves.

A A brief introduction to dependent types

  • The metatheory is a variant of the Calculus of Inductive Constructions with native inductive definitions, while universe levels are left implicit in the presentation.The formalization still relies on Rocq to infer and enforce universe levels, without using type-in-type.Source: A A brief introduction to dependent… · p. 19
  • Lists, sum types, and option types provide basic inductive structures, with lists using nil and cons and sums using tagged injections.Option extends a type with Some and an explicit None value.Source: A A brief introduction to dependent… · p. 19
  • Vectors are lists indexed by their length, with the empty vector indexed by zero and each cons increasing the tail’s length by one.The vector length appears as a type index.Source: A A brief introduction to dependent… · p. 19
  • Dependent pairs allow the type of the second component to depend on the first, enforcing agreement between a value and its type index.The appendix writes them as {x : A & P x}.Source: A A brief introduction to dependent… · p. 19
  • Membership judgments are inductive proofs that also encode an element’s position; the number of cons constructors supplies a de Bruijn index.The constructors represent membership at the head or in the tail.Source: A A brief introduction to dependent… · pp. 19–20
  • Heterogeneous lists are indexed by an index list and a type mapping, so each element’s type corresponds to its index.They have the same length as the index list; the appendix uses them in Section 2.Source: A A brief introduction to dependent… · p. 20
  • Record syntax names constructor parameters as fields, allowing values to be accessed through those field names.For a record rec, field1 rec denotes its first field.Source: A A brief introduction to dependent… · p. 20

B Implicit simplification in lift

The appendix explains how an input of type EV Σ can be used where EV Σ1 is required under the subsort relation.

B Implicit simplification in lift

  • Under the subsort hypothesis, the input variable of type EV Σ can be used where EV Σ1 is required.The example uses simplification to ensure the definition is type-correct.Source: B Implicit simplification in lift · p. 20

C The unlift function

Unlift is an optional inverse of lifting defined by recursive case analysis. Its partiality is concentrated in existential quantification, which lets a combined signature host patterns beyond those of its constituents.

C The unlift function

  • Unlift handles base cases successfully and reconstructs recursive patterns only when all recursive calls succeed.Bound variables represented by In proofs are adjusted using Lemma 2 (In_map_r).Source: C The unlift function · p. 21
  • For applications, the argument pattern's type requires the symbol's return sort to match, allowing reconstruction only for a symbol in Σ1.Source: C The unlift function · p. 21
  • Existential quantification is the only case that can fail independently, so unlift returns an optional pattern.Source: C The unlift function · p. 21
  • Quantifiers over a combined signature can use bound-variable sorts absent from a smaller signature, so the combined signature may host more patterns than its constituents; lift and unlift form a partial isomorphism.Source: C The unlift function · p. 22

D Implicit simplification in app

The definition of app relies on implicit type simplification to move from a combined-signature symbol condition to an application in Σ1. These conversions use equalities and dependent-type simplification; the paper omits transport's definition and usage.

D Implicit simplification in app

  • A symbol that maps back to a symbol σ1 in Σ1 can be used to construct app σ1 xs once the argument list is converted to the required type.Source: D Implicit simplification in app · p. 22
  • The argument-list type is converted using the combined parameter and return definitions, the glued carrier definition, and function η-expansion.Source: D Implicit simplification in app · p. 22
  • These conversions rely on simplifying with equalities such as H1, while the definition and usage of transport are omitted.The paper notes that many type theory systems use transport when simplification with equalities is unavailable.Source: D Implicit simplification in app · pp. 22–23

E Proof sketch of satisfaction preservation

The proof sketch starts from constituent models satisfying their respective theories and targets satisfaction of the combined theory in the glued model. It uses unlifteval to connect component evaluations to the target, then completes the generalized proof by induction on patterns.

E Proof sketch of satisfaction preservation

  • The component assumptions state that each theory's members evaluate to the top carrier in its own model.Source: E Proof sketch of satisfaction… · p. 23
  • The target is that every member of the combined theory evaluates to the top carrier in the glued model for every sort, pattern, and valuation.Source: E Proof sketch of satisfaction… · p. 23
  • Instantiating the component statements with unlifteval yields a true evaluation in either component model; rewriting and induction on the remaining pattern complete the generalized proof.The generalized induction allows arbitrary existential and least-fixed-point environments.Source: E Proof sketch of satisfaction… · p. 23

F Detailed example diagram

The diagram relates matching-logic concepts to the functions defined in the paper. Horizontal arrows show signature-governed applications and sorts, while vertical arrows show the functions introduced in the paper.

F Detailed example diagram

  • Horizontal arrows connect concepts whose applications and satisfaction-checking sorts are governed by the signature; vertical arrows represent the paper's functions.Semantic application interpretations are shown as branches from the relevant horizontal arrows.Source: F Detailed example diagram · p. 23

G Thoughts on model extension

Extension adds sorts, symbols, or theories to an existing structure, unlike gluing, which combines structures as a union. The paper describes specification-based and gluing-based approaches, with different proof obligations for their properties.

G Thoughts on model extension

  • Extension adds sorts, symbols, or theories to an existing structure, and the added elements should not invalidate existing satisfaction proofs.Unlike gluing, which combines two structures as their exact union, extension embeds only part of a structure into another.Source: G Thoughts on model extension · p. 24
  • The specification-based approach extends sorts and symbols by relaxing their no-junk conditions and requiring user-supplied functions for new sorts and symbols.For new sorts, these functions determine variables and carrier sets; for new symbols, they provide parameter and return sorts and interpretations.Source: G Thoughts on model extension · p. 25
  • Specialized families of axioms for new sorts can be proven using captured proof schemes, allowing these theory extensions to be automated.Arbitrary axioms can instead be expressed as patterns in the combined signature and joined to existing theories with separate satisfaction proofs.Source: G Thoughts on model extension · p. 25
  • Reordering extensions and distributing extension over gluing require separate proofs in the specification-based approach.These properties are reordering independence and distributivity, respectively.Source: G Thoughts on model extension · p. 26
  • The gluing-based approach treats new sorts as a disjoint union and groups functions for new elements into a model that can be glued to the existing model.The parameter and return sorts of new symbols are then provided in the usual way.Source: G Thoughts on model extension · p. 26
  • Theories must be joined in the same way under both approaches, while reordering and distributivity follow as instances of gluing properties.The stated derivation uses commutativity, associativity, and idempotence.Source: G Thoughts on model extension · p. 26
Loading 2609.34892v1…