Fragments and Fusion

Fragments are finite substructures that allow local reasoning. Fusion enforces coherence between syntax and semantics.

Fragments

A fragment is a finitely generated subalgebra of H closed under:

• Heyting operations,
• the modality j,
• the trace G.

Fragmentwise reasoning says two operators are equivalent when they agree on all fragments.

Fusion

Fusion identifies syntactic operators whose interpretations agree fragmentwise. It can also add new names for semantic behaviors already present in the system.

The fusion step is a closure operator: it is monotone, inflationary, and idempotent.