Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.floyd-cycle

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/floyd_cycle.clj1 definitions, 3 theorems

AHoF Floyd's Cycle Detection (tortoise and hare): detect a cycle in a linked list or a functional sequence x_{n+1} = f(x_n) in O(1) extra space, by advancing a SLOW pointer one step and a FAST pointer two steps per iteration. If the sequence is eventually periodic the fast pointer laps the slow one and they land on the same node; if it terminates, the fast pointer runs off the end. A cycle is detected exactly when the two pointers MEET (occupy the same position): meet? slow-position fast-position = (slow-position <= fast-position) AND (fast-position <= slow-position) (the positions are equal), over exact-rational (integer) positions. Proved native and axiom-free: the meeting test as position equality (a boolean conjunction of two comparisons via logic/if-data); that equal positions signal a cycle; the certificates that meeting positions coincide (each at most the other, native nnrat/at-most); and that different positions mean no meeting yet. The two-speed pointer advance is executable; what is proved is the meet decision. Requires audit/decide-nnrat-at-most, logic/if-data, nnrat/at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.floyd-cycle` prints this classification.

floyd-cycle/meet? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

floyd-cycle/same-position-detects-cycle :
  → floyd-cycle/meet? 4 4 = data/true

floyd-cycle/meeting-positions-coincide :
  → 4 ≤ 4

floyd-cycle/different-position-no-meeting :
  → floyd-cycle/meet? 2 5 = data/false