Categorial Type Logics

• Extensions to basic inference rules

  • Plugged-in concrete type logics
    • Type hierarchies: ℕ ⇒ ℤ ⇒ ℝ ⇒ ℂ
  • n-ary abstraction /w -- beta rule, but no currying
    • (A/wB)·B...·B ⇔ (A/B.../B)·B...·B ⇔ A
    • But: (A/wB)·B·B ↮ ((A/wB)·B)·B
  • Composition – (Y/X) · (X/Z) ⇔ Y/Z
    • e.g. type(sin2+cos2) = (ℝ/ℝ/ℝ) · ((ℝ/ℝ)·(ℝ/ℝ)) · ((ℝ/ℝ)·(ℝ/ℝ)) ⇔ (ℝ/ℝ/ℝ)·(ℝ/ℝ)·(ℝ/ℝ) ⇔ ℝ/ℝ

Notes: