Categorial Semantics for OpenMath : Type Names

• Per-type-symbol type assignment

  • Not(!)
  • But type(ℝ):= 'ℝ' --- i.e. ”name of type reals”
  • Similarly, type(mapping) := ('Y/X'/ 'X' / 'Y'), i.e. ”produces descriptor for type `mapping from X to Y' given descriptors for types X and Y”
  • Note: set names (ℝ,ℂ,ℕ,ℤ,...) are ambiguous
    • On the one hand, type is `power set' for set operations
    • On the other, type is `type name' for type inference

Notes: