Abstraction and Application

• Lambda abstraction.

  (a: S): R +-> e
  
  (a1: A1, a2: A2, ...): (R1, R2, ...) +-> e
  
  (): () +-> e
  

• Application.
  • f g x associates as f (g x)
  • f.g.x associates as (f g) x
  • f(a)(b) associates as (f(a)) (b)