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: Not Typable.
  • Linear: Yes.
Samuel Frontull / Georg Moser / Vincent van Oostrom

Term: (/d.e) ((x) (x))