Size-change termination in Python
Decides termination of first-order functional programs by checking size-change graphs.
- File
size_change_termination.py, 98 lines- Level
- I0 not checked yet
- Toolchain
- Python 3.14, pytest 9
- Test framework
- pytest
- Run the tests
python3 -m pytest
# SPDX-License-Identifier: MIT
# Part of https://algorithm.tamnd.com/size-change-termination/. The authors are listed in prov/WBRKWD.jsonl.
"""Size-change termination: the closure algorithm of Lee, Jones and Ben-Amram.
A size-change graph G = (f, g, arcs) describes one call from function f to
function g. An arc (i, j, True) says that argument j of the call is strictly
smaller than parameter i of f; an arc (i, j, False) says that it is smaller or
equal. Parameters are numbered from 0.
"""
from dataclasses import dataclass
from typing import Hashable, Iterable
Arc = tuple[int, int, bool]
@dataclass(frozen=True)
class Graph:
"""A size-change graph from function src to function dst."""
src: Hashable
dst: Hashable
arcs: frozenset[Arc]
@dataclass(frozen=True)
class Result:
"""The verdict, with a witness when the graphs are not size-change terminating.
witness is an idempotent graph f -> f of the closure with no strict arc
i -> i, and walk lists the indices of the input graphs whose composition,
in this order, is the witness.
"""
terminates: bool
witness: Graph | None = None
walk: tuple[int, ...] | None = None
def make_graph(src: Hashable, dst: Hashable, arcs: Iterable[Arc]) -> Graph:
"""Build a graph, keeping one arc per pair (i, j), strict if any is strict. O(arcs)."""
best: dict[tuple[int, int], bool] = {}
for i, j, strict in arcs:
best[(i, j)] = best.get((i, j), False) or bool(strict)
return Graph(src, dst, frozenset((i, j, s) for (i, j), s in best.items()))
def compose(g: Graph, h: Graph) -> Graph:
"""Return g;h, the graph of the call g followed by the call h.
Requires g.dst == h.src. There is an arc i -> k if some j has i -> j in g
and j -> k in h; it is strict if one of the two arcs is strict.
Cost O(|g.arcs| * |h.arcs|).
"""
if g.dst != h.src:
raise ValueError("graphs do not compose")
by_src: dict[int, list[tuple[int, bool]]] = {}
for j, k, s in h.arcs:
by_src.setdefault(j, []).append((k, s))
return make_graph(
g.src,
h.dst,
((i, k, s1 or s2) for i, j, s1 in g.arcs for k, s2 in by_src.get(j, ())),
)
def size_change_terminates(graphs: list[Graph]) -> Result:
"""Decide size-change termination of a finite set of size-change graphs.
Computes the closure S of the graphs under composition along walks of the
call graph, then checks every idempotent graph f -> f in S for a strict
arc i -> i. With F functions of at most p parameters, |S| is at most
F^2 * 3^(p^2), and the time is O(|S| * |graphs| * p^4) in the worst case;
the problem is PSPACE-complete, so an exponential closure is expected in
the worst case.
"""
base = [make_graph(g.src, g.dst, g.arcs) for g in graphs]
walks: dict[Graph, tuple[int, ...]] = {}
work: list[Graph] = []
for idx, g in enumerate(base): # @line L1
if g not in walks:
walks[g] = (idx,)
work.append(g)
while work: # @line L2
g = work.pop() # @line L3
for idx, h in enumerate(base): # @line L4
if h.src != g.dst:
continue
k = compose(g, h) # @line L5
if k not in walks: # @line L6
walks[k] = walks[g] + (idx,)
work.append(k)
for g, walk in walks.items(): # @line L7
if g.src == g.dst and compose(g, g) == g: # @line L8
if not any(i == j and s for i, j, s in g.arcs): # @line L9
return Result(False, g, walk)
return Result(True) # @line L10
test_size_change_termination.py 123 lines
# SPDX-License-Identifier: MIT
# Part of https://algorithm.tamnd.com/size-change-termination/. The authors are listed in prov/WBRKWD.jsonl.
import random
from size_change_termination import Graph, compose, make_graph, size_change_terminates
def descending_cycle(g: Graph) -> bool:
"""True if the arcs of a graph f -> f contain a cycle through a strict arc.
Brute force: i -> j is on a cycle iff j reaches i, by plain search.
"""
succ: dict[int, set[int]] = {}
for i, j, _ in g.arcs:
succ.setdefault(i, set()).add(j)
def reaches(a: int, b: int) -> bool:
seen, stack = {a}, [a]
while stack:
u = stack.pop()
if u == b:
return True
for v in succ.get(u, ()):
if v not in seen:
seen.add(v)
stack.append(v)
return False
return any(s and reaches(j, i) for i, j, s in g.arcs)
def closed_walks(graphs: list[Graph], max_len: int):
"""Yield (walk, composed graph) for every closed walk of length <= max_len."""
stack = [((i,), g) for i, g in enumerate(graphs)]
while stack:
walk, g = stack.pop()
if g.src == g.dst:
yield walk, g
if len(walk) < max_len:
for i, h in enumerate(graphs):
if h.src == g.dst:
stack.append((walk + (i,), compose(g, h)))
def check(graphs: list[Graph], max_len: int = 6) -> bool:
res = size_change_terminates(graphs)
if res.terminates:
# Every periodic call sequence w^omega must have a descending thread.
for walk, g in closed_walks(graphs, max_len):
assert descending_cycle(g), walk
else:
assert res.witness is not None and res.walk is not None
g = graphs[res.walk[0]]
g = make_graph(g.src, g.dst, g.arcs)
for i in res.walk[1:]:
g = compose(g, graphs[i])
assert g == res.witness
assert g.src == g.dst and compose(g, g) == g
assert not descending_cycle(g)
return res.terminates
def G(src, dst, *arcs) -> Graph:
return make_graph(src, dst, arcs)
def test_ackermann() -> None:
graphs = [
G("ack", "ack", (0, 0, True)),
G("ack", "ack", (0, 0, False), (1, 1, True)),
G("ack", "ack", (0, 0, True)),
]
assert check(graphs)
def test_page_example() -> None:
# p(m, n, r): r > 0 calls p(m, r - 1, n); n > 0 calls p(r, n - 1, m).
g1 = G("p", "p", (0, 0, False), (2, 1, True), (1, 2, False))
g2 = G("p", "p", (2, 0, False), (1, 1, True), (0, 2, False))
assert check([g1, g2])
res = size_change_terminates([g1, g2])
assert res.terminates
def test_swap_loops() -> None:
res = size_change_terminates([G("f", "f", (0, 1, False), (1, 0, False))])
assert not res.terminates
assert res.witness == G("f", "f", (0, 0, False), (1, 1, False))
assert check([G("f", "f", (0, 1, True), (1, 0, False))])
def test_mutual_recursion() -> None:
# f(x) calls g(x - 1); g(y) calls f(y): every cycle goes through the decrease.
assert check([G("f", "g", (0, 0, True)), G("g", "f", (0, 0, False))])
assert not check([G("f", "g", (0, 0, False)), G("g", "f", (0, 0, False))])
def test_edges() -> None:
assert size_change_terminates([]).terminates
assert size_change_terminates([G("f", "g", (0, 0, False))]).terminates
res = size_change_terminates([G("f", "f")])
assert not res.terminates and res.walk == (0,)
def test_random_against_walks() -> None:
rng = random.Random(7)
seen = {True: 0, False: 0}
for _ in range(600):
names = ["f", "g"][: rng.randint(1, 2)]
arity = {f: rng.randint(1, 3) for f in names}
graphs = []
for _ in range(rng.randint(1, 3)):
a, b = rng.choice(names), rng.choice(names)
arcs = [
(i, j, rng.random() < 0.4)
for i in range(arity[a])
for j in range(arity[b])
if rng.random() < 0.4
]
graphs.append(make_graph(a, b, arcs))
seen[check(graphs)] += 1
assert seen[True] > 50 and seen[False] > 50
What the next level needs
- the tests did not run in this build