Categorial Types

• Notation due to Lambek, modified to our needs

• Abstraction A/B – returns something of type A if given argument of type B

  • STS “mapsto(B,A)”; vernacular AB
  • A/B/C/D : three args

• Application A·B – something of type A applied to an argument of type B

  • STS “application(A,B)”; vernacular ??)
  • (A/Z/Y/X) · X · Y · Z “simplifies” to type A

• Plug in any type system (e.g. ECC) for atoms

  • Hence “categorial” semantics / type logic

Notes: