Syntactic Operators

The syntactic side is a typed lambda calculus that generates operators on the semantic domain.

Definable operators

Operators are built from:

• primitive constants,
• lambda abstraction and application,
• composition at the base type.

Each definable operator has an interpretation [[f]] : H^n -> H.

Interpretation constraints

An interpreted operator must be:

• monotone in each argument,
• join-continuous,
• compatible with j (modal homomorphism),
• compatible with G (trace homomorphism),
• fragment-preserving.

These constraints ensure that syntax respects the semantic structure.