How can we terminate partial functions?

Stream: new members

[Oscar Matemb ⚛️]

partial def compute_energy_tail_recursive (positions : List (List Float)) (cell_length : List Float) (cutoff : Float := 3.0)
(i : Nat := 0) (j : Nat := 1) (accumulated_energy : Float := 0.0) : Float :=
  let num_atoms := positions.length
  if i >= num_atoms - 1 then
    accumulated_energy
  else
    if j >= num_atoms then
      compute_energy_tail_recursive positions cell_length cutoff (i + 1) (i + 2) accumulated_energy
    else
      let r_ij := listSub (positions[i]!) (positions[j]!) []
      let r_ij1 := apply_pbc r_ij cell_length
      let r_ij2 := minimum_image_distance r_ij1 cell_length
      let distance := vectorNorm r_ij2
      let accumulated_energy :=
        if distance < cutoff then
          accumulated_energy + lennard_jones_potential distance
        else
          accumulated_energy
      compute_energy_tail_recursive positions cell_length cutoff i (j + 1) accumulated_energy
```

```

[Kim Morrison]

Please read TPIL's section of induction and recursion. Look for termination_by.

Also read the blog post recursive definitions in Lean.

[Notification Bot]

This topic was moved here from #lean4 > How can we terminate partial functions? by Kim Morrison.