Misplaced Pages

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. Statements evaluate to the set of values that "match" them, not to true or false.

Given a set of signatures ${\displaystyle \Sigma }$, a pattern can be:

• A variable: ${\displaystyle x\in Var}$
• A structure following signature ${\displaystyle \sigma \in \Sigma }$ using other patterns: ${\displaystyle \sigma (p_{1},p_{2},...,p_{n})}$
• The complement of another pattern: ${\displaystyle \neg p}$
• The intersection of two patterns: ${\displaystyle p_{1}\land p_{2}}$
• A binding: ${\displaystyle \exists x.p}$ with ${\displaystyle x\in Var}$

A matching logic may also have a set ${\displaystyle 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:

• ${\displaystyle \top \equiv \exists x.x}$
• ${\displaystyle \bot \equiv \neg \top }$
• ${\displaystyle p_{1}\lor p_{2}\equiv \neg (\neg p_{1}\land \neg p_{2})}$
• ${\displaystyle p_{1}\implies p_{2}\equiv \neg p_{1}\lor p_{2}}$
• ${\displaystyle p_{1}\Leftrightarrow p_{2}\equiv p_{1}\implies p_{2}\land p_{2}\implies p_{1}}$
• ${\displaystyle \forall x.p\equiv \neg (\exists x.\neg p)}$

${\displaystyle \top }$ is matched by all elements. ${\displaystyle \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 ${\displaystyle \mu }$-logic adds a fixed-point operator ${\displaystyle \mu }$.

Applications

Matching logic is used with reachability logic 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

References

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

• Logic