Matching logic explained

Matching logic is a formal logic mainly used to reason about the correctness of computer programs. Its operators use pattern matching to operate on the power set of states, rather than the set of states. It was created by Grigore Roșu and is used in the K Framework.

Overview

Matching logic operates on patterns.^[1] Statements evaluate to the set of values that "match" them, not to true or false.

Given a set of signatures

\Sigma , a pattern can be:

• A variable:

x \in Var

• A structure following signature

\sigma \in \Sigma using other patterns: \sigma(p _{1,} p _{2,} ..., p _{n)}

• The complement of another pattern:

\neg p

• The intersection of two patterns:

p _{1} \land p _{2}

• A binding:

\exists x . p with x \in Var

A matching logic may also have a set

S of sorts. In that case, each pattern belongs to a particular sort. Structures can be used to combine patterns of different sorts together. Some examples of sorts used when working with program semantics might be "32-bit integer values", "stack frames", or "heap memory".

Some derived concepts are defined as:

\top \equiv \exists x . x \bot \equiv \neg\top p _{1} \lor p _{2} \equiv \neg(\neg p _{1} \land \neg p _{2)} p _{1} \implies p _{2} \equiv \neg p _{1} \lor p _{2} p _{1} \Leftrightarrow p _{2} \equiv p _{1} \implies p _{2} \land p _{2} \implies p _{1} \forall x . p \equiv \neg (\exists x . \neg p) \top is matched by all elements. \bot is matched by none.

"One should be careful when reasoning with such non-classic logics, as basic intuitions may deceive."

When interpreting matching logic (that is, defining its semantic meaning), a pattern is modeled with a power set. The statement's interpretation is the set of values that match the pattern.

Matching μ-Logic

Matching

\mu -logic adds a fixed-point operator \mu .^[2]

Applications

Matching logic is used with reachability logic^[3] by the K Framework to specify an operational semantics and, from them, to create a Hoare logic.

Matching logic can be converted to first-order logic with equality, which allows the K Framework to use existing SMT-solvers to find proofs for theorems.

See also

• Separation logic
• Hoare logic
• Regular expression, which matches sets of strings

Notes and References

1. Roșu . Grigore . Matching Logic . Logical Methods in Computer Science . 2017 .
2. Chen . Xiaohong . Roșu . Grigore . Matching μ-Logic . 2019-01-19 . University of Illinois Research and Tech Reports . Computer Science .
3. Roșu . Grigore . ̧Ștefănescu . Andrei . Ciobâcă . Ștefan . Moore . Brandon M. . Reachability Logic . University of Illinois Technical Report . 2012 .