Categorial Semantics for OpenMath : OMATTR

• Attribution(a b,e) is type (A · B) · E

  • very different from ECC and STS

• Per-attribute-symbol type assignment

  • type(typeset_as) = ( X/X ) / Y (the “default”)
    • (((X/X)/Y) ·bold) ·ℝ = (X/X) ·ℝ = (ℝ/ℝ) ·ℝ = ℝ
    • Attribute does not affect semantics, but is typed
  • type(type) = (T / T) / ‘T’
    • Unifier to type T given a descriptor for type T
    • ‘…’ (“type descriptor”) for explicit type assignments
    • e.g. (((T/T)/'T') ·'ℝ') ·X = ℝ ; T=X=ℝ, type(x)=X

Notes: