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: Yes.
  • Typable: Typable.
  • Linear: Yes.
  • Normal form: λd.y z
Samuel Frontull / Georg Moser / Vincent van Oostrom

Term: /d.(y) (z)