Categorial Type Logic

• Type inference rules transform types

  • “beta reduction” -- e.g. (A/B/C)·C·B ⇔ A
    • Application is the inverse of abstraction
  • “Currying” (only to a limited extent in OpenMath)
    • (A/B/C)·C·B ⇔ (((A/B)/C)·C)·B
    • A/B/C ⇔ (A/B)/C ; A·B·C ⇔ (A·B)·C
    • E.g. type(log(e))= (ℝ/ℝ/ℝ)·ℝ ⇔ ℝ/ℝ

• Unification of type variables as meta inference rule

  • (X/Y)·ℝ ⇔ X with Y=ℝ; (((T/T)/'T')·'ℝ')·X ⇔ ℝ with X=T=ℝ

Notes: