object LambdaCalculusOptimizer {

  sealed trait Term

  case class Var(name: String) extends Term
  case class App(left: Term, right: Term) extends Term
  case class Abs(param: String, body: Term) extends Term

  def optimize(term: Term): Term = term match {
    case App(left, right) => optimizeApplication(left, right)
    case Abs(param, body) => optimizeAbstraction(param, body)
    case _ => term
  }

  private def optimizeApplication(left: Term, right: Term): Term = (left, right) match {
    case (Abs(param, body), arg) => optimize(substitute(body, param, arg))
    case _ => App(optimize(left), optimize(right))
  }

  private def optimizeAbstraction(param: String, body: Term): Term = body match {
    case Var(name) if name == param => Var(name)
    case _ => Abs(param, optimize(body))
  }

  private def substitute(term: Term, variable: String, replacement: Term): Term = term match {
    case Var(name) if name == variable => replacement
    case App(left, right) => App(substitute(left, variable, replacement), substitute(right, variable, replacement))
    case Abs(param, body) => {
      if (param == variable) {
        Abs(param, body)
      } else if (!freeVariables(replacement).contains(param)) {
        Abs(param, substitute(body, variable, replacement))
      } else {
        val freshVar = generateFreshVariable(body, variable)
        Abs(freshVar, substitute(substitute(body, param, Var(freshVar)), variable, replacement))
      }
    }
  }

  private def freeVariables(term: Term): Set[String] = term match {
    case Var(name) => Set(name)
    case App(left, right) => freeVariables(left) ++ freeVariables(right)
    case Abs(param, body) => freeVariables(body) - param
  }

  private def generateFreshVariable(term: Term, existingVariable: String): String = {
    val existingVars = freeVariables(term)
    var i = 0
    var freshVar = existingVariable
    while (existingVars.contains(freshVar)) {
      i += 1
      freshVar = existingVariable + i.toString
    }
    freshVar
  }

object LambdaCalculusOptimizerTest {

  def main(args: Array[String]): Unit = {
    // Test case 1: β-reduction
    val term1 = App(Abs("x", Var("x")), Var("y"))
    val optimizedTerm1 = LambdaCalculusOptimizer.optimize(term1)
    println("Test case 1:")
    println("Original term: " + term1)
    println("Optimized term: " + optimizedTerm1)

    // Test case 2: n-reduction
    val term2 = Abs("x", App(Var("x"), Var("y")))
    val optimizedTerm2 = LambdaCalculusOptimizer.optimize(term2)
    println("Test case 2:")
    println("Original term: " + term2)
    println("Optimized term: " + optimizedTerm2)

    // Test case 3: β-reduction with name conflict
    val term3 = App(Abs("x", Var("x")), Var("x"))
    val optimizedTerm3 = LambdaCalculusOptimizer.optimize(term3)
    println("Test case 3:")
    println("Original term: " + term3)
    println("Optimized term: " + optimizedTerm3)
  }
}