Philosophy:Matching logic

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 [math]\displaystyle{ \Sigma }[/math], a pattern can be:

• A variable: [math]\displaystyle{ x \in Var }[/math]
• A structure following signature [math]\displaystyle{ \sigma \in \Sigma }[/math] using other patterns: [math]\displaystyle{ \sigma(p_1, p_2, ..., p_n) }[/math]
• The complement of another pattern: [math]\displaystyle{ \neg p }[/math]
• The intersection of two patterns: [math]\displaystyle{ p_1 \land p_2 }[/math]
• A binding: [math]\displaystyle{ \exists x . p }[/math] with [math]\displaystyle{ x \in Var }[/math]

A matching logic may also have a set [math]\displaystyle{ S }[/math] 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:

• [math]\displaystyle{ \top \equiv \exists x . x }[/math]
• [math]\displaystyle{ \bot \equiv \neg\top }[/math]
• [math]\displaystyle{ p_1 \lor p_2 \equiv \neg(\neg p_1 \land \neg p_2) }[/math]
• [math]\displaystyle{ p_1 \implies p_2 \equiv \neg p_1 \lor p_2 }[/math]
• [math]\displaystyle{ p_1 \Leftrightarrow p_2 \equiv p_1 \implies p_2 \land p_2 \implies p_1 }[/math]
• [math]\displaystyle{ \forall x . p \equiv \neg (\exists x . \neg p) }[/math]

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

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