The untyped lambda calculus

e ::=
  x
  e e
  λ x. e

• Terms depending on terms

t ::=
  x
  t → t

e ::=
  x
  e e
  λ x : t . e

• Terms depending on terms
• Terms depending on types

k :: =
  *

t ::=
  x
  t → t
  ∀ a . t

e ::=
  x
  e e
  λ x : t . e
  Λ a : k . e

id : ∀ a . a → a
id = Λ a : * . λ x : a . x

• Terms depending on terms
• Types depending on types

k :: =
  *
  k → k

t ::=
  x
  t → t
  ∀ a : k . t

e ::=
  x
  e e
  λ x : t . e
  Λ a : k . e

• Terms depending on terms
• Terms depending on types
• Types depending on types

k ::= *

t ::=
  a
  ∀ a : k . t

e ::=
  x
  e e
  λ x : t . e
  Λ a : k . e

• Terms depending on terms
• Types depending on terms

e ::=
  x
  *
  e e
  ∀ x : e . e
  λ x : e . e

• Terms depending on terms
• Terms depending on types
• Types depending on types
• Types depending on terms

e ::=
  x
  *
  e e
  ∀ x : e . e
  λ x : e . e