Alpha Avoidance

Context:
Typed Term:
Untyped Term:
  • UT = (UT) | /x ... y.UT | UT ... UT | x
  • TYPE = 0 | TYPE -> TYPE
  • CTX = _ | x^TYPE ... y^TYPE
  • TT = (TT) | /x^TYPE ... y^TYPE.TT | TT ... TT | x
Max depth:
  • Variable capture: No.
  • Safe naming: No.
  • Typable: Typable.
  • Linear: Yes.
  • Normal form: x (c (c a))
Samuel Frontull / Georg Moser / Vincent van Oostrom

Term: (x) ((c) ((c) ((/i.(/x.a) (x)) ((x) (y)))))