     new AbsNode @varName, @body.reduce()
   @trace apply: (node) ->
     @body.replace @varName, node
+  # TODO Renaming is not correct as of now. Consider the case:
+  # (λy.λy1.x y y1)[x := y z]
+  # (λy.λy1.x y y1) must be alpha-renamed because y is free on (y z) and x is
+  # free on (x y y1). The current algorithm now chooses to rename y to y1, but
+  # is invalid, because it'll make the y variable, free in (λy1.x y y1) be bound
+  # to a new abstraction.
   @trace replace: (varName, node) ->
-    # TODO rename this abstraction's @varName in @body if @varName is in "node"'s free vars.
     # The parameter of this abstraction makes a new context, so no replacement
     # is needed.
     return @ if varName is @varName
-    new AbsNode @varName, @body.replace varName, node
+    # Avoid name collisions by renaming the @varName if it conflicts with any of
+    # the node's free vars.
+    freeVars = node.freeVars()
+    if @varName in freeVars
+      (@renameVar freeVars).replace varName, node
+    else
+      new AbsNode @varName, @body.replace varName, node
+
+  renameVar: (freeVars) ->
+    # The the letters part of the var in case it's an already renamed var.
+    base = @varName.replace /\d+/, ''
+    n = 1
+    name = base
+    while name in freeVars
+      name = base + n++
+    # A new AbsNode with the new name and the body with the renamed var.
+    new AbsNode name, (@body.replace @varName, new VarNode name)
+
+  freeVars: ->
+    removeAll @body.freeVars(), @varName
 
 class ApplyNode extends Node
   constructor: (@left, @right) ->

    "#{@left.leftApplyString()} #{@right.rightApplyString()}"
  rightApplyString: -> "(#{@})"
  @trace reduce: ->
    left = @left.reduce()
    (left.apply @right) or new ApplyNode left, @right.reduce()
  @trace apply: -> no
  @trace replace: (varName, node) ->
    new ApplyNode (@left.replace varName, node), (@right.replace varName, node)

# Global namespace.
Lambda = exports ? (@Lambda = {})

class VarNode extends Node
  constructor: (@name) ->
  toString: -> @name
  reduce: -> @
  apply: -> no
  replace: (varName, node) ->
    if varName is @name then node else @
  freeVars: -> [@name]

class AbsNode extends Node
  constructor: (@varName, @body) ->
