Categorial Semantics for OpenMath : OMA

• Application works like STS

  • apply(a,b1,…,bn) is type A · B1 · … · Bn

• Per-symbol type assignments (“lexicalism”)

  • type(sin) = ℂ/ℂ, …
    • Type symbol “ℂ” plugged in from specific type system
  • type(plus) = ℂ/wℂ, …
    • “/w” syntactic sugar for “n-ary abstraction”
  • type(list) = Uw/wU, …
    • “power” type constructor plugged in from specific type system
    • Type symbol “U” (universe) plugged in from “outside”

Notes: