[WIP] Termination Checking

[OzairFaizan]

Termination Checking

The goal of this PR is to introduce a termination checker phase for the functional subset of Scala.

Currently,

• Adds the infrastructure:
  • CheckTermination compiler phase, which forbids all recursive calls.
  • @terminates function annotation.
  • -Ycheck-termination compiler flag.
• Adds simple structural recursion termination check:
  • Looks at matches on inductive types to find sub-terms.
  • Checks that recursive calls are on sub-terms of input arguments.

Additional notes

This is an EPFL Research Project supervised by @mbovel.

[bishabosha]

I am curious how this will develop, is the goal to support some subset of recursion if the iteration condition can be proven to reach a base case?

[mbovel]

I am curious how this will develop, is the goal to support some subset of recursion if the iteration condition can be proven to reach a base case?

Yes, exactly.

We will start with direct structural recursion on inductive types. For example, recursion on a sub-list:

def sum(l: List[Int]): Int =
  l match
    case Nil => 0
    case x :: xs => x + sum(xs) // xs is strictly smaller than l

Later, we could extend this to more general patterns, such as mutual recursion or recursion on numeric arguments.

The main motivation is integration with refinement types. We will need termination guarantees for definitions that appear in erased proofs in order to preserve soundness.

[mbovel]

Failing test:

Error:  scala-library-bootstrapped: Failed binary compatibility check against org.scala-lang:scala-library:3.8.0! Found 1 potential problems (filtered 172)
Error:   * class scala.annotation.terminates does not have a correspondent in other version
Error:     filter with: ProblemFilters.exclude[MissingClassProblem]("scala.annotation.terminates")
Error:  
Error:  Filters in MiMaFilters.Scala3Library are used in this check.

You will probably need to add a filter in there:

scala3/project/MiMaFilters.scala

Lines 8 to 19 in f302695

	val ForwardsBreakingChanges: Map[String, Seq[ProblemFilter]] = Map(
	// Additions that require a new minor version of the library
	Build.mimaPreviousDottyVersion -> Seq(
	ProblemFilters.exclude[DirectMissingMethodProblem]("scala.caps.package#package.freeze"),
	ProblemFilters.exclude[DirectMissingMethodProblem]("scala.caps.package#package.cap"),
	ProblemFilters.exclude[FinalClassProblem]("scala.Function1$UnliftOps$"),
	ProblemFilters.exclude[FinalClassProblem]("scala.jdk.Accumulator$AccumulatorFactoryShape$"),
	ProblemFilters.exclude[DirectMissingMethodProblem]("scala.collection.ArrayOps.iterateUntilEmpty$extension"),
	ProblemFilters.exclude[DirectMissingMethodProblem]("scala.collection.ArrayOps.scala$collection$ArrayOps$$elemTag$extension"),
	ProblemFilters.exclude[MissingFieldProblem]("scala.language#experimental.safe"),
	ProblemFilters.exclude[MissingClassProblem]("scala.language$experimental$safe$")
	))

[noti0na1]

Later, we could extend this to more general patterns, such as mutual recursion or recursion on numeric arguments.

How do you tell if these is any recursion and check it statically?

[mbovel]

How do you tell if these is any recursion and check it statically?

We'd probably need to construct a call graph, and check a measure is decreasing across calls.

We'll try to replicate part of what is done in Lean or Rocq. We're not aiming for full generality of course.